Met-Rec: A Type-System for Staged Meta-Programming of Recursive Types

Isaac Oscar Gariano​
Victoria University Wellington

Meta-programming can automate labour-intensive tasks such as generating boiler-plate code or creating an interface to an external data source. Staging is a form of meta-programming: a program is not simply compiled and then run, instead a “stage” is executed, which may cause code to be generated, which may then be executed by subsequent “stages”.

Meta-programming can be challenging in statically typed languages: the appropriate type annotations of generated code may not be statically known, or they may refer to types that don't exist yet. A simple and flexible way of using staging with such languages is to only type-check a stage immediately before it is run: the first “stage” containing code to construct types and programs will be type-checked and then run, the second “stage” containing the generated code will then also be type-checked and run.

Met-Rec supports stage-based meta-programming, and provides a let-recursive expression to construct nominal/isorecursive and structural/equirecursive types. Met-Rec ensures that the construction of types is safe: code cannot name types that will never exist, a type will not be improperly used before it has been fully constructed, and meaningless recursive types of the form “T = T” cannot be defined.