SEMINAL: Searching for ML Type-Error Messages

Benjamin Lerner, Dan Grossman and Craig Chambers

The 2006 ACM SIGPLAN Workshop on ML (ML 2006)
Portland, Oregon, 16th September 2006

---

Abstract

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.

---

  

START Conference Manager (V2.52.7)

Maintainer: rrgerber@softconf.com