Finding Minimum Type Error Sources

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.  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 type inference to constraint satisfaction.  We then formulate the problem of computing minimum error sources in terms of weighted maximum satisfiability modulo theories (MaxSMT).  Ranking criteria are incorporated by assigning weights to typing constraints.  The reduction to MaxSMT allows us to build on SMT solvers to support rich type systems.  We have implemented an instance of our framework targeted at Hindley-Milner type systems.  We have evaluated our implementation on existing OCaml benchmarks for type error localization and showed that our approach can find minimum error sources subject to useful ranking criteria.

This work was presented at OOPSLA 2014.  This is joint work with Zvonimir Pavlinovic and Thomas Wies.

Bio: Tim King is a post doctoral researcher at Verimag in Grenoble.  He did his PhD under the advisement of Clark Barrett at NYU.  His research focuses on the construction of efficient solvers for the satisfiability modulo theories problem.  He is one of the main developers of the CVC4 satisfiability modulo theories solver and the author of its arithmetic solver.