Finding minimum type error sources
Finding minimum type error sources
复制标题
寻找最小类型错误源
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Thomas Wies
中科院分区：
文献类型：
--
作者：
Zvonimir Pavlinovic;Tim King;Thomas Wies
自动类型推理是功能编程语言的流行功能。如果无法键入程序，则编译器通常在其错误消息中报告单个程序位置。该位置是类型推理失败的点，但不一定是错误的实际来源。甚至没有考虑其他潜在的错误源。因此，编译器通常会错过真正的错误源，这增加了程序员的调试时间。在本文中，我们提出了一种自动定位类型错误的一般框架。我们的算法找到了所有最小误差源，其中最小的确切定义是根据编译器特定的排名标准给出的。编译器可以使用最小误差源来产生更有意义的错误报告，并进行自动纠正。我们的方法是通过将最小误差源的搜索减少到我们根据加权最大可满足模式理论（MAXSMT）而制定的优化问题来起作用。对加权MAXSMT的减少使我们能够在SMT求解器上构建以支持丰富的类型系统，同时摘要从混凝土标准中摘要，用于对误差源进行排名。我们已经实施了针对Hindley-Milner类型系统的框架实例，并在现有的OCAML基准测试中对其进行了评估，以实现类型错误本地化。我们的评估表明，我们的方法有可能显着提高最先进的编译器所产生的类型错误报告的质量。
Automatic type inference is a popular feature of functional programming languages. If a program cannot be typed, the compiler typically reports a single program location in its error message. This location is the point where the type inference failed, but not necessarily the actual source of the error. Other potential error sources are not even considered. Hence, the compiler often misses the true error source, which increases debugging time for the programmer. In this paper, we present a general framework for automatic localization of type errors. Our algorithm finds all minimum error sources, where the exact definition of minimum is given in terms of a compiler-specific ranking criterion. Compilers can use minimum error sources to produce more meaningful error reports, and for automatic error correction. Our approach works by reducing the search for minimum error sources to an optimization problem that we formulate in terms of weighted maximum satisfiability modulo theories (MaxSMT). The reduction to weighted MaxSMT allows us to build on SMT solvers to support rich type systems and at the same time abstract from the concrete criterion that is used for ranking the error sources. We have implemented an instance of our framework targeted at Hindley-Milner type systems and evaluated it on existing OCaml benchmarks for type error localization. Our evaluation shows that our approach has the potential to significantly improve the quality of type error reports produced by state of the art compilers.