TY - GEN
T1 - A general framework for relational parametricity
AU - Sojakova, Kristina
AU - Johann, Patricia
PY - 2018/7/9
Y1 - 2018/7/9
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85051139210&partnerID=8YFLogxK
U2 - 10.1145/3209108.3209141
DO - 10.1145/3209108.3209141
M3 - Conference contribution
T3 - Proceedings - Symposium on Logic in Computer Science
SP - 869
EP - 878
BT - Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
Y2 - 9 July 2018 through 12 July 2018
ER -