Benjamin Lerner

SEMINAL: Searching for ML Type-Error Messages

copyright notice

Benjamin Lerner, Dan Grossman, and Craig Chambers

ML Workshop 2006


We present a new way to generate type-error messages in a polymorphic, implicitly, and strongly typed language (specifically Caml). Our method separates error-message generation from type-checking by taking a fundamentally new approach: we present to programmers small term-level modifications that cause an ill-typed program to become well-typed. This approach aims to improve feedback to programmers with no change to the underlying type-checker nor the compilation of well-typed programs.

We have added a prototype implementation of our approach to the Objective Caml system by intercepting type-checker error messages and using the type-checker on candidate changes to see if they succeed. This novel front-end architecture naturally decomposes into (1) enumerating local changes to the abstract syntax tree that may remove type errors, (2) searching for places to try the changes, (3) using the type-checker to evaluate the changes, and (4) ranking the changes and presenting them to the user.



download vcard icon
Email (essential):
Location (likely):
Department of Computer Science, Office 309
Post (possible):
work Post-Doctoral Research Associate Brown University / Department of Computer Science / 115 Waterman Street, 4th floor / Providence, RI 02912-1910