Comprehensive parametric polymorphism: categorical models and type theory

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

1 Citation (Scopus)

Abstract

This paper combines reflexive-graph-category structure for relational parametricity with fibrational models of impredicative polymorphism. To achieve this, we modify the definition of fibrational model of impredicative polymorphism by adding one further ingredient to the structure: comprehension in the sense of Lawvere. Our main result is that such comprehensive models, once further endowed with reflexive-graph-category structure, enjoy the expected consequences of parametricity. This is proved using a type-theoretic presentation of the category-theoretic structure, within which the desired consequences of parametricity are derived. The formalisation requires new techniques because equality relations are not available, and standard arguments that exploit equality need to be reworked.
LanguageEnglish
Title of host publicationFoundations of Software Science and Computation Structures
Subtitle of host publication19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings
EditorsBart Jacobs, Christof Löding
Pages3-19
Number of pages17
Volume9634
ISBN (Electronic)978-3-662-49630-5
DOIs
Publication statusPublished - 22 Mar 2016

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743

Fingerprint

Polymorphism

Keywords

  • polymorphism
  • re exive-graph-category structure
  • parametricity
  • impredicative polymorphism
  • type theory

Cite this

Ghani, N., Nordvall Forsberg, F., & Simpson, A. (2016). Comprehensive parametric polymorphism: categorical models and type theory. In B. Jacobs, & C. Löding (Eds.), Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings (Vol. 9634, pp. 3-19). (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-662-49630-5_1
Ghani, Neil ; Nordvall Forsberg, Fredrik ; Simpson, Alex. / Comprehensive parametric polymorphism : categorical models and type theory. Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. editor / Bart Jacobs ; Christof Löding. Vol. 9634 2016. pp. 3-19 (Lecture Notes in Computer Science).
@inproceedings{db9cd8887a1140ea95d6bfcfd2213d9d,
title = "Comprehensive parametric polymorphism: categorical models and type theory",
abstract = "This paper combines reflexive-graph-category structure for relational parametricity with fibrational models of impredicative polymorphism. To achieve this, we modify the definition of fibrational model of impredicative polymorphism by adding one further ingredient to the structure: comprehension in the sense of Lawvere. Our main result is that such comprehensive models, once further endowed with reflexive-graph-category structure, enjoy the expected consequences of parametricity. This is proved using a type-theoretic presentation of the category-theoretic structure, within which the desired consequences of parametricity are derived. The formalisation requires new techniques because equality relations are not available, and standard arguments that exploit equality need to be reworked.",
keywords = "polymorphism, re exive-graph-category structure, parametricity, impredicative polymorphism, type theory",
author = "Neil Ghani and {Nordvall Forsberg}, Fredrik and Alex Simpson",
note = "The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-49630-5_1",
year = "2016",
month = "3",
day = "22",
doi = "10.1007/978-3-662-49630-5_1",
language = "English",
isbn = "978-3-662-49629-9",
volume = "9634",
series = "Lecture Notes in Computer Science",
publisher = "Springer Berlin Heidelberg",
pages = "3--19",
editor = "Bart Jacobs and L{\"o}ding, { Christof}",
booktitle = "Foundations of Software Science and Computation Structures",

}

Ghani, N, Nordvall Forsberg, F & Simpson, A 2016, Comprehensive parametric polymorphism: categorical models and type theory. in B Jacobs & C Löding (eds), Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. vol. 9634, Lecture Notes in Computer Science, pp. 3-19. https://doi.org/10.1007/978-3-662-49630-5_1

Comprehensive parametric polymorphism : categorical models and type theory. / Ghani, Neil; Nordvall Forsberg, Fredrik; Simpson, Alex.

Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. ed. / Bart Jacobs; Christof Löding. Vol. 9634 2016. p. 3-19 (Lecture Notes in Computer Science).

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

TY - GEN

T1 - Comprehensive parametric polymorphism

T2 - categorical models and type theory

AU - Ghani, Neil

AU - Nordvall Forsberg, Fredrik

AU - Simpson, Alex

N1 - The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-49630-5_1

PY - 2016/3/22

Y1 - 2016/3/22

N2 - This paper combines reflexive-graph-category structure for relational parametricity with fibrational models of impredicative polymorphism. To achieve this, we modify the definition of fibrational model of impredicative polymorphism by adding one further ingredient to the structure: comprehension in the sense of Lawvere. Our main result is that such comprehensive models, once further endowed with reflexive-graph-category structure, enjoy the expected consequences of parametricity. This is proved using a type-theoretic presentation of the category-theoretic structure, within which the desired consequences of parametricity are derived. The formalisation requires new techniques because equality relations are not available, and standard arguments that exploit equality need to be reworked.

AB - This paper combines reflexive-graph-category structure for relational parametricity with fibrational models of impredicative polymorphism. To achieve this, we modify the definition of fibrational model of impredicative polymorphism by adding one further ingredient to the structure: comprehension in the sense of Lawvere. Our main result is that such comprehensive models, once further endowed with reflexive-graph-category structure, enjoy the expected consequences of parametricity. This is proved using a type-theoretic presentation of the category-theoretic structure, within which the desired consequences of parametricity are derived. The formalisation requires new techniques because equality relations are not available, and standard arguments that exploit equality need to be reworked.

KW - polymorphism

KW - re exive-graph-category structure

KW - parametricity

KW - impredicative polymorphism

KW - type theory

UR - http://www.etaps.org/index.php/2016/fossacs

U2 - 10.1007/978-3-662-49630-5_1

DO - 10.1007/978-3-662-49630-5_1

M3 - Conference contribution book

SN - 978-3-662-49629-9

VL - 9634

T3 - Lecture Notes in Computer Science

SP - 3

EP - 19

BT - Foundations of Software Science and Computation Structures

A2 - Jacobs, Bart

A2 - Löding, Christof

ER -

Ghani N, Nordvall Forsberg F, Simpson A. Comprehensive parametric polymorphism: categorical models and type theory. In Jacobs B, Löding C, editors, Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Vol. 9634. 2016. p. 3-19. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-662-49630-5_1