Type Theory With Erasure

TL;DR

This paper introduces a structural version of type theory with erasure, enabling safe removal of irrelevant data during compilation, with formal models, semantics, and an implementation in Agda.

Contribution

It formalizes type theory with erasure as a second-order generalized algebraic theory, providing models, semantics, and a verified implementation.

Findings

Models based on categories with families support erasure semantics.

The theory is conservative over Martin-Löf type theory in both phases.

Constructed a presheaf model for code extraction with correctness proof.

Abstract

Erasure enriches type theory with a distinction between runtime relevant and irrelevant data, allowing the compilation step to safely erase the latter. Versions of this feature are implemented by many systems, including Agda, Idris, and Rocq. We present a structural version of type theory with erasure, formulated as a second-order generalised algebraic theory (SOGAT). Erasure is encoded as a phase distinction between runtime and erased terms, in the form of a proposition that can appear in a context. This formulation has several advantages: it has models based on categories with families, is compatible with other structural features such as staging, and provides a better guideline for implementation. Through the model theory of SOGATs, we study the semantics of type theory with erasure in families of sets, which generalises to any Grothendieck topos equipped with a tiny proposition. We establish conservativity over Martin-L\"of type theory (MLTT) in both phases. For code extraction, we construct a presheaf model that produces untyped lambda calculus programs and prove its correctness through gluing. Our results are formalised in Agda and we provide a toy elaborator implementation.