Finding minimum type error sources

Zvonimir Pavlinovic, Tim King, Thomas Wies

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationProceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA
PublisherAssociation for Computing Machinery
Pages525-542
Number of pages18
ISBN (Electronic)9781450325851
DOIs
StatePublished - Oct 15 2014
Event2014 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2014 - Portland, United States
Duration: Oct 20 2014Oct 24 2014

Publication series

NameProceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA

Other

Other2014 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2014
Country/TerritoryUnited States
CityPortland
Period10/20/1410/24/14

Keywords

  • Diagnostics
  • Satisfiability modulo theories
  • Type errors

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Finding minimum type error sources'. Together they form a unique fingerprint.

Cite this