A practical framework for type inference error explanation
| Autor: | Calvin Loncaric, Manu Sridharan, Cole Schlesinger, Satish Chandra |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Adaptive neuro fuzzy inference system
Theoretical computer science Computer science Semantics (computer science) Inference Type inference 020207 software engineering 0102 computer and information sciences 02 engineering and technology Solver Semantics 01 natural sciences Oracle Set (abstract data type) Constraint (information theory) 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering |
| Zdroj: | OOPSLA |
| DOI: | 10.1145/2983990.2983994 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|