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