Typing the Y Combinator
summary
Claim: adding a recursive type operator mu — mu as type-level fixed point — lets a statically-typed lambda calculus express the Y combinator and encode lists, streams and other recursive data. Two implementations appear: equi-recursive types (expansion equals mu) and iso-recursive types with explicit roll and unroll, and practical Haskell/OCaml encodings show roll/unroll inserted to satisfy the type checker so the Y combinator actually typechecks. Data versus codata maps to least versus greatest fixpoints.
AI-written summary · about
chapters (11)
- 0:00Start
- 5:38Using the New Operator
- 15:34The Y Combinator
- 19:12Eques Recursive Approach
- 23:13Typing Rules
- 25:22Production Languages
- 35:21Define Our Y Combinator
- 38:10Structural Induction
- 40:43Symmetric Notion of Greatest Fixed Points
- 43:54Conclusion
- 44:04Main Takeaways
related talks
58mMonoidal Catamorphisms
01h 12mTruth about Types
46mCorecursion, Codata, and Just a Little Combinatorial Game Theory
01h 39mIsomorphic Reasoning: Counting with Types Part 1
01h 52mIsomorphic Reasoning: Counting with Types Part 3
02h 28mIsomorphic Reasoning: Counting with Types Part 2
01h 20mA Practical Introduction to Haskell GADTs
24mHigher order programming with probabilistic effects: A model of stochastic memo...