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 (Print)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

Other

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

Fingerprint

Functional programming
Surface mount technology
Error correction
Computer programming languages
Concretes

Keywords

  • Diagnostics
  • Satisfiability modulo theories
  • Type errors

ASJC Scopus subject areas

  • Software

Cite this

Pavlinovic, Z., King, T., & Wies, T. (2014). Finding minimum type error sources. In Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA (pp. 525-542). Association for Computing Machinery. https://doi.org/10.1145/2660193.2660230

Finding minimum type error sources. / Pavlinovic, Zvonimir; King, Tim; Wies, Thomas.

Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA. Association for Computing Machinery, 2014. p. 525-542.

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

Pavlinovic, Z, King, T & Wies, T 2014, Finding minimum type error sources. in Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA. Association for Computing Machinery, pp. 525-542, 2014 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2014, Portland, United States, 10/20/14. https://doi.org/10.1145/2660193.2660230
Pavlinovic Z, King T, Wies T. Finding minimum type error sources. In Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA. Association for Computing Machinery. 2014. p. 525-542 https://doi.org/10.1145/2660193.2660230
Pavlinovic, Zvonimir ; King, Tim ; Wies, Thomas. / Finding minimum type error sources. Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA. Association for Computing Machinery, 2014. pp. 525-542
@inproceedings{efe7298e74854fe19bd40beb0e7929bd,
title = "Finding minimum type error sources",
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.",
keywords = "Diagnostics, Satisfiability modulo theories, Type errors",
author = "Zvonimir Pavlinovic and Tim King and Thomas Wies",
year = "2014",
month = "10",
day = "15",
doi = "10.1145/2660193.2660230",
language = "English (US)",
isbn = "9781450325851",
pages = "525--542",
booktitle = "Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA",
publisher = "Association for Computing Machinery",

}

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

SN - 9781450325851

SP - 525

EP - 542

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

PB - Association for Computing Machinery

ER -