Total Type Error Localization and Recovery with Holes
Total Type Error Localization and Recovery with Holes
复制标题
总类型错误定位和带孔恢复
DOI：
10.1145/3632910
复制
发表时间：
2024
影响因子：
--
通讯作者：
Omar, Cyrus
中科院分区：
文献类型：
--
作者：
Zhao, Eric;Maroof, Raef;Dukkipati, Anand;Blinn, Andrew;Pan, Zhiyi;Omar, Cyrus
类型系统通常只定义表达式是良好类型的条件，而使类型不良的表达式在形式上没有意义。这种方法不足以作为驱动现代编程环境的语言服务器的基础，现代编程环境有望从同时发生的本地化错误中恢复，并继续提供各种下游语义服务。本文解决了这个问题，贡献了第一个全面的正式帐户的总类型错误的定位和恢复：标记lambda演算。特别是，我们为具有标记错误的表达式定义了一个渐进类型系统，这些表达式作为非空洞操作，以及标记任意未标记表达式的完整过程。我们在Agda中机械化标记lambda演算的元理论，并将其实现，扩大规模，作为Hazel的新基础，Hazel是一个完整的活函数式编程环境，具有独特的，没有无意义的编辑器状态。标记lambda演算是双向类型的，因此本地化决策是基于本地类型信息流系统地可预测的。基于约束的类型推断可以在发现不一致时带来更远的信息，但这会使错误定位变得非常复杂。我们解决这个问题，通过部署约束解决作为一个类型洞填充层上这个渐进的双向类型的核心。由不一致的统一约束引起的错误仅局限于类型和表达式漏洞，即，系统使用跟踪出处的系统来识别不可填充的漏洞，而不是以特别的方式局限于特定的表达式。然后，用户可以通过从建议的部分一致类型的孔填充中进行选择来交互地将这些错误转移到特定的下游表达式，这将控制返回到双向系统。我们在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.
登录
查看更多内容
学会责备：通过数据驱动的诊断来定位新手类型错误
DOI：
--
发表时间：
2017
期刊：
Proc. ACM Program. Lang.
影响因子：
--
作者：
Eric L. Seidel;Huma Sibghat;Kamalika Chaudhuri;Westley Weimer;Ranjit Jhala
通讯作者：
Ranjit Jhala
无约束类型错误切片
DOI：
--
发表时间：
2011
期刊：
Symposium on Trends in Functional Programming
影响因子：
--
作者：
Thomas Schilling
通讯作者：
Thomas Schilling
tyler：一个基于图块的小型结构编辑器
DOI：
10.1145/3546196.3550164
发表时间：
2022
期刊：
Proceedings of the 7th ACM SIGPLAN International Workshop on Type-Driven Development
影响因子：
--
作者：
David Moon;Andrew Blinn;Cyrus Omar
通讯作者：
Cyrus Omar
与键入的孔进行实时图案匹配
影响因子：
--
作者：
Yuan, Yongwei;Guest, Scott;Griffis, Eric;Potter, Hannah;Moon, David;Omar, Cyrus
通讯作者：
Omar, Cyrus
DOI：
--
发表时间：
2016
期刊：
ACM-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
M. Cimini;Jeremy G. Siek
通讯作者：
Jeremy G. Siek