一句话：提出首个评估渐进类型归责策略的方法，并发现多数场景下不精确归责与可证明正确的归责同样有效。
渐进类型语言的归责系统通常由理论研究者设计，并伴随归责定理证明，但实际实现几乎不采用归责机制。这引出了两个问题：归责对程序员是否有价值，以及如何评估归责策略的有效性。本文提出首个归责策略评估方法，并将它应用于三种不同的渐进类型语义。评估从理性程序员视角衡量归责信息在定位类型错误时的帮助。结果显示，在大多数场景中，归责不精确的策略与可证明正确的归责策略对程序员同样有帮助，从而对渐进类型中归责的理论有效性提出了质疑。
Programming language theoreticians develop blame assignment systems and prove blame theorems for gradually typed programming languages. Practical implementations of gradual typing almost completely ignore the idea of blame assignment. This contrast raises the question whether blame provides any value to the working programmer and poses the challenge of how to evaluate the effectiveness of blame assignment strategies. This paper contributes (1) the first evaluation method for blame assignment strategies and (2) the results from applying it to three different semantics for gradual typing. These results cast doubt on the theoretical effectiveness of blame in gradual typing. In most scenarios, strategies with imprecise blame assignment are as helpful to a rationally acting programmer as strategies with provably correct blame.
@article{paperbot1139,
title = {How to evaluate blame for gradual types},
author = {Lukas Lazarek and Ben Greenman and Matthias Felleisen and Christos Dimoulas},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473573}
}