Relational parametricity for higher kinds

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

Abstract

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.
LanguageEnglish
Title of host publicationComputer science logic
Number of pages15
Publication statusAccepted/In press - 2012

Publication series

NameEPTCS

Fingerprint

Polymorphism
Computer programming languages

Keywords

  • relational parametricity
  • polymorphism
  • higher kinds
  • polymorphic programming languages
  • system f

Cite this

Atkey, R. (Accepted/In press). Relational parametricity for higher kinds. In Computer science logic (EPTCS).
Atkey, Robert. / Relational parametricity for higher kinds. Computer science logic. 2012. (EPTCS).
@inproceedings{4fbc1e789cb847c7b46af029f7dd4178,
title = "Relational parametricity for higher kinds",
abstract = "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.",
keywords = "relational parametricity, polymorphism, higher kinds, polymorphic programming languages, system f",
author = "Robert Atkey",
year = "2012",
language = "English",
series = "EPTCS",
booktitle = "Computer science logic",

}

Atkey, R 2012, Relational parametricity for higher kinds. in Computer science logic. EPTCS.

Relational parametricity for higher kinds. / Atkey, Robert.

Computer science logic. 2012. (EPTCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

TY - GEN

T1 - Relational parametricity for higher kinds

AU - Atkey, Robert

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

KW - relational parametricity

KW - polymorphism

KW - higher kinds

KW - polymorphic programming languages

KW - system f

UR - https://personal.cis.strath.ac.uk/robert.atkey/fomega-parametricity.html

M3 - Conference contribution book

T3 - EPTCS

BT - Computer science logic

ER -

Atkey R. Relational parametricity for higher kinds. In Computer science logic. 2012. (EPTCS).