Relational Parametricity for Higher Kinds
Relational Parametricity for Higher Kinds
复制标题
高级类型的关系参数性
DOI：
10.4230/lipics.csl.2012.46
复制
发表时间：
2012
影响因子：
22.7
通讯作者：
R. Atkey
中科院分区：
文献类型：
--
作者：
R. Atkey
Reynolds的关系参数化概念对多态编程语言和基于System F的类型理论有着极大的影响力，并得到了很好的研究。将关系参数性扩展到更高类型的多态性（允许对类型操作符和类型进行量化）并没有得到太多的关注。我们提出了系统Fω的关系参数化模型，在归纳结构的非谓词演算，并显示它如何形成长谷川定义的一般类模型的一个实例。我们调查我们的模型的一些后果，并表明它支持的定义归纳类型，索引的任意一种，并提供了初始化的推理原则。
Reynolds’ notion of relational parametricity has been extremely influential and well studied for polymorphic programming languages and type theories based on System F. The extension of relational parametricity to higher kinded polymorphism, which allows quantification over type operators as well as types, has not received as much attention. We present a model of relational parametricity for System Fω, within the impredicative Calculus of Inductive Constructions, and show how it forms an instance of a general class of models defined by Hasegawa. We investigate some of the consequences of our model and show that it supports the definition of inductive types, indexed by an arbitrary kind, and with reasoning principles provided by initiality.