Category Theory for the Working Hacker
summary
Explains how types, logic and category theory are the same machinery by giving concrete categorical semantics for lambda calculus terms: models products and sums with commuting diagrams and a universality condition, shows pairing = ⟨f,g⟩ and case = [f,g], and treats functions as exponentials (currying = adjunction to product). Notes monads and functors originate in category theory, points out identity = pair(first,second) only holds in total languages (Idris/Agda/Coq), and demonstrates product/sum duality by flipping arrows.
AI-written summary · about
chapters (7)
- 0:00The value of persistence
- 2:40Propositions as types
- 7:31Introduction to categories
- 12:44Understanding products
- 28:21Understanding sums
- 38:38Lambda calculus semantics
- 44:50Duality and concluding thoughts
related talks
01h 11mCategories for the Working Hacker
52mCategory Theory Through Functional Programming (part 1/3)
01h 29mCategory Theory Track by Bartosz Milewski Part 1
56mCategory Theory Through Functional Programming (part 2/3)
42mWhat did category theory do for us?
57mApplied category theory and abstract algebra
02h 24mCategory Theory Track
01h 31mCategory Theory Track by Bartosz Milewski Part 2