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 *confusions*, 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 lambda-calculus with recursion. We provide an algorithm to detect non-termination on-the-fly during reduction, with proofs of correctness and completeness. Our termination-monitoring algorithm turns out to be closely related to the normalization strategy for macro expansion in the `cpp` preprocessor.

翻译：我们提出一种适用于ML族语言的新语言特性：允许选择性地“解包”某些数据构造器，使其运行时表示被编译为仅保留参数标识。当解包可能导致“混淆”（即不同值具有相同表示）时，该操作必须被静态拒绝。我们讨论大数场景的应用——解包允许编写兼具效率与安全性的代码，替代要么安全但慢速、要么快速但不安全的现有方案。我们解释了拒绝错误解包请求所需的静态分析过程，展示了针对OCaml编程语言的该特性原型实现，讨论了若干设计选择以及与保护性代数数据类型等高级特性的交互机制。该静态分析需要在类型表达式中展开类型定义，而当存在递归类型定义时，这一过程未必能归一化——换言之，我们必须判定含递归的一阶λ演算中项的归一化问题。我们提供了一种在归约过程中实时检测非终止性的算法，并给出正确性与完备性证明。有趣的是，此终止监控算法与cpp预处理器的宏展开归一化策略密切相关。