Type-Sensitive Algebraic Macros
summary
Claims a type-sensitive algebraic theory that directly encodes typechecking and elaboration for STλC, plus concrete variants: Bidirectional STλC and search-based type inference, all implemented as macros in Agda and exposed in a GitHub playground. Macros are algebraic operations (intro, goal, has, hole) composed with algebraic effects and handlers to swap checkers versus elaborators, and a meta-variable unification API (new, unify, choice) implements Prolog-style tactics. Equations are stated but not yet fully proved; System M and dependent-type extensions are in progress.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 0:21Speaker introduction
- 1:04STLC background
- 1:24Type checker with algebra
- 2:49Macros in type checker
- 3:11Type-sensitive macros
- 5:00Higher-order syntax in Agda
- 5:23Extending macros to elaboration
- 6:06Bidirectional type checking
- 7:33Type theories algebra
- 8:18Macros in unification system
- 9:47Future work beyond STLC
- 10:32Resources and implementation
- 11:15Q&A: Motivation
- 12:17Q&A: Algebraic effects
- 12:40Q&A: Applicative vs monadic
- 14:08Closing remarks
related talks
12mMulti-Stage Programming with Generative and Analytical Macros
24mScoped and Typed Staging by Evaluation
30mConstraint Typing with Boolean Algebra
25mShallowly embedding type theories
16mAn Intrinsically Typed Compiler for Algebraic Effect Handlers
46mThe Calculated Typer (Functional Pearl)
20mPredictable macros for hindley milner
40mDomain Specific Type Systems