Benjamin Lerner

Searching for Type-Error Messages

copyright notice

Benjamin Lerner, Matthew Flower, Dan Grossman, and Craig Chambers

PLDI 2007


Advanced type systems often need some form of type inference to reduce the burden of explicit typing, but type inference often leads to poor error messages for programs that do not type-check. This work pursues a new approach to constructing compilers and presenting type-error messages in which the type-checker itself does not produce the messages. Instead, it is an oracle for a search procedure that finds similar programs that do type-check. Our two-fold goal is to improve error messages while simplifying compiler construction.

Our primary implementation and evaluation is for Caml, a language with full type inference. We also present a prototype for C++ template functions, where type instantiation is implicit. A key extension is making our approach robust even when the program has multiple independent type errors.



download vcard icon
Email (essential):
Location (likely):
West Village H, Office 314
Post (possible):
Northeastern University
College of Computer and Information Science
360 Huntington Ave, 2nd floor
Boston, MA 02115
work Lecturer Office 314