A relationally parametric model of dependent type theory

Robert Atkey, Neil Ghani, Patricia Johann

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

10 Citations (Scopus)

Abstract

Reynolds' theory of relational parametricity captures the invariance of polymorphically typed programs under change of data representation. Reynolds' original work exploited the typing discipline of the polymorphically typed lambda-calculus System F, but there is now considerable interest in extending relational parametricity to type systems that are richer and more expressive than that of System F. This paper constructs parametric models of predicative and impredicative dependent type theory. The significance of our models is twofold. Firstly, in the impredicative variant we are able to deduce the existence of initial algebras for all indexed=functors. To our knowledge, ours is the first account of parametricity for dependent types that is able to lift the useful deduction of the existence of initial algebras in parametric models of System F to the dependently typed setting. Secondly, our models offer conceptual clarity by uniformly expressing relational parametricity for dependent types in terms of reflexive graphs, which allows us to unify the interpretations of types and kinds, instead of taking the relational interpretation of types as a primitive notion. Expressing our model in terms of reflexive graphs ensures that it has canonical choices for the interpretations of the standard type constructors of dependent type theory, except for the interpretation of the universe of small types, where we formulate a refined interpretation tailored for relational parametricity. Moreover, our reflexive graph model opens the door to generalisations of relational parametricity, for example to higher-dimensional relational parametricity.
LanguageEnglish
Title of host publicationPOPL '14 Proceedings of the 41st ACM SIGPLAN-SIGACT
Subtitle of host publicationSymposium on Principles of Programming Languages
Place of PublicationNew York, NY.
Pages503-515
Number of pages13
DOIs
Publication statusPublished - 24 Jan 2014
EventPOPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - San Diego, United States
Duration: 22 Jan 201424 Jan 2014
http://popl.mpi-sws.org/2014/

Conference

ConferencePOPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
CountryUnited States
CitySan Diego
Period22/01/1424/01/14
Internet address

Fingerprint

Algebra
Invariance

Keywords

  • relational parametricity
  • dependent type theory
  • data representations
  • higher-dimensional
  • initial algebras
  • parametric modeling
  • parametric models
  • reflexive graphs

Cite this

Atkey, R., Ghani, N., & Johann, P. (2014). A relationally parametric model of dependent type theory. In POPL '14 Proceedings of the 41st ACM SIGPLAN-SIGACT: Symposium on Principles of Programming Languages (pp. 503-515). New York, NY.. https://doi.org/10.1145/2535838.2535852
Atkey, Robert ; Ghani, Neil ; Johann, Patricia. / A relationally parametric model of dependent type theory. POPL '14 Proceedings of the 41st ACM SIGPLAN-SIGACT: Symposium on Principles of Programming Languages. New York, NY., 2014. pp. 503-515
@inproceedings{0c679fbfdce242438a1d9e2bba96cb21,
title = "A relationally parametric model of dependent type theory",
abstract = "Reynolds' theory of relational parametricity captures the invariance of polymorphically typed programs under change of data representation. Reynolds' original work exploited the typing discipline of the polymorphically typed lambda-calculus System F, but there is now considerable interest in extending relational parametricity to type systems that are richer and more expressive than that of System F. This paper constructs parametric models of predicative and impredicative dependent type theory. The significance of our models is twofold. Firstly, in the impredicative variant we are able to deduce the existence of initial algebras for all indexed=functors. To our knowledge, ours is the first account of parametricity for dependent types that is able to lift the useful deduction of the existence of initial algebras in parametric models of System F to the dependently typed setting. Secondly, our models offer conceptual clarity by uniformly expressing relational parametricity for dependent types in terms of reflexive graphs, which allows us to unify the interpretations of types and kinds, instead of taking the relational interpretation of types as a primitive notion. Expressing our model in terms of reflexive graphs ensures that it has canonical choices for the interpretations of the standard type constructors of dependent type theory, except for the interpretation of the universe of small types, where we formulate a refined interpretation tailored for relational parametricity. Moreover, our reflexive graph model opens the door to generalisations of relational parametricity, for example to higher-dimensional relational parametricity.",
keywords = "relational parametricity, dependent type theory, data representations, higher-dimensional, initial algebras, parametric modeling, parametric models, reflexive graphs",
author = "Robert Atkey and Neil Ghani and Patricia Johann",
year = "2014",
month = "1",
day = "24",
doi = "10.1145/2535838.2535852",
language = "English",
isbn = "9781450325448",
pages = "503--515",
booktitle = "POPL '14 Proceedings of the 41st ACM SIGPLAN-SIGACT",

}

