The Calculated Typer (Functional Pearl)
summary
Derives type checkers mechanically from a behavioural semantics by solving an inequality spec with equational, fold-based calculation and fold fusion to turn specs into folding operators; introduces a partial-order of types (error as bottom, optional top) so monotonicity is automatic; produces correct-by-construction type checkers and handles exception/checked-exception extensions; main results and proofs are Agda formalization with artifacts available (Zenodo, ACM DOI); lambda support in the type-checker derivation requires termination assumptions, while calculating typing rules avoids that limitation.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 3:18Source language and semantics
- 8:19Reframing type checker spec
- 13:01Type checkers as folds
- 21:11Monotonicity problem
- 28:41Summary
- 31:09Question and answer session
related talks
19mIll-Typed Programs Don't Evaluate
15mMonadic Compiler Calculation (Functional Pearl)
26mType Narrowing the Hard Way
20mTowards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
22mType-Safe Code Generation With Algebraic Effects and Handlers
30mType-Checking Heterogeneous Sequences in a Simple Embeddable Type System
14mType-Sensitive Algebraic Macros