Safe Pattern Generation for Multi-Stage Programming
summary
Design for typed generation of patterns whose shape is only known at staging time, implemented as a library on Metro camel. Core techniques are inductive code definitions to build bodies with arbitrarily many bound variables and existential wrappers plus a continuation-based encoding to hide varying pattern-body types. Demonstrates list-map loop unrolling generator that selects unrolling depth at run time (examples show ~16 optimal) and produced generated code with performance matching handwritten implementations; scope-extrusion checks remain work in progress.
AI-written summary · about
chapters (14)
- 0:00Multi-stage programming intro
- 2:53Pattern generation motivation
- 4:38Safe pattern generation goals
- 8:07Pattern type system design
- 12:58Generating pattern cases
- 15:49Dynamic pattern generation
- 19:20Inductive code definitions
- 21:07Case study list map unrolling
- 22:30System extensibility & future work
- 23:53Resources & conclusion
- 24:34Q&A: record patterns
- 25:37Q&A: benchmarking
- 26:39Q&A: nested patterns
- 28:02Q&A: unexpected apps
related talks
36mDependently Typed Multi-Stage Programming, Revisited
12mMulti-Stage Programming with Generative and Analytical Macros
08mCompiling pattern matching to in-place modifications
22mType-Safe Code Generation With Algebraic Effects and Handlers
14mMulti-stage Programming in the Large with Staged Classes
25mRecursive Program Synthesis using Paramorphisms
30mConstrained generation of well-typed programs
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)