一句话:提出 MacoCaml,一种结合宏、阶段分离和基于引用的 staging 的 OCaml 编译时代码生成设计,并给出形式化与实现。
本文提出 MacoCaml,一种为 OCaml 语言设计的编译时代码生成新方案。它创新性地结合了宏、阶段分离与基于引用的 staging:宏作为编译时绑定,表达式通过 staging 注解跨求值阶段,编译时求值发生在顶层 splice 中。作者形式化了一个类型化源演算 maco,支持交错类型检查与编译时代码生成,并带有显式编译时堆的引用和模块。研究证明了可靠性和阶段区分等关键性质。MacoCaml 已在 OCaml 编译器中实现,并通过移植两个重要库验证了其有效性。
We introduce MacoCaml, a new design and implementation of compile-time code generation for the OCaml language. MacoCaml features a novel combination of macros with phase separation and quotation-based staging, where macros are considered as compile-time bindings, expression cross evaluation phases using staging annotations, and compile-time evaluation happens inside top-level splices. We provide a theoretical foundation for MacoCaml by formalizing a typed source calculus maco that supports interleaving typing and compile-time code generation, references with explicit compile-time heaps, and modules. We study various crucial properties including soundness and phase distinction. We have implemented MacoCaml in the OCaml compiler, and ported two substantial existing libraries to validate our implementation.
@article{paperbot1907,
title = {MacoCaml: Staging Composable and Compilable Macros},
author = {Ningning Xie and Leo White and Olivier Nicole and Jeremy Yallop},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {ICFP},
year = {2023},
doi = {10.1145/3607851}
}