Universal properties for universal types in bifibrational parametricity

Research output: Contribution to journalArticle

Abstract

In the 1980s, John Reynolds postulated that a parametrically polymorphic function is an ad-hoc polymorphic function satisfying a uniformity principle. This allowed him to prove that his set-theoretic semantics has a relational lifting which satisfies the Identity Extension Lemma and the Abstraction Theorem. However, his definition (and subsequent variants) has only been given for specific models. In contrast, we give a model-independent axiomatic treatment by characterising Reynolds’ definition via a universal property, and show that the above results follow from this universal property in the axiomatic setting.
LanguageEnglish
Pages810–827
Number of pages18
JournalMathematical Structures in Computer Science
Volume29
Issue number6
Early online date22 Mar 2019
DOIs
Publication statusPublished - 30 Jun 2019

Fingerprint

Uniformity
Lemma
Semantics
Theorem
Model
Abstraction

Keywords

  • categorical semantics
  • comprehension categories
  • relational parametricity

Cite this

@article{9621be5730ca48868fff827b12ce21bd,
title = "Universal properties for universal types in bifibrational parametricity",
abstract = "In the 1980s, John Reynolds postulated that a parametrically polymorphic function is an ad-hoc polymorphic function satisfying a uniformity principle. This allowed him to prove that his set-theoretic semantics has a relational lifting which satisfies the Identity Extension Lemma and the Abstraction Theorem. However, his definition (and subsequent variants) has only been given for specific models. In contrast, we give a model-independent axiomatic treatment by characterising Reynolds’ definition via a universal property, and show that the above results follow from this universal property in the axiomatic setting.",
keywords = "categorical semantics, comprehension categories, relational parametricity",
author = "Neil Ghani and {Nordvall Forsberg}, Fredrik and Federico Orsanigo",
year = "2019",
month = "6",
day = "30",
doi = "10.1017/S0960129518000336",
language = "English",
volume = "29",
pages = "810–827",
journal = "Mathematical Structures in Computer Science",
issn = "0960-1295",
number = "6",

}

Universal properties for universal types in bifibrational parametricity. / Ghani, Neil; Nordvall Forsberg, Fredrik; Orsanigo, Federico.

In: Mathematical Structures in Computer Science, Vol. 29, No. 6, 30.06.2019, p. 810–827.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Universal properties for universal types in bifibrational parametricity

AU - Ghani, Neil

AU - Nordvall Forsberg, Fredrik

AU - Orsanigo, Federico

PY - 2019/6/30

Y1 - 2019/6/30

N2 - In the 1980s, John Reynolds postulated that a parametrically polymorphic function is an ad-hoc polymorphic function satisfying a uniformity principle. This allowed him to prove that his set-theoretic semantics has a relational lifting which satisfies the Identity Extension Lemma and the Abstraction Theorem. However, his definition (and subsequent variants) has only been given for specific models. In contrast, we give a model-independent axiomatic treatment by characterising Reynolds’ definition via a universal property, and show that the above results follow from this universal property in the axiomatic setting.

AB - In the 1980s, John Reynolds postulated that a parametrically polymorphic function is an ad-hoc polymorphic function satisfying a uniformity principle. This allowed him to prove that his set-theoretic semantics has a relational lifting which satisfies the Identity Extension Lemma and the Abstraction Theorem. However, his definition (and subsequent variants) has only been given for specific models. In contrast, we give a model-independent axiomatic treatment by characterising Reynolds’ definition via a universal property, and show that the above results follow from this universal property in the axiomatic setting.

KW - categorical semantics

KW - comprehension categories

KW - relational parametricity

U2 - 10.1017/S0960129518000336

DO - 10.1017/S0960129518000336

M3 - Article

VL - 29

SP - 810

EP - 827

JO - Mathematical Structures in Computer Science

T2 - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

SN - 0960-1295

IS - 6

ER -