Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
Explaining ML Type Errors by Data Flows
verfasst von : Holger Gast
Erschienen in: Implementation and Application of Functional Languages
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 arrowrepresents 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.