Parametricity and dependent types

Jean-Philippe Bernardy, Patrik Jansson, Ross Paterson. Parametricity and dependent types. In Paul Hudak, Stephanie Weirich, editors, Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010. pages 345-356, ACM, 2010. [doi]


Reynolds’ abstraction theorem shows how a typing judgement in System F can be translated into a relational statement (in second order predicate logic) about inhabitants of the type. We expose a similar result, where terms, types, and their relations are expressed in a single typed lambda calculus (a pure type system). Working within a single system dispenses the need for an interpretation layer, allowing for an unusually simple presentation. While the unification puts some constraints on the type system (which we spell out), the result applies to many interesting cases, including dependently-typed ones.