文章基本信息

标题：Relational Parametricity for Higher Kinds
本地全文：下载
作者：Robert Atkey
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2012
卷号：16
页码：46-61
DOI：10.4230/LIPIcs.CSL.2012.46
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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 Fomega, 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.
关键词：Relational Parametricity; Higher Kinds; Polymorphism