一句话：为 ML 系语言提出可选择性未装箱数据构造器，并给出拒绝表示混淆的静态分析与终止性判定算法。
论文为 ML 家族语言提出“未装箱数据构造器”特性：允许选择性让某些构造器在运行时被编译掉，仅保留其参数上的恒等表示，从而兼顾效率与安全。难点在于不同值可能具有相同表示，因此必须静态拒绝危险的未装箱请求。作者给出所需静态分析，在 OCaml 中实现原型，并讨论与 Guarded Algebraic Datatypes 等特性的交互。该分析需展开递归类型定义，不一定规范化，核心可归约为带递归的一阶 λ 演算项规范化。作者提出归约过程中即时检测非终止的算法，证明其正确性与完备性，并指出它与 cpp 预处理器宏展开策略密切相关。
We propose a new language feature for ML-family languages, the ability to selectively unbox certain data constructors, so that their runtime representation gets compiled away to just the identity on their argument. Unboxing must be statically rejected when it could introduce confusion, that is, distinct values with the same representation. We discuss the use-case of big numbers, where unboxing allows to write code that is both efficient and safe, replacing either a safe but slow version or a fast but unsafe version. We explain the static analysis necessary to reject incorrect unboxing requests. We present our prototype implementation of this feature for the OCaml programming language, discuss several design choices and the interaction with advanced features such as Guarded Algebraic Datatypes. Our static analysis requires expanding type definitions in type expressions, which is not necessarily normalizing in presence of recursive type definitions. In other words, we must decide normalization of terms in the first-order λ -calculus with recursion. We provide an algorithm to detect non-termination on-the-fly during reduction, with proofs of correctness and completeness. Our algorithm turns out to be closely related to the normalization strategy for macro expansion in the cpp preprocessor.
@article{paperbot2653,
title = {Unboxed Data Constructors: Or, How cpp Decides a Halting Problem},
author = {Nicolas Chataing and Stephen Dolan and Gabriel Scherer and Jeremy Yallop},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632893}
}