Type Arithmetic and the Yoneda Lemma
summary
Type signatures get counted and proven equal to set cardinalities using category theory and code: natural transformations, Yoneda lemma, and representable functors turn parametric reasoning into concrete isomorphisms. Haskell/Scala examples and supplied programs enumerate cases (Bool->Bool = 4, Bool×Bool = 4, Maybe = 1+|a|), and the surprising results are certified (for all a. a -> a has 1 inhabitant, (a,a) -> a corresponds to two inhabitants). Slides and exercises implement and verify the isomorphisms, and the method yields mechanically checkable proofs.
AI-written summary · about
chapters (8)
- 0:00Type arithmetic and Yoneda
- 10:05Type arithmetic foundations
- 20:28Liveness and type equality
- 30:07Category theory basics
- 40:30Products and coproducts
- 50:13Representable functors
- 57:27Yoneda with concrete types
- 1:02:26Advanced type signatures
related talks
54mCategory Theory Through Functional Programming (part 3/3)
57mApplied category theory and abstract algebra
34mFormalizing the ∞-categorical Yoneda lemma
52mCategory Theory Through Functional Programming (part 1/3)
51mCategory Theory for the Working Hacker
23mImplementing a category-theoretic framework for typed abstract syntax
31mAlgebraic Data Types, Categorically
23mReasoning about types and code