Type Theory Behind Glasgow Haskell Compiler Internals (Part 1)
summary
Claim: GHC implements type theory concretely, not just as lore—GHC Core = System F + algebraic datatypes and successive extensions add GADTs, type families, data kinds, type/kind equality and preliminary dependent-type features, with explicit translation algorithms and type-theoretic properties. Tooling details: bootstrapping via stage1→stage2 compilers, runtime system largely in C (~10% C), build-and-test takes hours, repo shows hundreds of contributors and ~10k issues. Slides and exercises live on the linked GitHub for hands-on follow-up.
AI-written summary · about
chapters (20)
- 0:00Intro
- 4:10GHC Development Process
- 9:45The Glasgow Haskell Compiler
- 14:45New Contributors
- 16:55Documentation
- 19:15Feature Requests
- 20:45Resources
- 23:10Github
- 25:05Directory structure
- 29:55C code
- 32:50Libraries
- 37:20Runtime System
- 39:40Why build a compiler
- 44:10Building a compiler
- 47:30Read GHC directory
- 48:45Alternative build system
- 50:25Advice for newcomers
- 52:50Lowhanging fruits
- 54:10Important advice
- 55:50Workshop structure
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)
48mEnhancing your Haskell with Dependently Typed Programming
57mPropositions as Types
41mWar Time Proofs and Futuristic Programs