TY - GEN
T1 - Finding Minimum Type Error Sources
AU - Pavlinovic, Zvonimir
AU - King, Tim
AU - Wies, Thomas
N1 - Publisher Copyright:
© 2015 Gesellschaft fur Informatik (GI). All rights reserved.
PY - 2015
Y1 - 2015
N2 - Automatic type inference is a popular feature of functional programming languages. If a program cannot be typed, the compiler reports the first location with a type conflict as the source of the error. However, this is often not the true error source. We present a general algorithm that helps to produce more meaningful type error reports. The algorithm finds all minimum error sources, where the definition of minimum is given by a compiler-specific ranking criterion (e.g. minimizing the program changes needed to fix the error). The 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). This formulation allows us to build on SMT solvers to support rich type systems and, at the same time, abstract from the concrete ranking criterion. We have implemented an instance of our algorithm targeted at OCaml programs. Our evaluation shows that our approach significantly improves upon the quality of type error reports produced by state of the art compilers. This work appeared at OOPSLA 2014 where it won a Best Paper Award.
AB - Automatic type inference is a popular feature of functional programming languages. If a program cannot be typed, the compiler reports the first location with a type conflict as the source of the error. However, this is often not the true error source. We present a general algorithm that helps to produce more meaningful type error reports. The algorithm finds all minimum error sources, where the definition of minimum is given by a compiler-specific ranking criterion (e.g. minimizing the program changes needed to fix the error). The 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). This formulation allows us to build on SMT solvers to support rich type systems and, at the same time, abstract from the concrete ranking criterion. We have implemented an instance of our algorithm targeted at OCaml programs. Our evaluation shows that our approach significantly improves upon the quality of type error reports produced by state of the art compilers. This work appeared at OOPSLA 2014 where it won a Best Paper Award.
UR - http://www.scopus.com/inward/record.url?scp=85134731876&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85134731876&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:85134731876
T3 - Lecture Notes in Informatics (LNI), Proceedings - Series of the Gesellschaft fur Informatik (GI)
SP - 43
EP - 44
BT - Software Engineering and Management 2015
A2 - Assmann, Uwe
A2 - Demuth, Birgit
A2 - Spitta, Thorsten
A2 - Puschel, Georg
A2 - Kaiser, Ronny
PB - Gesellschaft fur Informatik (GI)
T2 - Software Engineering and Management 2015: Multikonferenz der GI-Fachbereiche Softwaretechnik (SWT) und Wirtschaftsinformatik (WI), FA WI-MAW - Software Engineering and Management 2015: Multiconference of the GI Special Interest Groups Software Engineering (SWT) and Information Systems (WI), FA WI-MAW
Y2 - 17 March 2015 through 20 March 2015
ER -