一句话：将多阶段编程与 OCaml 模块函子结合，形式化设计并证明类型可靠性与阶段区分。
多阶段编程可消除抽象与性能的矛盾，但其与大规模程序语言特性（如模块系统）的交互尚缺研究，阻碍其集成到现有语言并在大程序中有效使用。本文以 OCaml 宏扩展 MacoCaml 为基础，研究如何将编译期代码生成（宏与引用）与模块函子结合，讨论求值顺序等设计选择，并通过精化（elaboration）给出形式化演算。作者证明该设计满足句法类型可靠性、精化可靠性以及阶段区分等关键元理论性质。该工作为 OCaml 宏系统的后续探索与实现奠定基础。
Multi-stage programming has been used in a wide variety of domains to eliminate the tension between abstraction and performance. However, the interaction of multi-stage programming features with features for programming-in-the-large remains understudied, hindering the full integration of multi-stage programming support into existing languages, and limiting the effective use of staging in large programs. We take steps to remedy the situation by studying the extension of MacoCaml, a recent OCaml extension that supports compile-time code generation via macros and quotations , with module functors, the key mechanism in OCaml for assembling program components into larger units. We discuss design choices related to evaluation order, formalize our calculus via elaboration, and show that the design enjoys key metatheoretical properties: syntactic type soundness, elaboration soundness, and phase distinction. We believe that this study lays a foundation for the continued exploration and implementation of the OCaml macro system.
@article{ChiangYWX24,
title = {Staged Compilation with Module Functors},
author = {Tsung-Ju Chiang and Jeremy Yallop and Leo White and Ningning Xie},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674649}
}