Type-Safe Tree Transformations for Precisely-Typed Compilers

Abstract

Compilers translate programs from a source language to a target language. This can be done by translating into an intermediate tree representation, performing multiple partial transformations on the tree, and translating out. Compiler implementers must choose between encoding transformation invariants with multiple tree types at the cost of code boilerplate and duplication, or forgoing static correctness by using a broad and imprecise tree datatype. This thesis proposes a new approach to writing precisely-typed compilers and tree transformations without code boilerplate or duplication. The approach requires encoding the tree nodes using two type indices, one for the phase of the root node and another for the phase of all children nodes. This tree datatype can represent partially transformed nodes, and distinguish between trees of different phases. In order to make this approach possible it was necessary to modify the Scala type checker to better infer types in ‘match’-expressions. Precisely-typed tree transformations make use of the default case of a ‘match’-expression; this case must be elaborated to a type which is the type difference of the scrutinee expression and all previously matched patterns. We demonstrate the viability of this approach by implementing a case study for a precisely-typed compiler for the instructional language Lacs. This case study modifies the existing implementation of Lacs to track which subset of tree nodes may be present before and after any given tree transformation. We show that this approach can increase static correctness without the burden of additional code boilerplate or duplication.