Bifibrational Functorial Semantics of Parametric Polymorphism
Bifibrational Functorial Semantics of Parametric Polymorphism
复制标题
DOI：
10.1016/j.entcs.2015.12.011
复制
发表时间：
2015-12-21
影响因子：
--
通讯作者：
Revell, Tim
中科院分区：
文献类型：
--
作者：
Ghani, Neil;Johann, Patricia;Revell, Tim
Reynolds的参数多态性理论捕捉了多态类型程序在数据表示变化下的不变性。在语义上，自反图范畴和纤维化都被认为是参数多态性的范畴理解。本文通过展示双纤化的相关性，进一步促进了这一范畴观点。我们开发了一个双纤维框架的系统F的参数模型，在他们验证的身份扩展引理和雷诺兹的抽象定理。我们还证明了我们的模型满足预期的性质，如初始代数和最终余代数的存在性，以及参数性意味着双自然性。
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.