Universal properties for universal types in bifibrational parametricity

Research output: Contribution to journalArticle

4 Downloads (Pure)

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.
Original languageEnglish
Pages (from-to)810–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

JF - Mathematical Structures in Computer Science

SN - 0960-1295

IS - 6

ER -