Bifibrational functorial semantics of parametric polymorphism

Ghani, Neil and Johann, Patricia and Forsberg, Fredrik Nordvall and Orsanigo, Federico and Revell, Tim (2015) Bifibrational functorial semantics of parametric polymorphism. Electronic Notes in Theoretical Computer Science, 319. pp. 165-181. ISSN 1571-0661 (https://doi.org/10.1016/j.entcs.2015.12.011)

[thumbnail of Ghani-etal-ENTCS2015-bifibrational-functorial-semantics-of-parametric-polymorphism]
Preview
 Text. Filename: Ghani_etal_ENTCS2015_bifibrational_functorial_semantics_of_parametric_polymorphism.pdf
Final Published Version
License: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 logo
Download (330kB)| Preview

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.

CORE (COnnecting REpositories)