The Calculated Typer

16 January 2025

Zac Garby, Graham Hutton, and Patrick Bahr

In preparation, to submit to ICFP ‘25

Abstract

We present a calculational approach to type checking, showing how type checkers can be derived from behaviour specifications using equational reasoning. In addition, we show how the calculations can be simplified by taking an algebraic approach based on a fusion property, and further improved by taking a constraint-based approach to solving and composing fusion preconditions. We illustrate our methodology with three examples of increasing complexity, starting with a simple expression language, then adding support for exceptions, and finally considering a version of the lambda calculus.