Blogs >>
SPLASH 2016
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Fri 4 Nov 2016 10:30 - 10:55 at Matterhorn 1 - Typing, in Practice Chair(s): Sebastian Erdweg

Many languages have support for automatic type inference. But when inference
fails, the reported error messages can be unhelpful, highlighting a code
location far from the source of the problem. Several lines of work have emerged
proposing error reports derived from correcting sets: a set of program points
that, when fixed, produce a well-typed program. Unfortunately, these approaches
are tightly tied to specific languages; targeting a new language requires
encoding a type inference algorithm for the language in a custom constraint
system specific to the error reporting tool.

We show how to produce correcting set-based error reports by leveraging existing
type inference implementations, easing the burden of adoption and, as type
inference algorithms tend to be efficient in practice, producing error reports
of comparable quality to similar error reporting tools orders of magnitude
faster. Many type inference algorithms are already formulated as dual phases of
type constraint generation and solving; rather than (re)implementing type
inference in an error explanation tool, we isolate the solving phase and treat
it as an oracle for solving typing constraints. Given any set of typing
constraints, error explanation proceeds by iteratively removing conflicting
constraints from the initial constraint set until discovering a subset on which
the solver succeeds; the constraints removed form a correcting set. Our
approach is agnostic to the semantics of any particular language or type system,
instead leveraging the existing type inference engine to give meaning to
constraints.