Counter-factual typing for debugging type errors
Counter-factual typing for debugging type errors
复制标题
用于调试类型错误的反事实类型
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Martin Erwig
中科院分区：
文献类型：
--
作者：
Sheng Chen;Martin Erwig
修改程序以响应类型错误在现代软件开发中起着重要的作用。然而，生成好的类型错误消息仍然是高表达类型系统的一个问题。现有的方法往往在定位错误和提出补救措施方面缺乏准确性。具体地说，它们要么无法一致地定位类型错误的源，要么报告了太多的潜在错误位置。此外，提供的更改建议往往是不正确的。这使得调试过程乏味且无效。我们提出了一种方法来解决类型调试的问题，它是基于生成和过滤一组全面的类型更改建议。具体来说，我们生成所有（程序结构保留）类型更改，可能会修复类型错误。这些建议将以迭代的方式排列并呈现给程序员。在某些情况下，我们还提出建议，以改变计划。在大多数情况下，这种策略可以快速提供正确的更改建议，同时不会错过任何罕见的建议。类型改变建议的潜在巨大集合的计算是高效的，因为它基于变分类型推断算法，该算法仅对具有变化的程序进行一次类型检查，有效地重用共享部分的类型信息。我们已经评估了我们的方法，并与以前的方法进行了比较。基于大量的例子从文献中，我们发现，我们的方法优于其他方法，并提供了一个可行的替代方案。
Changing a program in response to a type error plays an important part in modern software development. However, the generation of good type error messages remains a problem for highly expressive type systems. Existing approaches often suffer from a lack of precision in locating errors and proposing remedies. Specifically, they either fail to locate the source of the type error consistently, or they report too many potential error locations. Moreover, the change suggestions offered are often incorrect. This makes the debugging process tedious and ineffective. We present an approach to the problem of type debugging that is based on generating and filtering a comprehensive set of type-change suggestions. Specifically, we generate all (program-structure-preserving) type changes that can possibly fix the type error. These suggestions will be ranked and presented to the programmer in an iterative fashion. In some cases we also produce suggestions to change the program. In most situations, this strategy delivers the correct change suggestions quickly, and at the same time never misses any rare suggestions. The computation of the potentially huge set of type-change suggestions is efficient since it is based on a variational type inference algorithm that type checks a program with variations only once, efficiently reusing type information for shared parts. We have evaluated our method and compared it with previous approaches. Based on a large set of examples drawn from the literature, we have found that our method outperforms other approaches and provides a viable alternative.