Please note: This master’s thesis presentation will take place in DC 3317.
Pedro Oliveira, Master’s candidate
David R. Cheriton School of Computer Science
Supervisor: Professor Ondřej Lhoták
Compilers translate programs from a source language to a target language. Usually, this is done by translating into an intermediate tree representation, performing multiple partial transformations in 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 checked 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 elaborate 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 didactic language Lacs. This case study modifies the exiting 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.