3 ms·
The Calculated Typer – Haskell Symposium (ICFP⧸SPLASH'25) [video]
- matt_d 1y agoPaper: https://dl.acm.org/doi/10.1145/3759164.3759346 https://dl.acm.org/doi/10.1145/3759164.3759346 Haskell & Agda Code: https://doi.org/10.5281/zenodo.16751639 https://doi.org/10.5281/zenodo.16751639 Abstract: https://bahr.io/pubs/entries/calctyper.html https://bahr.io/pubs/entries/calctyper.html > We present a calculational approach to the design of type checkers, showing how they can be derived from behavioural specifications using equational reasoning. We focus on languages whose semantics can be expressed as a fold, and show how the calculations can be simplified using fold fusion. This approach enables the compositional derivation of correct-by-construction type checkers based on solving and composing fusion preconditions. We introduce our approach using a simple expression language, to which we then add support for exception handling and checked exceptions.