Parametric polymorphism - universally

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

4 Citations (Scopus)

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.
LanguageEnglish
Title of host publicationLogic, Language, Information, and Computation
Subtitle of host publication22nd International Workshop, WoLLIC 2015, Bloomington, IN, USA, July 20-23, 2015, Proceedings
EditorsValeria de Paiva, Ruy de Queiroz, Lawrence S. Moss, Daniel Leivant, Anjolina G. de Oliveira
Pages81-92
Number of pages12
DOIs
Publication statusPublished - 24 Jun 2015
EventWorkshop on Logic, Language and Information (WoLLIC 2015) - Indiana University, Bloomington, IN, United States
Duration: 20 Jul 201523 Jul 2015

Publication series

NameLecture Notes in Computer Science
PublisherSpringer, Heidelberg
Volume9160
ISSN (Print)0302-9743

Conference

ConferenceWorkshop on Logic, Language and Information (WoLLIC 2015)
CountryUnited States
CityBloomington, IN
Period20/07/1523/07/15

Fingerprint

Polymorphism
Semantics

Keywords

  • parametric polymorphism
  • type theory
  • programming

Cite this

Ghani, N., Nordvall Forsberg, F., & Orsanigo, F. (2015). Parametric polymorphism - universally. In V. de Paiva, R. de Queiroz, L. S. Moss, D. Leivant, & A. G. de Oliveira (Eds.), Logic, Language, Information, and Computation: 22nd International Workshop, WoLLIC 2015, Bloomington, IN, USA, July 20-23, 2015, Proceedings (pp. 81-92). (Lecture Notes in Computer Science; Vol. 9160). https://doi.org/10.1007/978-3-662-47709-0_7
Ghani, Neil ; Nordvall Forsberg, Fredrik ; Orsanigo, Federico. / Parametric polymorphism - universally. Logic, Language, Information, and Computation: 22nd International Workshop, WoLLIC 2015, Bloomington, IN, USA, July 20-23, 2015, Proceedings. editor / Valeria de Paiva ; Ruy de Queiroz ; Lawrence S. Moss ; Daniel Leivant ; Anjolina G. de Oliveira. 2015. pp. 81-92 (Lecture Notes in Computer Science).
@inproceedings{dd70f5e5661a4fd3bafc275f70c01190,
title = "Parametric polymorphism - universally",
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.",
keywords = "parametric polymorphism, type theory, programming",
author = "Neil Ghani and {Nordvall Forsberg}, Fredrik and Federico Orsanigo",
note = "The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-47709-0_7",
year = "2015",
month = "6",
day = "24",
doi = "10.1007/978-3-662-47709-0_7",
language = "English",
isbn = "978-3-662-47708-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer, Heidelberg",
pages = "81--92",
editor = "{de Paiva}, Valeria and {de Queiroz}, Ruy and Moss, {Lawrence S.} and Daniel Leivant and {de Oliveira}, {Anjolina G.}",
booktitle = "Logic, Language, Information, and Computation",

}

Ghani, N, Nordvall Forsberg, F & Orsanigo, F 2015, Parametric polymorphism - universally. in V de Paiva, R de Queiroz, LS Moss, D Leivant & AG de Oliveira (eds), Logic, Language, Information, and Computation: 22nd International Workshop, WoLLIC 2015, Bloomington, IN, USA, July 20-23, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9160, pp. 81-92, Workshop on Logic, Language and Information (WoLLIC 2015), Bloomington, IN, United States, 20/07/15. https://doi.org/10.1007/978-3-662-47709-0_7

Parametric polymorphism - universally. / Ghani, Neil; Nordvall Forsberg, Fredrik; Orsanigo, Federico.

Logic, Language, Information, and Computation: 22nd International Workshop, WoLLIC 2015, Bloomington, IN, USA, July 20-23, 2015, Proceedings. ed. / Valeria de Paiva; Ruy de Queiroz; Lawrence S. Moss; Daniel Leivant; Anjolina G. de Oliveira. 2015. p. 81-92 (Lecture Notes in Computer Science; Vol. 9160).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

TY - GEN

T1 - Parametric polymorphism - universally

AU - Ghani, Neil

AU - Nordvall Forsberg, Fredrik

AU - Orsanigo, Federico

N1 - The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-47709-0_7

PY - 2015/6/24

Y1 - 2015/6/24

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) 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.

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) 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.

KW - parametric polymorphism

KW - type theory

KW - programming

UR - http://www.indiana.edu/~iulg/wollic/

UR - http://dx.doi.org/10.1007/978-3-662-47709-0

U2 - 10.1007/978-3-662-47709-0_7

DO - 10.1007/978-3-662-47709-0_7

M3 - Conference contribution book

SN - 978-3-662-47708-3

T3 - Lecture Notes in Computer Science

SP - 81

EP - 92

BT - Logic, Language, Information, and Computation

A2 - de Paiva, Valeria

A2 - de Queiroz, Ruy

A2 - Moss, Lawrence S.

A2 - Leivant, Daniel

A2 - de Oliveira, Anjolina G.

ER -

Ghani N, Nordvall Forsberg F, Orsanigo F. Parametric polymorphism - universally. In de Paiva V, de Queiroz R, Moss LS, Leivant D, de Oliveira AG, editors, Logic, Language, Information, and Computation: 22nd International Workshop, WoLLIC 2015, Bloomington, IN, USA, July 20-23, 2015, Proceedings. 2015. p. 81-92. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-662-47709-0_7