Parametric polymorphism - universally

Ghani, Neil and Nordvall Forsberg, Fredrik and Orsanigo, Federico; de Paiva, Valeria and de Queiroz, Ruy and Moss, Lawrence S. and Leivant, Daniel and de Oliveira, Anjolina G., eds. (2015) Parametric polymorphism - universally. In: Logic, Language, Information, and Computation. Lecture Notes in Computer Science . Springer Berlin/Heidelberg, USA, pp. 81-92. ISBN 978-3-662-47708-3 (https://doi.org/10.1007/978-3-662-47709-0_7)

[thumbnail of Ghani-etal-WoLLIC-2015-Parametric-polymorphism-universally]
Preview
Text. Filename: Ghani_etal_WoLLIC_2015_Parametric_polymorphism_universally.pdf
Accepted Author Manuscript

Download (350kB)| 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) have 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.