一句话：提出标记 lambda 演算，首次形式化完全类型错误定位与恢复，并在 Hazel 中实现无无意义编辑器状态的实时环境。
现有类型系统通常只定义良类型表达式，使错误表达式在形式上无意义，难以支持需同时定位错误并继续提供服务的语言服务器。本文提出标记 lambda 演算，首次形式化完全类型错误定位与恢复：带标记错误被视作非空洞，并定义任意表达式的全标记化过程。该演算为渐进双向类型系统，定位依据局部信息流可预测；约束求解作为类型洞填充层，将不一致合一约束的错误限定在类型/表达式洞，并用追踪来源识别不可填充洞。作者在 Agda 中机械化元理论，并在 Hazel 实时函数式编程环境中实现，使用户可选择部分一致的洞填充来交互移动错误，避免无意义编辑器状态。
Type systems typically only define the conditions under which an expression is well-typed, leaving ill-typed expressions formally meaningless. This approach is insufficient as the basis for language servers driving modern programming environments, which are expected to recover from simultaneously localized errors and continue to provide a variety of downstream semantic services. This paper addresses this problem, contributing the first comprehensive formal account of total type error localization and recovery: the marked lambda calculus. In particular, we define a gradual type system for expressions with marked errors, which operate as non-empty holes, together with a total procedure for marking arbitrary unmarked expressions. We mechanize the metatheory of the marked lambda calculus in Agda and implement it, scaled up, as the new basis for Hazel, a full-scale live functional programming environment with, uniquely, no meaningless editor states. The marked lambda calculus is bidirectionally typed, so localization decisions are systematically predictable based on a local flow of typing information. Constraint-based type inference can bring more distant information to bear in discovering inconsistencies but this notoriously complicates error localization. We approach this problem by deploying constraint solving as a type-hole-filling layer atop this gradual bidirectionally typed core. Errors arising from inconsistent unification constraints are localized exclusively to type and expression holes, i.e., the system identifies unfillable holes using a system of traced provenances, rather than localized in an ad hoc manner to particular expressions. The user can then interactively shift these errors to particular downstream expressions by selecting from suggested partially consistent type hole fillings, which returns control back to the bidirectional system. We implement this type hole inference system in Hazel.
@article{paperbot2586,
title = {Total Type Error Localization and Recovery with Holes},
author = {Eric Zhao and Raef Maroof and Anand Dukkipati and Andrew Blinn and Zhiyi Pan and Cyrus Omar},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632910}
}