Total Type Error Localization and Recovery with Holes
summary
Defines a marked lambda calculus that makes every program meaningful by inserting error marks as nonempty holes, gives a total marking procedure (every unmarked term yields a marked term), and mechanizes metatheory in Agda mechanization. Builds a type-hole filling layer that runs constraint-based unification atop a bidirectional core, collects all consistent hole fillings and exposes them as choices; the Hazel implementation offers previews and user selection instead of guessing, with artifacts available and evaluated.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:03Ill-typed code challenges
- 3:26Conventional semantics limits
- 4:28Marked lambda calculus
- 7:59Error marks in typing
- 9:44Formalizing totality
- 11:49Bidirectional and global inference
- 12:51Type holes in Hazel
- 14:38Future directions
- 15:01Q&A
related talks
44mHazel: A Live Functional Programming Environment with Typed Holes
42mSuggesting Valid Substitutions For Typed Holes
32mTotally Live Programming with Hazel (Progress Report)
20mGetting into the Flow: Towards Better Type Error Messages for Constraint-Based ...
29mType Inference Techniques: Implementation and Formalization, Better Together
01h 00mA Type-Safe Structure Editor Calculus + Strictly Capturing Non-Strict Closures
23mError Message Annotation Plugins for Haskell
16mWe’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators