Parametricity, type equality, and higher-order polymorphism

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.