A general framework for relational parametricity

Kristina Sojakova, Patricia Johann

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

Reynolds' original theory of relational parametricity was intended to capture the observation that polymorphically typed System F programs preserve all relations between inputs. But as Reynolds himself later showed, his theory can only be formulated in a metatheory with an impredicative universe, such as the Calculus of Inductive Constructions. A number of more abstract treatments of relational parametricity have since appeared; however, as we show, none of these seem to express Reynolds' original theory in a satisfactory way. To correct this, we develop an abstract framework for relational parametricity that delivers a model expressing Reynolds' theory in a direct and natural way. This framework is uniform with respect to a choice of meta-theory, which allows us to obtain the well-known PER model of Longo and Moggi as a direct instance in a natural way as well. Underlying the framework is the novel notion of a 2-fibration with isomorphisms, which relaxes certain strictness requirements on split 2-fibrations. Our main theorem is a generalization of Seely's classical construction of sound models of System F from split 2-fibrations: we prove that the canonical interpretation of System F induced by every 2-fibration with isomorphisms validates System F's entire equational theory on the nose, independently of the parameterizing meta-theory. Moreover, we offer a novel relationally parametric model of System F (after Orsanigo), which is proof-relevant in the sense that witnesses of relatedness are themselves suitably related. We show that, unlike previous frameworks for parametricity, ours recognizes this new model in a natural way. Our framework is thus descriptive, in that it accounts for well-known models, as well as prescriptive, in that it identifies abstract properties that good models of relational parametricity should satisfy and suggests new constructions of such models.
Original languageEnglish
Title of host publicationProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages869-878
ISBN (Electronic)9781450355834
DOIs
Publication statusPublished - 9 Jul 2018
Externally publishedYes
Event33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 - Oxford, United Kingdom
Duration: 9 Jul 201812 Jul 2018

Publication series

NameProceedings - Symposium on Logic in Computer Science
ISSN (Print)1043-6871

Conference

Conference33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
Country/TerritoryUnited Kingdom
CityOxford
Period9/07/1812/07/18

Funding

Acknowledgments This research is supported by NSF awards 1420175 and 1545197. We thank Steve Awodey and Peter Dybjer for helpful discussions.

FundersFunder number
National Science Foundation1545197
Directorate for Computer and Information Science and Engineering1420175

    Fingerprint

    Dive into the research topics of 'A general framework for relational parametricity'. Together they form a unique fingerprint.

    Cite this