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]
Text. Filename: Ghani_etal_MSCS_2019_Universal_properties_for_universal_types_in_bifibrational.pdf
Accepted Author Manuscript

Download (394kB)| Preview


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.