Parametricity, type equality, and higher-order polymorphism

Abstract

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