一句话：提出一种实用的模式系统，静态检测 call-by-value 递归定义中的恶性循环，并成功替换 OCaml 的不健全语法检查。
在 call-by-value 语言中，递归定义可用来构造递归函数或循环数据结构，但如 let rec x = x + 1 这类定义含恶性循环，求值时会运行时失败。本文提出一种新的静态分析来排除此类失败：给出一组声明式推理规则，证明其相对于 Nordlander、Carlsson 和 Gill 的源级语义是可靠的，并说明可按一种异常简单的方式将其导向算法的后向分析检查。该实现已替换 OCaml 原有的脆弱语法检查，后者随语言演化漏掉了若干微妙错误。论文还记录了异常、一等模块、GADT 等真实函数式语言高级特性与递归定义安全检查交互时出现的问题。
In call-by-value languages, some mutually-recursive definitions can be safely evaluated to build recursive functions or cyclic data structures, but some definitions (let rec x = x + 1) contain vicious circles and their evaluation fails at runtime. We propose a new static analysis to check the absence of such runtime failures. We present a set of declarative inference rules, prove its soundness with respect to the reference source-level semantics of Nordlander, Carlsson, and Gill [2008], and show that it can be directed into an algorithmic backwards analysis check in a surprisingly simple way. Our implementation of this new check replaced the existing check used by the OCaml programming language, a fragile syntactic criterion which let several subtle bugs slip through as the language kept evolving. We document some issues that arise when advanced features of a real-world functional language (exceptions in first-class modules, GADTs, etc.) interact with safety checking for recursive definitions.
@article{paperbot1146,
title = {A practical mode system for recursive definitions},
author = {Alban Reynaud and Gabriel Scherer and Jeremy Yallop},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434326}
}