TY - GEN
T1 - Finding minimum type error sources
AU - Pavlinovic, Zvonimir
AU - King, Tim
AU - Wies, Thomas
PY - 2014/10/15
Y1 - 2014/10/15
N2 - 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.
AB - 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.
KW - Diagnostics
KW - Satisfiability modulo theories
KW - Type errors
UR - http://www.scopus.com/inward/record.url?scp=84908298791&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84908298791&partnerID=8YFLogxK
U2 - 10.1145/2660193.2660230
DO - 10.1145/2660193.2660230
M3 - Conference contribution
AN - SCOPUS:84908298791
T3 - Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA
SP - 525
EP - 542
BT - Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA
PB - Association for Computing Machinery
T2 - 2014 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2014
Y2 - 20 October 2014 through 24 October 2014
ER -