Type Checking Program Generators Using the Record Calculus Seminars/Workshops

Abstract

Program Generation (PG) is about writing programs that write programs. A program generator composes various pieces of code to construct a new program. An important challenge of PG that has been studied widely is how to ensure that a generator will produce type-safe code. We address the same problem by showing that record calculus can be used to obtain a type system for program generation. We first show that operational semantics of record calculus and program generation are equivalent, and that a record type system can be used to type-check program generators. We also show that this is true in the presence of expressions with side-effects. The record type system yields a type system that is equal to Kim, Yi and Calcagno's staged type system. We then make use of an already-existing record calculus feature, subtyping, to extend the program generation type system with subtyping constraints. As a result, we obtain a very expressive type system to statically guarantee that a generator will produce type-safe code. We state and prove the theorems based on an ML-like language with program generation constructs.