# A Relationally Parametric Model of Dependent Type Theory

## Publication Information

Robert Atkey, Neil Ghani, and Patricia Johann.

*A Relationally Parametric Model of Dependent Type Theory*. In

*Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014)*. 2014.

DOI:

10.1145/2535838.2535852## 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 λ-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. By expressing our model in terms of reflexive
graphs, our model 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.