# How to encode a function from an existential type

I am having trouble using parametricity to show that existential types work in System F (or System Fω) in the way one would expect them to work.

It is known that an existential type $$\exists t.~P~t$$ (where $$P$$ is any type constructor, not necessarily covariant) is encoded as: $$\forall r.~(\forall t.~P~t \to r)\to r$$

(I think it is assumed that $$\forall r$$ implies a parametricity constraint.)

Let's denote this encoding as the type constructor $$E : (* \to *) \to *$$ that takes any $$P : * \to *$$ and makes a new type $$\exists t.~P~t$$ out of $$P$$. (Here, the notation * means the kind of types.)

So, for any type constructor $$P$$ we define: $$E~P = \forall r.~(\forall t.~P~t \to r)\to r$$

 E P = ∀(r : *) → (∀(t : *) → P t → r) → r


To create values of the type $$E~P$$, one uses the standard function pack defined as:

 pack : ∀(s : *) → P s → E P
pack = λ(s : *) → λ(ps : P s) → λ(r : *) → λ(c : ∀(t : *) → P t → r) → c s ps


Now, the main question is:

How to write a function type $$(\exists t.~P~t) \to q$$, where $$q$$ is a fixed type.

There are two ways of writing that type:

1. Just use the encoding $$E~P$$ as shown above, and write: $$T_1= E~P\to q = (\forall r.~(\forall t.~P~t \to r)\to r)\to q$$

2. Squint at $$(\exists t.~P~t) \to q$$ and notice that it should be just a function $$P~t \to q$$ but universally quantified in $$t$$. So, we should have: $$T_2 = \forall t.~(P~t \to q)$$

I want to prove that the types $$T_1$$ and $$T_2$$ are equivalent, under appropriate parametricity assumptions.

I don't seem to be able to do that, though. What I tried:

• Write explicit code for functions $$\mathrm{out} : T_1 \to T_2$$ and $$\mathrm{in}:T_2\to T_1$$ and then prove that in and out are inverses.

out : (E P → q) → ∀(t : *) → P t → q
out = λ(y : E P → q) → λ(t : *) → λ(pt : P t) → y (pack t pt)

in : (∀(t : *) → P t → q) → E P → q
in = λ(c : ∀(t : *) → P t → q) → λ(ep : E P) → ep q c


I can prove that out . in = id (this is just straightforward substitution).

The difficult direction is to prove that in . out = id; this requires some parametricity assumptions. I tried using the naturality law of $$E~P$$ but that does not seem to be enough.

Specifically, after using the naturality law, it still remains to prove that, for any $$e : E~P$$, that is, $$e : \forall r.~(\forall t.~P~t \to r)\to r$$, we will have: $$e~ (E~ P)~ \mathrm{pack} = e$$

• The Yoneda identities do not apply because of the universal quantifier inside $$\forall t. ~P~t\to r$$.

• I have read Wadler's "Recursive types for free" but the techniques in there don't seem to help so far. The identity e (E P) pack == e is superficially similar to the identity (4) shown in Wadler: fold T in = id but the types are different and I can't prove what I need.

Using function extensionality, it suffices to prove:

$$∀ Z\ z. e\ (E\ P)\ \mathrm{pack}\ Z\ z = e\ Z\ z$$

The naturality rule for $$e$$ is:

$$f\ (e\ A\ k) = e\ B\ (ΛR. λr. f\ (k\ R\ r))$$

If we pick $$k = \mathrm{pack}$$, so $$A = E\ P$$, and $$f\ e = e\ Z\ z$$, then we get:

$$e\ (E\ P)\ \mathrm{pack}\ Z\ z = e\ Z\ (ΛR. λr. \mathrm{pack}\ R\ r\ Z\ z) = e\ Z\ (ΛR. λr. z\ R\ r) = e\ Z\ z$$

So that gets you the $$e\ (E\ P)\ \mathrm{pack} = e$$ equation you want.

• Thank you, that looks perfect. I didn't think of writing out the extensional equality of functions like you did (with an arbitrary Z z). Without that, I could not find a suitable f for the naturality law. I will need to go through your derivation once again before approving the answer. Apr 1 at 21:34