Logical properties of a modality for erasure

Logical properties of a modality for erasure
Nils Anders Danielsson
Draft, 2019. [pdf, highlighted Agda code, zip file with code]

Abstract

This text develops some theory for a type constructor Erased, which turns out to be a modality. Erased is similar to an identity function for types, but values of type Erased A should be erased by the compiler. Special typing rules are used to avoid getting into a situation in which a program has to make a decision based on an erased piece of data, and this arguably makes the theory of Erased more interesting than that of the identity function.

The theory has been formalised in Agda. It is developed based on some assumptions that are satisfied in Cubical Agda, and also in more traditional Agda with the K rule.

The text focuses on the logical properties of Erased, provable inside Agda, rather than external properties related to, say, time or space complexity. One question is when an erased value can be resurrected. In an attempt to shed some light on this question the text develops some theory of two notions of stability, one of which corresponds to the concept of a modal type.

The text includes an example suggesting how the theory can be put to use in practice: a type that is equivalent to the unary natural numbers and computes roughly like the unary natural numbers at compile-time (for some operations), but computes roughly like an arbitrary, possibly efficient implementation of natural numbers at run-time.