Universal properties for universal types in bifibrational parametricity

Ghani, Neil and Nordvall Forsberg, Fredrik and Orsanigo, Federico (2019) Universal properties for universal types in bifibrational parametricity. Mathematical Structures in Computer Science, 29 (6). 810–827. ISSN 1469-8072 (https://doi.org/10.1017/S0960129518000336)

[thumbnail of Ghani-etal-MSCS-2019-Universal-properties-for-universal-types-in-bifibrational]
Preview
 Text. Filename: Ghani_etal_MSCS_2019_Universal_properties_for_universal_types_in_bifibrational.pdf
Accepted Author Manuscript
Download (394kB)| Preview

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.

CORE (COnnecting REpositories)