Type Theory Forall #39 Equality, Quotation, Bidirectional Type Checking - David Christiansen
Jun 13, 2024
David Christiansen, former Executive Director of the Haskell Foundation, talks about writing The Little Typer, Equality, Bidirectional Type Checking, and Quotation with the host. They explore the challenges of book reprints, bi-directional type checking, macro implementation, and Lean macros. Technical discourse on content levels and audience interaction, with insights on normalization by evaluation and personal anecdotes.
AI Snips
Chapters
Transcript
Episode notes
Apply Bidirectional Type Checking
- Use bidirectional type checking to make type checking syntax-directed without full higher-order unification.
- Put introduction forms in checking mode and elimination forms in synthesis mode to minimize user annotations.
Conversion Breaks Syntax-Directed Rules
- The conversion (or subsumption) rule breaks syntax-directedness and must be handled explicitly in the bidirectional design.
- Using conversion when switching from synthesis to checking localizes where equality/subtyping checks occur.
Prefer Annotations Over Full Unification
- When implementing dependently-typed features (e.g., implicit arguments), avoid higher-order unification by using bidirectional checking and explicit implicitness.
- Request annotations when synthesis fails and postpone work rather than building full higher-order unification.