zbMATH — the first resource for mathematics

Parametric polymorphism – universally. (English) Zbl 06484970
Paiva, Valeria (ed.) et al., Logic, language, information, and computation. 22nd international workshop, WoLLIC 2015, Bloomington, IN, USA, July 20–23, 2015. Proceedings. Berlin: Springer (ISBN 978-3-662-47708-3/pbk; 978-3-662-47709-0/ebook). Lecture Notes in Computer Science 9160, 81-92 (2015).
Summary: 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.
For the entire collection see [Zbl 1319.03010].

03B70 Logic in computer science
Full Text: DOI