Category Theory Through Functional Programming (part 1/3)

on YouTube ↗52m

" summary

A practical walk through category theory implemented in Haskell and Scala using real code that typechecks and illustrates concepts: categories encoded as types and morphisms, GHC 8 and advanced extensions required, a monoid as a one‑object category, orders as categories, products shown as the usual product as pair type with the universal arrow and a constructive uniqueness sketch that typechecks though full equality proofs need dependent types, coproducts as sums, and the arrow functor (D -> -) given by postcomposition.

AI-written summary · about

" chapters (8)

1. 0:00Introduction
2. 3:13Defining category in Haskell
3. 9:00Categories as monoids and sets
4. 16:49Universal constructions and products
5. 26:10Initial objects and duality
6. 32:57Co-products and duality in Haskell
7. 41:49Functors between categories
8. 49:00Functors in Haskell and conclusion

" related talks

• 01h 29mCategory Theory Track by Bartosz Milewski Part 1Bartosz Milewski · ZuriHac 2023
• 41mA Pragmatic Introduction to Category TheoryDaniela Sfregola · Lambda World 2017
• 51mCategory Theory for the Working HackerPhilip Wadler · Lambda World 2016
• 42mA pragmatic introduction to Category TheoryDaniela Sfregola · Scala Days Berlin 2018
• 40mA Pragmatic Introduction to Category TheoriesDaniela Sfregola · Code Mesh 2017
• 32mClassical Category Theory in Plain ScalaVlad Patryshev · Scale By The Bay 2018
• 01h 11mCategories for the Working HackerPhilip Wadler · Lambda Days 2018
• 42mWhat did category theory do for us?Sergei Winitzki · Scale By The Bay 2019