Internalizing Representation Independence with Univalence

TL;DR

This paper introduces a method to internalize representation independence in dependently-typed programming languages using univalence and higher inductive types, enabling internal correctness proofs for complex implementations.

Contribution

It develops techniques for establishing internal relational representation independence in dependent type theory using higher inductive types and univalence, extending previous external guarantees.

Findings

Formalized in Cubical Agda with univalence support

Applied to matrices, queues, and multisets

Achieved internal equality of implementations via univalence

Abstract

In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our programming language is dependently-typed, however, we would like to appeal to such invariance results within the language itself, in order to obtain correctness theorems for complex implementations by transferring them from simpler, related implementations. Recent work in proof assistants has shown that Voevodsky's univalence principle allows transferring theorems between isomorphic types, but many instances of representation independence in programming involve non-isomorphic representations. In this paper, we develop techniques for establishing internal relational representation independence results in dependent type theory, by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. We illustrate our techniques by considering applications to matrices, queues, and finite multisets. Our results are all formalized in Cubical Agda, a recent extension of Agda which supports univalence and higher inductive types in a computationally well-behaved way.