Document Type
Article
Publication Date
1-5-2024
Journal Title
Proceedings of the ACM on Programming Languages
Volume Number
8
Issue Number
POPL
First Page
2340
Last Page
2369
DOI
https://doi.org/10.1145/3632920
Version
Publisher PDF: the final published version of the article, with professional formatting and typesetting
Creative Commons License
This work is licensed under a CC BY License.
Disciplines
Mathematics
Abstract
Parametricity is a property of the syntax of type theory implying, e.g., that there is only one function having the type of the polymorphic identity function. Parametricity is usually proven externally, and does not hold internally. Internalising it is difficult because once there is a term witnessing parametricity, it also has to be parametric itself and this results in the appearance of higher dimensional cubes. In previous theories with internal parametricity, either an explicit syntax for higher cubes is present or the theory is extended with a new sort for the interval. In this paper we present a type theory with internal parametricity which is a simple extension of Martin-Löf type theory: there are a few new type formers, term formers and equations. Geometry is not explicit in this syntax, but emergent: the new operations and equations only refer to objects up to dimension 3. We show that this theory is modelled by presheaves over the BCH cube category. Fibrancy conditions are not needed because we use span-based rather than relational parametricity. We define a gluing model for this theory implying that external parametricity and canonicity hold. The theory can be seen as a special case of a new kind of modal type theory, and it is the simplest setting in which the computational properties of higher observational type theory can be demonstrated.
Digital USD Citation
Altenkirch, Thorsten; Chamoun, Yorgo; Kaposi, Ambrus; and Shulman, Michael, "Internal Parametricity, without an Interval" (2024). Mathematics: Faculty Scholarship. 9.
https://digital.sandiego.edu/mathematics-faculty/9
