Deriving Type Checkers

The relationship between a type system’s specification and the implementation of the type checker is a recurring issue when writing compilers for programming languages and it is an ongoing question if – and if so, how – the formal description of a type system can be used to support the compiler writer when implementing the type checking phase. In this paper we propose type systems formalized by constraintbased inference rules to form an ideal abstraction to accomplish the task of automatically deriving type checking functionality from them. We develop a set of algorithms employing the constraint-based flavor of the rules to perform type checks and present the design and implementation of a Haskell library utilizing these algorithms to provide functionality for the type checking phase based on the chosen abstraction