Isomorphic Reasoning: Counting with Types Part 3
summary
Shows how to use category-theory tools (Yoneda lemmas, representable/Naperian and container functors, products/coproducts, initial/terminal objects) to treat polymorphic types as arithmetic and count their inhabitants, including discussion of observational equality and parametricity. Covers System F (with de Bruijn indices) and demonstrates an implementation of the type-algebra and a parser/printer in Haskell/Scala/Idris that enumerates inhabitants via sequences of isomorphisms, and outlines possible extensions like functor fixpoints and System Fω.
AI-written summary · about
related talks
01h 15mA Crash Course in Category Theory
01h 11mHands on Chat About Categories
51mCategory Theory for People who Can't be Bothered to Learn It (Part 2)
55mCategory Theory - Part 3 of 6
01h 12mTruth about Types
48mCategory Theory: You Already Know It
36mCategory Theory: An Abstraction for Anything
01h 00mCategory Theory - Part 4 of 6