Blogs (9) >>
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

Fri 4 Nov

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
Typing, in PracticeOOPSLA at Matterhorn 1
Chair(s): Sebastian Erdweg Delft University of Technology, Netherlands
A Practical Framework for Type Inference Error Explanation
Calvin Loncaric University of Washington, Satish Chandra Samsung Research America, Manu Sridharan Samsung Research America, Cole Schlesinger Samsung Research America
DOI Pre-print Media Attached
Dynamically Diagnosing Type Errors in Unsafe CodeAEC
Stephen Kell University of Cambridge
DOI Media Attached
First-Class Effect Reflection for Effect-Guided Programming
Yuheng Long Iowa State University, Yu David Liu , Hridesh Rajan Iowa State University, USA
Java and Scala's Type Systems are Unsound: The Existential Crisis of Null PointersAEC
Nada Amin EPFL, Ross Tate Cornell University
Link to publication DOI Pre-print