Type Theory Behind the Glasgow Haskell Compiler Internals (Part 6)
summary
Traces the concrete extensions to GHC Core: role-based coercions (implemented in 2015), System FC variants (FC2, FC‑, FCPro) that add roles, data promotion and kind polymorphism (data kinds / PolyKinds rolled into GHC 7.2–7.6 around 2012–2013), and the move to collapse kinds into types with TypeInType (GHC 8.0). Claims get formalized: the dependent-Haskell design (System D) is machine‑checked in Coq (2017 paper). Several proofs (progress/preservation) and multi‑year implementation effort are explicit; some features are proven but not yet production‑ready.
AI-written summary · about
chapters (16)
- 0:00Intro
- 1:32New types
- 2:20Real expressions
- 3:43The typing rule
- 6:00Example
- 12:38System FC2
- 14:30System FC Pro
- 20:07Type Family
- 21:05Equality
- 27:08Type and Type
- 30:14GHC Core
- 36:01Functional Programming
- 39:24SystemD
- 41:48Extended Type System
- 42:58System FC
- 51:30System D
related talks
01h 20mA Practical Introduction to Haskell GADTs
51mPragmatism, Puritanism and Functional Programming
01h 12mTruth about Types
44mFunctional Programming: Failed Successfully
22mA Type System For Feature Engineering (Extended Abstract)
02h 28mIsomorphic Reasoning: Counting with Types Part 2
48mEnhancing your Haskell with Dependently Typed Programming
01h 52mIsomorphic Reasoning: Counting with Types Part 3