PL Seminar: Finding Minimum Type Error Sources
Event details
| Date | 28.05.2014 |
| Hour | 14:00 › 15:00 |
| Speaker |
Zvonimir Pavlinovic (research intern with UC Berkeley Security Group) |
| Location | |
| Category | Conferences - Seminars |
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.
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.
Practical information
- General public
- Free