Type-Sensitive Algebraic Macros

Explore a short research paper presentation on Type-Sensitive Algebraic Macros delivered at the PEPM 2025 conference by April Gonçalves and Robert Atkey from the University of Strathclyde. This 14-minute video introduces a novel approach to metaprogramming in typed languages, addressing the challenges that make it difficult and error-prone despite advances by Idris and Lean teams. Learn about their proposed type-sensitive algebraic theory for typechecker scripting, which aims to provide a more principled approach to type-directed macros. The presentation demonstrates how their theory encodes typechecking and elaboration for STλC, and showcases two variations—Bidirectional STλC and Search-based Type Inference—to illustrate the framework's versatility. The research is implemented in Agda and was presented at the ACM SIGPLAN-sponsored PEPM 2025 conference on January 21, 2025.