Zero-Cost Coercions for Program and Proof Reuse

TL;DR

This paper presents a method for creating zero-cost coercions between different variants of inductive datatypes, enabling reuse of programs and proofs across types without runtime or proof effort, formalized in the Cedille language.

Contribution

It introduces identity coercions between non-indexed and indexed datatypes, leveraging erasure in Cedille to achieve zero-cost type conversions and proof reuse.

Findings

Enables reuse of vector programs for list implementations without runtime overhead.

Allows reuse of vector proofs for list proofs without additional proof obligations.

Formalized in Cedille, demonstrating practical applicability of zero-cost coercions.

Abstract

We introduce the notion of identity coercions between non-indexed and indexed variants of inductive datatypes, such as lists and vectors. An identity coercion translates one type to another such that the coercion function definitionally reduces to the identity function. This allows us to reuse vector programs to derive list programs (and vice versa), without any runtime cost. This also allows us to reuse vector proofs to derive list proofs (and vice versa), without the cost of equational reasoning proof obligations. Our work is formalized in Cedille, a dependently typed programming language based on a type-annotated Curry-style type the- ory with implicit (or, erased) products (or, dependent functions), and relies crucially on erasure to introduce definitional equalities between underlying untyped terms.