A General Framework for Relational Parametricity

Authors: Kristina Sojakova and Patricia Johann

Paper Information

Title:A General Framework for Relational Parametricity
Authors:Kristina Sojakova and Patricia Johann
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:Theory of Computation, Categorical Semantics, Parametricity

ABSTRACT. Reynolds’ original theory of relational parametricity intended to capture the idea that polymorphically typed System F programs preserve all relations between inputs. But as Reynolds himself later showed, his theory can only be formalized in a meta-theory with an impredicative universe, such as Martin-Löf Type Theory. A number of more abstract treatments of relational parametricity have since appeared; however, as we show, none of these truly generalize Reynolds’ original theory, in the sense of having it as a direct instance. Indeed, they all require certain strictness conditions that Reynolds’ theory does not satisfy. To correct this, we develop an abstract framework for relational parametricity that does deliver Reynolds’ theory as a direct instance in a natural way. This framework is parametric and 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. Moreover, we demonstrate on a concrete example that our notion of parametricity also encompasses proof-relevant parametric models, which does not seem to be the case for the well-known definitions. Our framework is thus both descriptive, in that it accounts for well-known models, and prescriptive, in that it identifies properties that good models of relational parametricity should satisfy. It is constructed using the new notion of a split λ2-fibration with isomorphisms, introduced in this paper, which relaxes certain strictness requirements on split λ2-fibrations. Our main theorem is a generalization of Seely’s classical construction of sound models for System F from split λ2-fibrations: we prove that the canonical model of System F induced by every split λ2-fibration with isomorphisms validates System F’s entire equational theory on the nose, independently of the parameterizing meta-theory.

Talk:Jul 10 12:00 (Session 54E)