Getting into the Flow: Towards Better Type Error Messages for Constraint-Based ...
summary
Proposes turning constraint-generation into explicit data flows by attaching provenances (sequences of source locations) to algebraic subtyping constraints, then running a second unification pass to detect conflicts and render error traces; implements the idea as hmlloc/hmloc (code and artifacts available) and supports products, functions, records and let-polymorphism. Categorizes errors by complexity (e.g. level-one vs level-two errors), compares against OCamL and Helium with 120 participants (one participant per system) and finds no quantitative win but positive qualitative feedback and clear directions for refinement.
AI-written summary · about
chapters (12)
- 0:00Better type error messages
- 1:17Type error limitations
- 2:20Data flow error messages
- 3:47Project goals and error types
- 5:10Algebraic subtyping insight
- 6:36Typing rules and constraints
- 9:03Unification pass and errors
- 10:29User study results
- 12:41Recommendations and future work
- 13:43Related work
- 14:24Accomplishments and questions
- 14:52Q&A
related talks
38mType System Foundations for Super-Charged Semantic Code Search
28mA Deepdive Into Flow
21mTotal Type Error Localization and Recovery with Holes
29mType Inference Techniques: Implementation and Formalization, Better Together
17mThis will flow your mind
44mInitiatory Journey from Exceptions to Composable Error Types
24mCode Generation via Meta-programming in Dependently Typed Proof Assistants
38mLiving with Spec