SPLASH 2014
Mon 20 - Fri 24 October 2014 Portland, Oregon, United States
Thu 23 Oct 2014 15:52 - 16:15 at Salon E - Debugging Chair(s): Caitlin Sadowski

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 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 built 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.

Video: http://www.infoq.com/presentations/mimimum-type-errors

Finding Minimum Type Error Sources (oopsla2014-pavlinovic.pdf)1.1MiB

Thu 23 Oct

oopsla2014
15:30 - 17:00: OOPSLA - Debugging at Salon E
Chair(s): Caitlin SadowskiGoogle
oopsla2014141407100000015:30 - 15:52
Talk
Dan BarowyUniversity of Massachusetts, Amherst, Dimitar GochevUniversity of Massachusetts, Amherst, Emery BergerUniversity of Massachusetts, Amherst
Link to publication
oopsla2014141407235000015:52 - 16:15
Talk
Zvonimir PavlinovicNew York University, Tim KingNew York University, Thomas WiesNew York University
Link to publication File Attached
oopsla2014141407370000016:15 - 16:37
Talk
Peng LiuPurdue University, Omer TrippIBM Thomas J. Watson Research Center, Xiangyu ZhangPurdue University
Link to publication
oopsla2014141407505000016:37 - 17:00
Talk
Linhai SongUniversity of Wisconsin–Madison, Shan LuUniversity of Chicago
Link to publication