# Proofs for Free - Parametricity for Dependent Types

Jean-Philippe Bernardy,
Patrik Jansson and
Ross Paterson.
in *Journal of Functional Programming*, vol. 22(2), pp. 107-152, 2012.

## Abstract

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 obtain a similar result for pure type systems: for any PTS used as
a programming language, there is a PTS that can be used as a logic for
parametricity. Types in the source PTS are translated to relations
(expressed as types) in the target. Similarly, values of a given type
are translated to proofs that the values satisfy the relational
interpretation. We extend the result to inductive families.

We also show that the assumption that every term satisfies the
parametricity condition generated by its type is consistent with the
generated logic.

## Summary

The core of the paper is a translation 〚-〛
of terms in a pure type system satisfying

Γ ⊢ *A*: *B* ⇒ 〚Γ〛 ⊢ 〚*A*〛: 〚*B*〛 *A*

This means that if *A* has type *B*, then

- we can translate
*B* into
a predicate 〚*B*〛 satisfied by *A*, and
- we can obtain a proof of
〚
*B*〛 *A*
by applying the same translation to *A*.

Applying the same translation to a definition of an inductive type family
yields parametricity results for the constants of the family.
## Formats