Type Theory Behind the Glasgow Haskell Compiler Internals (Part 3)
summary
History of how GHC Core actually changes: precise extensions (GADTs, type families, data kinds, type/kind equality, moves toward dependent types), the encoding or the Core extension chosen, and the translation algorithms used each year. Details about evaluation and lowering: the STG machine, codegen targets like C--/LLVM/assembly, and what the generated artifacts look like. Practical hooks: user rewriting rules, compiler plugins, using GHC as a library, and the type‑theoretic properties proved (or not) for each extension.
AI-written summary · about
chapters (12)
- 0:00Start
- 8:42Cogeneration
- 11:26Vm Generation
- 13:36How To Extend Your Compiler
- 14:42Writing Rules
- 16:01Plugins
- 24:44Type Theory
- 26:21What Is Lambda Calculus
- 27:24Lambda Calculus
- 44:53Typing Rules
- 45:40Assign Types to the Lambda Abstraction
- 55:36Typing Rule for Variable
related talks
01h 20mA Practical Introduction to Haskell GADTs
51mPragmatism, Puritanism and Functional Programming
58mSome History of Functional Programming Languages
44mFunctional Programming: Failed Successfully
01h 12mTruth about Types
48mEnhancing your Haskell with Dependently Typed Programming
49mFree vs Tagless Final: What, Why, When?
22mA Type System For Feature Engineering (Extended Abstract)