Compiling Programs with Erased Univalence

Compiling Programs with Erased Univalence
Andreas Abel, Nils Anders Danielsson and Andrea Vezzosi
Draft, 2021. [pdf, extended version, highlighted Agda code, zip file with code]

Abstract

We present a variant of cubical type theory with an erasure modality to mark data that should be erased by compilers. In this variant glue types—used to prove univalence—as well as higher constructors may only be used in compile-time code. We show, under certain assumptions, that every closed, run-time natural number reduces to the right value after erasure.

We have developed a variant of Cubical Agda based on the ideas presented here, thereby providing what appears to be the first compiler for some variant of cubical type theory, and we present a case study intended to illustrate that the resulting language is useful in practice.