Bifibrational functorial semantics of parametric polymorphism

Neil Ghani, Patricia Johann, Fredrik Nordvall Forsberg, Federico Orsanigo, Tim Revell

Research output: Contribution to journalArticle

1 Citation (Scopus)

Abstract

Reynolds' theory of parametric polymorphism captures the invariance of polymorphically typed programs under change of data representation. Semantically, reflexive graph categories and fibrations are both known to give a categorical understanding of parametric polymorphism. This paper contributes further to this categorical perspective by showing the relevance of bifibrations. We develop a bifibrational framework for models of System F that are parametric, in that they verify the Identity Extension Lemma and Reynolds' Abstraction Theorem. We also prove that our models satisfy expected properties, such as the existence of initial algebras and final coalgebras, and that parametricity implies dinaturality.

Fingerprint

Polymorphism
Semantics
Categorical
Invariance
Algebra
Representation of data
Coalgebra
Fibration
Lemma
Verify
Imply
Graph in graph theory
Theorem
Model

Keywords

  • fibred category theory
  • logical relations
  • parametricity
  • system F

Cite this

@article{acc778a193094441bd66d45f772e7e95,
title = "Bifibrational functorial semantics of parametric polymorphism",
abstract = "Reynolds' theory of parametric polymorphism captures the invariance of polymorphically typed programs under change of data representation. Semantically, reflexive graph categories and fibrations are both known to give a categorical understanding of parametric polymorphism. This paper contributes further to this categorical perspective by showing the relevance of bifibrations. We develop a bifibrational framework for models of System F that are parametric, in that they verify the Identity Extension Lemma and Reynolds' Abstraction Theorem. We also prove that our models satisfy expected properties, such as the existence of initial algebras and final coalgebras, and that parametricity implies dinaturality.",
keywords = "fibred category theory, logical relations, parametricity, system F",
author = "Neil Ghani and Patricia Johann and Forsberg, {Fredrik Nordvall} and Federico Orsanigo and Tim Revell",
year = "2015",
month = "12",
day = "21",
doi = "10.1016/j.entcs.2015.12.011",
language = "English",
volume = "319",
pages = "165--181",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",

}

Bifibrational functorial semantics of parametric polymorphism. / Ghani, Neil; Johann, Patricia; Forsberg, Fredrik Nordvall; Orsanigo, Federico; Revell, Tim.

In: Electronic Notes in Theoretical Computer Science, Vol. 319, 21.12.2015, p. 165-181.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Bifibrational functorial semantics of parametric polymorphism

AU - Ghani, Neil

AU - Johann, Patricia

AU - Forsberg, Fredrik Nordvall

AU - Orsanigo, Federico

AU - Revell, Tim

PY - 2015/12/21

Y1 - 2015/12/21

N2 - Reynolds' theory of parametric polymorphism captures the invariance of polymorphically typed programs under change of data representation. Semantically, reflexive graph categories and fibrations are both known to give a categorical understanding of parametric polymorphism. This paper contributes further to this categorical perspective by showing the relevance of bifibrations. We develop a bifibrational framework for models of System F that are parametric, in that they verify the Identity Extension Lemma and Reynolds' Abstraction Theorem. We also prove that our models satisfy expected properties, such as the existence of initial algebras and final coalgebras, and that parametricity implies dinaturality.

AB - Reynolds' theory of parametric polymorphism captures the invariance of polymorphically typed programs under change of data representation. Semantically, reflexive graph categories and fibrations are both known to give a categorical understanding of parametric polymorphism. This paper contributes further to this categorical perspective by showing the relevance of bifibrations. We develop a bifibrational framework for models of System F that are parametric, in that they verify the Identity Extension Lemma and Reynolds' Abstraction Theorem. We also prove that our models satisfy expected properties, such as the existence of initial algebras and final coalgebras, and that parametricity implies dinaturality.

KW - fibred category theory

KW - logical relations

KW - parametricity

KW - system F

UR - http://www.scopus.com/inward/record.url?scp=84951851297&partnerID=8YFLogxK

UR - http://events.cs.bham.ac.uk/mfps31/

U2 - 10.1016/j.entcs.2015.12.011

DO - 10.1016/j.entcs.2015.12.011

M3 - Article

VL - 319

SP - 165

EP - 181

JO - Electronic Notes in Theoretical Computer Science

T2 - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -