The paper introduces type slicing for bidirectional type systems, a theory that explains why expressions have certain types by producing minimal slices of the program sufficient to reproduce queried type information. The metatheory is mechanized in Agda and a linear-time approximation is implemented for the Hazel programming environment.
Background
Type systems are foundational to modern programming languages, but IDEs and compilers only report types without explaining their origin. Bidirectional type checking, as used in languages like Haskell and Agda, combines type synthesis and analysis for better error messages and performance.
- Source
- Lobsters
- Published
- Oct 6, 2026 at 09:36 PM
- Score
- 5.0 / 10