Atkey, R, Ghani, N & Johann, P 2014, A relationally parametric model of dependent type theory. in POPL '14 Proceedings of the 41st ACM SIGPLAN-SIGACT: Symposium on Principles of Programming Languages. New York, NY., pp. 503-515, POPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, United States, 22/01/14. https://doi.org/10.1145/2535838.2535852

A relationally parametric model of dependent type theory. / Atkey, Robert; Ghani, Neil; Johann, Patricia.

POPL '14 Proceedings of the 41st ACM SIGPLAN-SIGACT: Symposium on Principles of Programming Languages. New York, NY., 2014. p. 503-515.

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

TY - GEN

T1 - A relationally parametric model of dependent type theory

AU - Atkey, Robert

AU - Ghani, Neil

AU - Johann, Patricia

PY - 2014/1/24

Y1 - 2014/1/24

N2 - Reynolds' theory of relational parametricity captures the invariance of polymorphically typed programs under change of data representation. Reynolds' original work exploited the typing discipline of the polymorphically typed lambda-calculus System F, but there is now considerable interest in extending relational parametricity to type systems that are richer and more expressive than that of System F. This paper constructs parametric models of predicative and impredicative dependent type theory. The significance of our models is twofold. Firstly, in the impredicative variant we are able to deduce the existence of initial algebras for all indexed=functors. To our knowledge, ours is the first account of parametricity for dependent types that is able to lift the useful deduction of the existence of initial algebras in parametric models of System F to the dependently typed setting. Secondly, our models offer conceptual clarity by uniformly expressing relational parametricity for dependent types in terms of reflexive graphs, which allows us to unify the interpretations of types and kinds, instead of taking the relational interpretation of types as a primitive notion. Expressing our model in terms of reflexive graphs ensures that it has canonical choices for the interpretations of the standard type constructors of dependent type theory, except for the interpretation of the universe of small types, where we formulate a refined interpretation tailored for relational parametricity. Moreover, our reflexive graph model opens the door to generalisations of relational parametricity, for example to higher-dimensional relational parametricity.

AB - Reynolds' theory of relational parametricity captures the invariance of polymorphically typed programs under change of data representation. Reynolds' original work exploited the typing discipline of the polymorphically typed lambda-calculus System F, but there is now considerable interest in extending relational parametricity to type systems that are richer and more expressive than that of System F. This paper constructs parametric models of predicative and impredicative dependent type theory. The significance of our models is twofold. Firstly, in the impredicative variant we are able to deduce the existence of initial algebras for all indexed=functors. To our knowledge, ours is the first account of parametricity for dependent types that is able to lift the useful deduction of the existence of initial algebras in parametric models of System F to the dependently typed setting. Secondly, our models offer conceptual clarity by uniformly expressing relational parametricity for dependent types in terms of reflexive graphs, which allows us to unify the interpretations of types and kinds, instead of taking the relational interpretation of types as a primitive notion. Expressing our model in terms of reflexive graphs ensures that it has canonical choices for the interpretations of the standard type constructors of dependent type theory, except for the interpretation of the universe of small types, where we formulate a refined interpretation tailored for relational parametricity. Moreover, our reflexive graph model opens the door to generalisations of relational parametricity, for example to higher-dimensional relational parametricity.

KW - relational parametricity

KW - dependent type theory

KW - data representations

KW - higher-dimensional

KW - initial algebras

KW - parametric modeling

KW - parametric models

KW - reflexive graphs

UR - http://dl.acm.org/citation.cfm?id=2535838

U2 - 10.1145/2535838.2535852

DO - 10.1145/2535838.2535852

M3 - Conference contribution book

SN - 9781450325448

SP - 503

EP - 515

BT - POPL '14 Proceedings of the 41st ACM SIGPLAN-SIGACT

CY - New York, NY.

ER -

Atkey R, Ghani N, Johann P. A relationally parametric model of dependent type theory. In POPL '14 Proceedings of the 41st ACM SIGPLAN-SIGACT: Symposium on Principles of Programming Languages. New York, NY. 2014. p. 503-515 https://doi.org/10.1145/2535838.2535852