一句话:重新审视 ANF 的底层内涵性质,论证应优先采用 monadic form,只在低层命令式中间表示中做 A-规范化。
ANF 是被广泛研究的中间表示:它在语法中显式化局部控制流与数据流,并让控制流图等价的程序具有唯一范式。但 ANF 难以高效实现,也难以扩展新的词法作用域构造(如带作用域的区域分配),根源在于 commuting conversion 的规范化十分困难。本文指出这一源于高层演算与形式模型的传统看法是错误的:通过研究 ANF 的底层内涵(intensional)性质,作者导出一个 commuting conversion 规范化很简单的范式,无需 join point、无需代码复制、内联后也无需重新规范化,且易于扩展新的词法作用域效应。文章形式化了 ANF 与 monadic form 的联系及其内涵性质,推导出命令式 ANF,并设计了一条从含 scoped region 的未类型化 λ-演算,经 monadic form,到低层命令式 monadic form 的编译流水线;在该低层形式中 A-规范化是平凡且对区域安全的。作者证明该编译器相对 ANF 保持或优化栈与内存行为,其形式化还重建并系统化了实践(包括生产级编译器)中的务实选择。
A-normal form (ANF) is a widely studied intermediate form in which local control and data flow is made explicit in syntax, and a normal form in which many programs with equivalent control-flow graphs have a single normal syntactic representation. However, ANF is difficult to implement effectively and, as we formalize, difficult to extend with new lexically scoped constructs such as scoped region-based allocation. The problem, as has often been observed, is that normalization of commuting conversions is hard. This traditional view of ANF that normalizing commuting conversions is hard, found in formal models and informed by high-level calculi, is wrong. By studying the low-level intensional aspects of ANF, we can derive a normal form in which normalizing commuting conversion is easy, does not require join points, or code duplication, or renormalization after inlining, and is easily extended with new lexically scoped effects. We formalize the connection between ANF and monadic form and their intensional properties, derive an imperative ANF, and design a compiler pipeline from an untyped λ-calculus with scoped regions, to monadic form, to a low-level imperative monadic form in which A-normalization is trivial and safe for regions. We prove that any such compiler preserves, or optimizes, stack and memory behaviour compared to ANF. Our formalization reconstructs and systematizes pragmatic choices found in practice, including current production-ready compilers. The main take-away from this work is that, in general, monadic form should be preferred over ANF, and A-normalization should only be done in a low-level imperative intermediate form. This maximizes the advantages of each form, and avoids all the standard problems with ANF.