paperbot · PL 论文追踪

全部论文 待读 收藏

P2 How to Evaluate Blame for Gradual Types, Part 2

如何评估渐进类型中的 blame,第二部分
ICFP 7(ICFP)2023匹配度 2/10 · 该论文研究渐进类型系统中 blame 与运行时检查对调试渐近类型 veneer 错误的帮助,属于 PL/类型系统与调试方向,但不涉及 AI/LLM、静态分析/形式化验证、浮点程序分析或贝叶斯程序分析,与用户核心研究画像无直接交集。引用 4 inbox
Lukas Lazarek, Ben Greenman, Matthias Felleisen, Christos Dimoulas
crossref: 2026-09-10

AI 速览

一句话:理性程序员实验表明,运行时检查单独帮助有限,Natural 检查结合 blame 显著提供更优调试提示。

为现有编程语言添加渐进类型系统时,需要为大量已有无类型库提供类型 veneer,使带类型组件能导入库功能并获得类型检查,而无需修改库。程序员在创建这些 veneer 时会犯持久性错误,引发问题。研究问题是:学术界研究的渐进类型系统运行时检查能否帮助程序员调试这类错误。论文采用理性程序员(rational-programmer)评估方法,比较运行时检查、底层语言安全检查以及 Natural 运行时检查与 blame 组合的效果。结果表明,仅靠运行时检查通常不如底层语言安全检查有帮助;但将 Natural 运行时检查与 blame 结合能提供显著更优的调试提示。

问题
为无类型库编写渐进类型 veneer 时,程序员会犯错且难以调试;现有运行时检查能否有效辅助调试此类错误尚不明确。
方法
采用理性程序员评估方法,对比不同运行时检查策略(包括底层语言安全检查、Natural 运行时检查,以及带 blame 的组合)对调试的帮助。
评估
通过理性程序员实验发现,单独的运行时检查通常不如底层语言安全检查有帮助;而 Natural 运行时检查结合 blame 能显著提供更优的调试提示。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@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}
}