Explaining ML type errors by data flows

Abstract

We present a novel approach to explaining ML type errors: Since the type system inhibits data flows that would abort the program at run-time, our type checker identifies as explanations those data flows that violate the typing rules. It also detects the notorious backflows, which are artifacts of unification, and warns the user about the possibly unexpected typing. The generated explanations comprise a detailed textual description and an arrow overlay to the source code, in which each arrow represents one data flow. The description refers only to elementary facts about program evaluation, not to the type checking process itself. The method integrates well with unification-based type checking: Type-correct programs incur a modest overhead compared to normal type checking. If a type error occurs, a simple depth-first graph traversal yields the explanation. A proof-of-concept implementation is available. © Springer-Verlag Berlin Heidelberg 2005.