Staged Compilation with Two-Level Type Theory

TL;DR

This paper demonstrates how two-level type theory (2LTT) can be effectively used for staged compilation with dependent types, providing a correct staging algorithm and establishing strong conservativity over the object theory.

Contribution

It introduces a novel staged compilation approach using 2LTT, including a staging-by-evaluation algorithm and proof of its correctness, supporting full dependent types.

Findings

Staging-by-evaluation technique for 2LTT.

Proof of correctness and conservativity of the staging algorithm.

Supports full dependent types and unrestricted staging.

Abstract

The aim of staged compilation is to enable metaprogramming in a way such that we have guarantees about the well-formedness of code output, and we can also mix together object-level and meta-level code in a concise and convenient manner. In this work, we observe that two-level type theory (2LTT), a system originally devised for the purpose of developing synthetic homotopy theory, also serves as a system for staged compilation with dependent types. 2LTT has numerous good properties for this use case: it has a concise specification, well-behaved model theory, and it supports a wide range of language features both at the object and the meta level. First, we give an overview of 2LTT's features and applications in staging. Then, we present a staging algorithm and prove its correctness. Our algorithm is "staging-by-evaluation", analogously to the technique of normalization-by-evaluation, in that staging is given by the evaluation of 2LTT syntax in a semantic domain. The staging algorithm together with its correctness constitutes a proof of strong conservativity of 2LLT over the object theory. To our knowledge, this is the first description of staged compilation which supports full dependent types and unrestricted staging for types.