Searching for Type-Error Messages
PLDI 2007
Abstract
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.
Links
- Full text (ACM DL):
- Slides:
- ppt
- Citation:
- BibTeX
- Project page:
- available here
Contact
- Email (essential):
- (first initial + last name) {at} ccs.neu.edu
- Location (likely):
- West Village H, Office 326
- Post (possible):
-
Northeastern University
Khoury College of Computer Sciences
360 Huntington Ave, 2nd floor
Boston, MA 02115
