Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference

Ishan Bhanuka, Lionel Parreaux, David Binder, Jonathan Immanuel Brachthäuser

TL;DR

The paper introduces HM^ℓ, a flow-based approach to generate type error messages for constraint-based type inference by tracking data-flow provenances through program locations. It formalizes a data-flow model with subtyping constraints, classifies errors into levels based on direction changes, and provides both subtyping-based and unification-based reporting strategies. The authors implement HM^ℓ as an OCaml-compatible extension and evaluate it against OCaml and Helium via a user study, finding limited quantitative gains but qualitative support for flow-based explanations, especially for complex errors. The work demonstrates the potential of data-flow-informed error messages to improve programmer understanding, while highlighting the need for careful presentation and future enhancements, including interactive IDE integrations and handling of additional type-system features.

Abstract

Creating good type error messages for constraint-based type inference systems is difficult. Typical type error messages reflect implementation details of the underlying constraint-solving algorithms rather than the specific factors leading to type mismatches. We propose using subtyping constraints that capture data flow to classify and explain type errors. Our algorithm explains type errors as faulty data flows, which programmers are already used to reasoning about, and illustrates these data flows as sequences of relevant program locations. We show that our ideas and algorithm are not limited to languages with subtyping, as they can be readily integrated with Hindley-Milner type inference. In addition to these core contributions, we present the results of a user study to evaluate the quality of our messages compared to other implementations. While the quantitative evaluation does not show that flow-based messages improve the localization or understanding of the causes of type errors, the qualitative evaluation suggests a real need and demand for flow-based messages.

Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference

TL;DR

The paper introduces HM^ℓ, a flow-based approach to generate type error messages for constraint-based type inference by tracking data-flow provenances through program locations. It formalizes a data-flow model with subtyping constraints, classifies errors into levels based on direction changes, and provides both subtyping-based and unification-based reporting strategies. The authors implement HM^ℓ as an OCaml-compatible extension and evaluate it against OCaml and Helium via a user study, finding limited quantitative gains but qualitative support for flow-based explanations, especially for complex errors. The work demonstrates the potential of data-flow-informed error messages to improve programmer understanding, while highlighting the need for careful presentation and future enhancements, including interactive IDE integrations and handling of additional type-system features.

Abstract

Creating good type error messages for constraint-based type inference systems is difficult. Typical type error messages reflect implementation details of the underlying constraint-solving algorithms rather than the specific factors leading to type mismatches. We propose using subtyping constraints that capture data flow to classify and explain type errors. Our algorithm explains type errors as faulty data flows, which programmers are already used to reasoning about, and illustrates these data flows as sequences of relevant program locations. We show that our ideas and algorithm are not limited to languages with subtyping, as they can be readily integrated with Hindley-Milner type inference. In addition to these core contributions, we present the results of a user study to evaluate the quality of our messages compared to other implementations. While the quantitative evaluation does not show that flow-based messages improve the localization or understanding of the causes of type errors, the qualitative evaluation suggests a real need and demand for flow-based messages.
Paper Structure (62 sections, 10 equations, 26 figures, 1 table)

This paper contains 62 sections, 10 equations, 26 figures, 1 table.

Table of Contents

  1. Introduction
  2. Flow-Based Error Messages
  3. Complex Type Errors
  4. Contributions
  5. Classifying Type Errors
  6. Flow of Types
  7. Change of Direction
  8. Level-0 Errors
  9. Level-1 Errors
  10. Level-2 Errors
  11. Reporting Different Levels
  12. Formalization
  13. Terms and Locations
  14. Syntax of Terms
  15. Types and Provenances
  16. ...and 47 more sections

Figures (26)

  • Figure 1: Simple example of OCaml compiler error message.
  • Figure 2: Simple example of $\textsf{HM}^{\ell}$ error message.
  • Figure 3: Complex example of $\textsf{HM}^{\ell}$ error message.
  • Figure 4: Examples of faulty programs and their corresponding constraint graphs.
  • Figure 5: Level-0 error.
  • ...and 21 more figures

Theorems & Definitions (1)

  • definition 1