LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Past Seminars
Improving Type Error Localization for Languages with Type Inference
- Date
- Tuesday, June 27 2017 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Thomas Wies (New York University)
Static type inference as found in programming languages such as OCaml and Haskell is a prime example of a language feature that can boost productivity but that can also be a usability nightmare. A type inference algorithm infers the types of expressions in a program based on how these expressions are used. The compiler can then use the inferred types to prove strong static correctness guarantees about a program without requiring any explicit type annotations. On the other hand, automated type inference can also be counterproductive. If a conflicting use of an expression (i.e. a type mismatch) is detected, the compiler reports the corresponding program location as the source of the type error. However, the actual error source is often elsewhere in the program. This can result in confusing error messages. The programmer needs to understand the basic workings of the inference algorithm to interpret the error message correctly and debug the program. This debugging process is often laborious and the lack of better error localization steepens the learning curve for programmers learning the language.
In this talk, I will present a new algorithm for localizing type errors that provides formal quality guarantees about the identified type error sources. The algorithm works efficiently in practice and has the potential to significantly improve the quality of type error reports produced by state-of-the-art compilers.