WG211/M8Aktemur
Relating Staged Computation to the Record Calculus
Baris Aktemur
It has been previously shown that there is a close relation between record calculus and program generation (e.g. Lisp-like quasiquotations): A translation has been defined to convert staged expressions to record calculus expressions, and it has been shown that the call-by-value semantics of the staged and the record calculi are equivalent, modulo the translation and admin reductions. This relation has led to the result that a record calculus type system can be used to type-check staged expressions. In this work-in-progess, we investigate the relation further. The contributions are twofold:
(1) We fine-tune the previously found relation between the two operational semantics, and obtain more precise results. In particular, we show that three kinds of admin reductions suffice, and these reductions can be applied exhaustively.
(2) We define a reverse translation that converts record calculus expressions back to the staged calculus, allowing us to go back and forth between the two calculi. As a result, taking a step of evaluation in the staged calculus is equal to first translating the staged expression to a record expression, then taking a step of evaluation in the record calculus followed by exhaustive admin reductions, and finally translating the resulting record expression back to the staged calculus.
We believe that this result is an important step towards reusing already-existing record calculus static analyses
not only type checking
to reason about staged expressions.
