静态类型错误的动态见证（或者，错误类型的程序通常出错）
Dynamic Witnesses for Static Type Errors (or, Ill-Typed Programs Usually Go Wrong)
摘要：
静态类型错误是类型化函数式语言新手的常见绊脚石。我们提出了一个动态的方法来解释类型错误，通过生成反例证人输入，说明了一个病态的程序出错。首先，给定一个病态类型的函数，我们象征性地执行主体来合成使程序出错的见证值。我们证明，我们的程序合成一般的证人，如果一个证人被发现，那么对于所有居住的输入类型，存在的值，可以使功能出错。其次，我们将展示如何扩展此过程，以产生一个约简图，可用于交互式可视化和调试见证执行。第三，我们评估了我们的方法在两个数据集上的覆盖率，这两个数据集包括4,500多个不良类型的学生项目。我们的技术能够为大约85%的程序生成证人，我们的约简图为超过80%的证人生成小反例，并且一个简单的启发式算法允许我们使用证人以大约70%的准确率找到类型错误的来源。最后，我们评估我们的证人是否帮助学生理解和修复类型错误，并发现与我们的证人提出的学生显示出更大的理解类型错误比那些提出了一个标准的错误信息。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
