Type Theory Behind the Glasgow Haskell Compiler Internals (Part 5)
summary
Tracks the concrete claim that GHC Core grows by one clean extension — System F_Omega → System FC — adding coercions as types to compile GADTs and associated types via explicit casts, dictionaries and type-level functions. Shows the implementation: explicit coercion arguments, dictionaries-as-records, typechecker+optimizer that erase coercions at runtime. Demonstrates a real bug (several years of exploitable newtype-deriving mishaps revealing Bool internals) and the practical fix: roles/nominal vs representational equality (2011) that prevents the misuse and keeps performance.
AI-written summary · about
chapters (10)
- 0:00Start
- 1:13Algebraic Data Types in the Ghc
- 3:11Algebraic Data Types and Associated Types
- 4:12Algebraic Data Types
- 5:20Generalized Algebraic Data Types
- 11:45Type Constraint
- 16:43Cast Operator
- 56:14Nominal Equality
- 56:25Type Synonyms
- 57:16Parametric and Non-Parametric Type Variable Occurrences
related talks
01h 20mA Practical Introduction to Haskell GADTs
51mPragmatism, Puritanism and Functional Programming
01h 12mTruth about Types
02h 28mIsomorphic Reasoning: Counting with Types Part 2
01h 52mIsomorphic Reasoning: Counting with Types Part 3
22mA Type System For Feature Engineering (Extended Abstract)
01h 39mIsomorphic Reasoning: Counting with Types Part 1
44mFunctional Programming: Failed Successfully