一句话：提出 Lambda Set Specialization，首个不受限特化去函数化技术，并用类型系统与机器化证明支撑。
高阶函数给静态分析与优化编译带来困难，去函数化可将程序转换为语义等价的一阶表示。已有特化去函数化技术会限制函数值的使用方式，迫使实现回退到高开销的动态方案。本文提出 Lambda Set Specialization（LSS），首个不限制函数值使用方式的特化去函数化技术。作者用多态类型系统追踪函数值在程序中的流动，将高阶函数相对于其参数的特化重新表述为类型单态化，并给出简单可处理的类型推断算法；在 Isabelle/HOL 中完成机器化证明，证明推断算法相对类型系统的可靠性与完备性。评估在 MLton/Standard ML、OCaml 与 Morphic 上，LSS 预处理带来最高 6.85x、3.45x 和 78.93x 的运行加速。
Higher-order functions pose a challenge for both static program analyses and optimizing compilers. To simplify the analysis and compilation of languages with higher-order functions, a rich body of prior work has proposed a variety of defunctionalization techniques, which can eliminate higher-order functions from a program by transforming the program to a semantically-equivalent first-order representation. Several modern languages take this a step further, specializing higher-order functions with respect to the functions on which they operate, and in turn allowing compilers to generate more efficient code. However, existing specializing defunctionalization techniques restrict how function values may be used, forcing implementations to fall back on costly dynamic alternatives. We propose lambda set specialization (LSS), the first specializing defunctionalization technique which imposes no restrictions on how function values may be used. We formulate LSS in terms of a polymorphic type system which tracks the flow of function values through the program, and use this type system to recast specialization of higher-order functions with respect to their arguments as a form of type monomorphization. We show that our type system admits a simple and tractable type inference algorithm, and give a formalization and fully-mechanized proof in the Isabelle/HOL proof assistant showing soundness and completeness of the type inference algorithm with respect to the type system. To show the benefits of LSS, we evaluate its impact on the run time performance of code generated by the MLton compiler for Standard ML, the OCaml compiler, and the new Morphic functional programming language. We find that pre-processing with LSS achieves run time speedups of up to 6.85x under MLton, 3.45x for OCaml, and 78.93x for Morphic.
@article{paperbot1947,
title = {Better Defunctionalization through Lambda Set Specialization},
author = {William Brandon and Benjamin Driscoll and Frank Dai and Wilson Berkow and Mae Milano},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591260}
}