一句话:理性程序员实验表明,运行时检查单独帮助有限,Natural 检查结合 blame 显著提供更优调试提示。
为现有编程语言添加渐进类型系统时,需要为大量已有无类型库提供类型 veneer,使带类型组件能导入库功能并获得类型检查,而无需修改库。程序员在创建这些 veneer 时会犯持久性错误,引发问题。研究问题是:学术界研究的渐进类型系统运行时检查能否帮助程序员调试这类错误。论文采用理性程序员(rational-programmer)评估方法,比较运行时检查、底层语言安全检查以及 Natural 运行时检查与 blame 组合的效果。结果表明,仅靠运行时检查通常不如底层语言安全检查有帮助;但将 Natural 运行时检查与 blame 结合能提供显著更优的调试提示。
Equipping an existing programming language with a gradual type system requires two major steps. The first and most visible one in academia is to add a notation for types and a type checking apparatus. The second, highly practical one is to provide a type veneer for the large number of existing untyped libraries; doing so enables typed components to import pieces of functionality and get their uses type-checked, without any changes to the libraries. When programmers create such typed veneers for libraries, they make mistakes that persist and cause trouble. The question is whether the academically investigated run-time checks for gradual type systems assist programmers with debugging such mistakes. This paper provides a first, surprising answer to this question via a rational-programmer investigation: run-time checks alone are typically less helpful than the safety checks of the underlying language. Combining Natural run-time checks with blame, however, provides significantly superior debugging hints.
@article{paperbot1910,
title = {How to Evaluate Blame for Gradual Types, Part 2},
author = {Lukas Lazarek and Ben Greenman and Matthias Felleisen and Christos Dimoulas},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {ICFP},
year = {2023},
doi = {10.1145/3607836}
}