一句话：提出为静态类型错误合成反例见证输入，证明病态程序通常会出错，并用归约图和用户研究辅助调试。
静态类型错误是类型化函数式语言新手常遇到的障碍。本文提出动态解释方法：对类型不正确的函数体进行符号执行，合成能说明程序如何出错的反例见证输入。作者证明该方法生成通用见证：若找到见证，则对所有可居留输入类型，都存在使函数出错的值；并扩展为归约图以交互式可视化、调试见证执行。作者在含 4500 多个类型错误学生程序的两个数据集上评估：约 85% 的程序可生成见证，超过 80% 的见证得到小反例，简单启发式定位错误源准确率约 70%。用户研究显示，见证能帮助学生更好理解类型错误。
Abstract Static type errors are a common stumbling block for newcomers to typed functional languages. We present a dynamic approach to explaining type errors by generating counterexample witness inputs that illustrate how an ill-typed program goes wrong. First, given an ill-typed function, we symbolically execute the body to synthesize witness values that make the program go wrong. We prove that our procedure synthesizes general witnesses in that if a witness is found, then for all inhabited input types, there exist values that can make the function go wrong. Second, we show how to extend this procedure to produce a reduction graph that can be used to interactively visualize and debug witness executions. Third, we evaluate the coverage of our approach on two data sets comprising over 4,500 ill-typed student programs. Our technique is able to generate witnesses for around 85% of the programs, our reduction graph yields small counterexamples for over 80% of the witnesses, and a simple heuristic allows us to use witnesses to locate the source of type errors with around 70% accuracy. Finally, we evaluate whether our witnesses help students understand and fix type errors, and find that students presented with our witnesses show a greater understanding of type errors than those presented with a standard error message.
@article{paperbot331,
title = {Dynamic witnesses for static type errors (or, Ill-Typed Programs Usually Go Wrong)},
author = {ERIC L. SEIDEL and RANJIT JHALA and WESTLEY WEIMER},
journal = {Journal of Functional Programming},
volume = {28},
year = {2018},
doi = {10.1017/s0956796818000126}
}