A Type System for Program Transformations based on Parametric Tree Grammars

Program transformations are an important area of metaprogramming. Compil-ers and preprocessors commonly apply multiple program transformations in a row, using the output of one transformation as input for the next. Thereby, each transformation relies on the output of the preceding transformation to be correct. For example, a C compiler depends on the preprocessor to expand all macro definitions as to be able to process the input. Syntactic extensibility of programming languages exposes the implementation of program transforma-tions to the user, which makes it even more important to specify and check their input and output behavior. Current general-purpose program transformation languages are usually untyped, hence they cannot ensure that the composition of multiple transfor-mations is safe, i.e. does not lead to a runtime error. While there is research in designing type-safe program transformation languages for specific domains like XML, the safety properties of general-purpose program transformation languages have not yet been thoroughly studied. To this end, we develop a core calculus for program transformation languages suited to formally explore the safety properties of program transformations. On top of that calculus, we design a domain-specific type system based on regular tree grammars. The idea is to use tree grammars as types describing the abstract syntax of the manipulated programs. This makes it possible to specify the input and output language of a transformation and hence to check the validity of composite transformations. We show that the type system is expressive enough to ensure the safety of program transformations in our calculus and formally prove its soundness. Furthermore, we extend our calculus and the grammar-based type system with higher-order functions and parametric types. We believe that the resulting language constitutes a solid basis for further research on program transformation languages