A Practical Introduction to Haskell GADTs
summary
Claim: GADTs let the compiler assume different types in different pattern branches so invariants live in types, reducing unsafeCoerce. Workshop builds a simply typed Lambda interpreter ("Glam") and several exercises: singleton indices, heterogeneous lists indexed by promoted type-level lists, an Elem/LM index and an evaluator that typechecks. Uses GHC extensions (GADTs, DataKinds, ScopedTypeVariables), shows GADTs give branch-specific type info, explains need top-level type signatures for untouchable variables, demonstrates de Bruijn indices with the LM index trick, and notes a GHC warning/bug fixed around 7.12.
AI-written summary · about
chapters (22)
- 0:00Introduction to GADTs
- 4:51GADT fundamentals
- 8:24First live GADT example
- 11:26Understanding type equality
- 14:03Syntax and alternative definitions
- 17:36Exercise: Defining GADTs
- 22:20Exercise solution review
- 25:36Deriving shows and constraints
- 28:12Type inference challenges
- 31:38Principled typing tradeoff
- 36:03Scoped type variables
- 38:05Higher rank types debate
- 42:03GHC bugs and warnings
- 45:43Heterogeneous lists
- 51:25Promoted data types
- 55:13Indexing into HLists
- 58:27Exercise solution: HList get
- 1:02:04Introduction to Glamda
- 1:05:28De Bruijn indices
- 1:07:58Expression data type
- 1:11:51Type-safe evaluation
- 1:15:32Final takeaways and resources
related talks
01h 00mType Theory Behind the Glasgow Haskell Compiler Internals (Part 5)
49mType Theory Behind the Glasgow Haskell Compiler Internals (Part 2)
57mType Theory Behind Glasgow Haskell Compiler Internals (Part 1)
58mType Theory Behind the Glasgow Haskell Compiler Internals (Part 3)
01h 01mType Theory Behind the Glasgow Haskell Compiler Internals (Part 6)
58mType Theory Behind the Glasgow Haskell Compiler Internals (Part 4)
49mA Hands on Tutorial to Generic Programming in Haskell (Part 2)
12mSingletons and You in Haskell