Type Theory Behind the Glasgow Haskell Compiler Internals (Part 2)
summary
Follows the GHC compilation pipeline down to the internal, explicitly typed GHC Core, shows how Haskell features become concrete Core constructs (GADTs, type families, data kinds and the move toward dependent types), demonstrates the -ddump-simpl workflow and optimizer loop with a concrete example that eliminates a function, and explains what is lost (location info, hard-to-map-to-source transformations) and what gains appear (System F style foundations and year-by-year Core changes since 2012).
AI-written summary · about
chapters (13)
- 0:00Compiler overview
- 2:03Six main compiler stages
- 4:46Compilation pipeline rationale
- 10:51Parsing and renaming
- 17:37Abstract syntax tree
- 20:44Declaration types
- 24:52Type checking and inference
- 28:23GHC core intermediate language
- 31:00Type theory connection
- 34:08Core expression analysis
- 36:25Compiler debugging challenges
- 39:41Binders and optimizations
- 42:04Desugaring example and conclusion
related talks
01h 20mA Practical Introduction to Haskell GADTs
51mPragmatism, Puritanism and Functional Programming
01h 12mTruth about Types
44mFunctional Programming: Failed Successfully
48mEnhancing your Haskell with Dependently Typed Programming
21mFinally Tagless DSLs and MTL
22mA Type System For Feature Engineering (Extended Abstract)
41mIdris: Practical Dependent Types with Practical Examples