Type-safe generation of modules in applicative and generative styles
summary
Defines two staged ML-like languages, lambda-G and lambda-A, with a type-preserving translation and implementation into plain MetaOCaml using a genlet primitive to avoid duplication. Claims soundness of module-code generation for both generative functors and applicative functors, handles nested modules, and proves typing is preserved. Microbenchmarks show eliminated indirection and no code-explosion; generated modules beat non-generated ones on up to 10 nested functor applications (example drawn from MirageOS use).
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:39MetaML-style limits
- 3:14ML modules performance
- 5:56Motivation for code gen
- 6:18Staging expression constructs
- 7:04Staging modules new
- 8:18$-operator type safety
- 9:03Staging IntEq MakeSet
- 9:46Generative vs applicative
- 10:54Lambda-G and lambda-A types
- 11:42Translations to MetaOCaml
- 12:53Performance experiments
- 13:59Summary
related talks
20mGenerating Well-Typed Terms that are not "Useless"
45mLogic Meta Programming for Functional Languages
23mBetter Defunctionalization through Lambda Set Specialization
36mDependently Typed Multi-Stage Programming, Revisited
22mType-Safe Code Generation With Algebraic Effects and Handlers
24mOn the design and implementation of Modular Explicits
24mCode Extraction from Coq to ML-like languages
50mA Type-Theoretic Framework for Certified Meta-programming