A General Framework for Relational Parametricity

TL;DR

This paper introduces a comprehensive, flexible framework for relational parametricity that encompasses existing models and proposes new categorical models, enhancing understanding and construction of polymorphic type theories.

Contribution

It develops an abstract, general framework for relational parametricity that subsumes Reynolds' original model and introduces two novel categorical models of System F.

Findings

Framework generalizes Reynolds' model within type theory

Includes categorical versions of Reynolds' and proof-relevant models

Recognizes both existing and new models naturally

Abstract

Reynolds' original theory of relational parametricity was 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 the Calculus of Inductive Constructions. Abstracting from Reynolds' ideas, Dunphy and Reddy developed their well-known framework for parametricity that uses parametric limits in reflexive graph categories and aims to subsume a variety of parametric models. As we observe, however, their theory is not sufficiently general to subsume the very model that inspired parametricity, namely Reynolds' original model, expressed inside type theory. To correct this, we develop an abstract framework for relational parametricity that generalizes the notion of a reflexive graph categories and delivers Reynolds' model as a direct instance in a 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. In addition, we offer two novel relationally parametric models of System F: i) a categorical version of Reynolds' model, where types are functorial on isomorphisms and all polymorphic functions respect the functorial action, and ii) a proof-relevant categorical version of Reynolds' model (after Orsanigo), where, additionally, witnesses of relatedness are themselves suitably related. We show that, unlike previously existing frameworks for parametricity, ours recognizes both of these new models 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.