17
$\begingroup$

Internal parametricity refers to the ability to claim that $\forall u : (\forall t. t \to t). u = \lambda x. x$ and similarly for other pi types abstracting over types (this is a meta-theoretic property of System F, but in dependent type one may internalize it). This is not provable in most popular systems like Idris, Lean, and Agda, but there is some work like "type theory in color" to internalize parametricity in a dependent type system.

I'm wondering how this theorem can be useful. Does it simplify proofs? Does it have powerful corollaries?

To be clear, by "theorem proving" I meant in the object level, not meta level.

$\endgroup$
0

3 Answers 3

10
$\begingroup$

I don’t know about the theorem in itself, but internal parametricity in the sense of a translation from a dependly typed system to itself (as first pioneered by Bernardi and Lasson) is quite an important building block in recent works. For instance, to get automatic proof of equivalences between types, as done in Univalent Parametricity.

$\endgroup$
0
8
$\begingroup$

I don't know as much about parametricity for dependently typed language to be fully confident about this so take this with a grain of salt. But to give an upper bound on the potential utility of internal parametricity, let me describe one effective way to work with external parametricity.

Although you cannot prove $\forall u : (\forall t.t\to t). u = \lambda x. x$ within a typical type theory, one thing you can do is, given a concrete term $u$, construct a proof of $u = \lambda x. x$ (for an extensional $=$).

More generally, given a term $t : T$, you can translate the type $T$ to its Reynolds-relation $\lceil T\rceil : T \to T \to \mathrm{Type}$ and the term $t$ to a proof $\lceil t \rceil : \lceil T\rceil\;t\;t$ (from which theorems such as the one above can be derived). For example, the paramcoq plugin does this translation in Coq. Internal parametricity is when that translation is instead definable as a function in the theory itself. But external parametricity already goes a long way.

Whenever you would apply the parametricity theorem to a variable $v : T$, add the relevant instance of that theorem as an additional assumption $v' : \lceil T \rceil\;v\;v$, and whenever $v$ gets instantiated with a concrete term $t$, invoke external parametricity to construct the required proof $\lceil t \rceil$. This bloats proofs since you're threading extra assumptions and proving obvious things, but the effort is mechanizable to a high degree. Without changing the language (by adding parametricity axioms or switching to a language that internalizes parametricity), external parametricity is at least enough to enable applications of parametricity in the style of Theorems for free!.

$\endgroup$
4
$\begingroup$

Here are two uses of parametricity:

  • Bob Atkey has a way of connecting parametricity to Noether's theorem to automatically derive conservation laws from the type of the Lagrangian. Presumably internalizing parametricity would let you prove conservation laws internally rather than just as a metatheorem

  • My own work on "Reification by Parametricity" allows fast reification of terms, even allowing reification of metaprograms that generate terms, in some sense. However, proving that these reifications are correct requires either reducing them, or having an internalized parametricity theorem in hand. The latter would allow vastly more efficient reification.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.