Type Theory Behind the Glasgow Haskell Compiler Internals (Part 4)
summary
Explains that GHC Core is essentially System F Omega plus algebraic datatypes for decades, demonstrates concrete translations from Haskell source into explicit-core (GHC Core dumps shown), and gives the actual typing rules, erasure behavior, and proofs or counterexamples for progress/preservation and normalization. Covers practical extensions — GADTs, type families, data kinds, type/kind equality — with the translation algorithms and where type inference becomes undecidable, and states work in progress to move Core toward dependent types without claiming they are production-ready.
AI-written summary · about
chapters (9)
- 0:00Type derivation and proof systems
- 5:31Progress and preservation
- 10:30Safety in simply typed lambda
- 18:22Limitations of simply typed lambda
- 20:38Lambda cube introduction
- 33:37System F and parametricity
- 47:02System F in Haskell practice
- 51:22System F Omega and type functions
- 55:19GHC Core and System F Omega history
related talks
01h 20mA Practical Introduction to Haskell GADTs
51mPragmatism, Puritanism and Functional Programming
01h 12mTruth about Types
01h 52mIsomorphic Reasoning: Counting with Types Part 3
02h 28mIsomorphic Reasoning: Counting with Types Part 2
22mA Type System For Feature Engineering (Extended Abstract)
57mPropositions as Types
44mFunctional Programming: Failed Successfully