Parametricity, type equality, and higher-order polymorphism

Dimitrios Vytiniotis and Stephanie Weirich


Propositions that express type equality are a frequent ingredient of modern functional programming – they can encode generic functions, dynamic types, and GADTs. Via the Curry–Howard correspondence, these propositions are ordinary types inhabited by proof terms, computed using runtime type representations. In this paper we show that two examples of type equality propositions actually do reflect type equality; they are only inhabited when their arguments are equal and their proofs are unique (up to equivalence.) We show this result in the context of a strongly normalizing language with higher-order polymorphism and primitive recursion over runtime-type representations by proving Reynolds's abstraction theorem. We then use this theorem to derive “free” theorems about equality types.


Publication typeArticle
Published inJournal of Functional Programming
PublisherCambridge University Press
> Publications > Parametricity, type equality, and higher-order polymorphism