The Marriage of Univalence and Parametricity
- 15 January 2021
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 68 (1), 1-44
- https://doi.org/10.1145/3429979
Abstract
Reasoning modulo equivalences is natural for everyone, including mathematicians. Unfortunately, in proof assistants based on type theory, which are frequently used to mechanize mathematical results and carry out program verification efforts, equality is appallingly syntactic, and as a result, exploiting equivalences is cumbersome at best. Parametricity and univalence are two major concepts that have been explored in the literature to transport programs and proofs across type equivalences, but they fall short of achieving seamless, automatic transport. This work first clarifies the limitations of these two concepts when considered in isolation and then devises a fruitful marriage between both. The resulting concept, called univalent parametricity, is an extension of parametricity strengthened with univalence that fully realizes programming and proving modulo equivalences. Our approach handles both type and term dependency, as well as type-level computation. In addition to the theory of univalent parametricity, we present a lightweight framework implemented in the Coq proof assistant that allows the user to transparently transfer definitions and theorems for a type to an equivalent one, as if they were equal. For instance, this makes it possible to conveniently switch between an easy-to-reason-about representation and a computationally efficient representation as soon as they are proven equivalent. The combination of parametricity and univalence supports transport à la carte: basic univalent transport, which stems from a type equivalence, can be complemented with additional proofs of equivalences between functions over these types, in order to be able to transport more programs and proofs, as well as to yield more efficient terms. We illustrate the use of univalent parametricity on several examples, including a recent integration of native integers in Coq. This work paves the way to easier-to-use proof assistants by supporting seamless programming and proving modulo equivalences.Keywords
Funding Information
- ANID FONDECYT REGULAR project (1190058)
- ANID/CONICYT REDES Project (170067)
- ERC starting (CoqHoTT 637339)
- Inria Équipe Associée GECO
This publication has 23 references indexed in Scilit:
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOLPublished by Springer Science and Business Media LLC ,2013
- Automatic Data RefinementLecture Notes in Computer Science, 2013
- Data Refinement in Isabelle/HOLLecture Notes in Computer Science, 2013
- Proofs for freeJournal of Functional Programming, 2012
- Dependently Typed Programming in AgdaLecture Notes in Computer Science, 2009
- Wellfounded Trees and Dependent Polynomial FunctorsLecture Notes in Computer Science, 2004
- Changing Data Representation within the Coq SystemLecture Notes in Computer Science, 2003
- A coherence theorem for Martin-Löf's type theoryJournal of Functional Programming, 1998
- Parametricity as isomorphismTheoretical Computer Science, 1994
- The calculus of constructionsInformation and Computation, 1988