A general framework for relational parametricity

DOI10.1145/3209108.3209141zbMATH Open1497.68126arXiv1805.00067OpenAlexW2963096092MaRDI QIDQ5145366FDOQ5145366

Authors: Kristina Sojakova, Patricia Johann 

Publication date: 20 January 2021

Published in: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1805.00067

Recommendations

• A relationally parametric model of dependent type theory
• Relational parametricity for higher kinds
• Bifibrational functorial semantics of parametric polymorphism
• scientific article; zbMATH DE number 2185651
• Logical relations and parametricity -- a Reynolds programme for category theory and programming languages

zbMATH Keywords

categorical semanticsparametricitySystem F

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Categorical semantics of formal languages (18C50) Functional programming and lambda calculus (68N18)

Cited In (9)

• A fibrational tale of operational logical relations: pure, effectful and differential
• Relational parametricity for higher kinds
• What should a generic object be?
• Title not available (Why is that?)
• Categorical models for Abadi and Plotkin's logic for parametricity
• Title not available (Why is that?)
• Title not available (Why is that?)
• Relational limits in general polymorphism
• Relational Parametricity for Computational Effects

This page was built for publication: A general framework for relational parametricity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145366)