<p>Using function extensionality, it suffices to prove:</p>
<p><span class="math-container">$$∀ Z\ z. e\ (E\ P)\ \mathrm{pack}\ Z\ z = e\ Z\ z$$</span></p>
<p>The naturality rule for <span class="math-container">$e$</span> is:</p>
<p><span class="math-container">$$f\ (e\ A\ k) = e\ B\ (ΛR. λr. f\ (k\ R\ r))$$</span></p>
<p>If we pick <span class="math-container">$k = \mathrm{pack}$</span>, so <span class="math-container">$A = E\ P$</span>, and <span class="math-container">$f\ e = e\ Z\ z$</span>, then we get:</p>
<p><span class="math-container">$$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$$</span></p>
<p>So that gets you the <span class="math-container">$e\ (E\ P)\ \mathrm{pack} = e$</span> equation you want.</p>

CC BY-SA 4.0
2024-04-01T21:34:38.217Z
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.
winitzki
CC BY-SA 4.0
2024-04-01T19:27:30.017Z
2024-04-01T19:27:30.017Z
Dan Doel
<p>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.</p>
<p>It is known that an existential type <span class="math-container">$\exists t.~P~t$</span> (where <span class="math-container">$P$</span> is any type constructor, not necessarily covariant) is encoded as:  <span class="math-container">$$\forall r.~(\forall t.~P~t \to r)\to r $$</span></p>
<p>(I think it is assumed that <span class="math-container">$\forall r$</span> implies a parametricity constraint.)</p>
<p>Let's denote this encoding as the type constructor <span class="math-container">$E : (* \to *) \to *$</span> that takes any <span class="math-container">$P : * \to *$</span> and makes a new type <span class="math-container">$\exists t.~P~t$</span> out of <span class="math-container">$P$</span>. (Here, the notation <code>*</code> means the kind of types.)</p>
<p>So, for any type constructor <span class="math-container">$P$</span> we define:
<span class="math-container">$$E~P = \forall r.~(\forall t.~P~t \to r)\to r $$</span></p>
<pre><code> E P = ∀(r : *) → (∀(t : *) → P t → r) → r
</code></pre>
<p>To create values of the type <span class="math-container">$E~P$</span>, one uses the standard function <code>pack</code> defined as:</p>
<pre><code> pack : ∀(s : *) → P s → E P
 pack = λ(s : *) → λ(ps : P s) → λ(r : *) → λ(c : ∀(t : *) → P t → r) → c s ps
</code></pre>
<p>Now, the main question is:</p>
<p>How to write a function type <span class="math-container">$(\exists t.~P~t) \to q$</span>, where <span class="math-container">$q$</span> is a fixed type.</p>
<p>There are two ways of writing that type:</p>
<ol>
<li><p>Just use the encoding <span class="math-container">$ E~P$</span> as shown above, and write: <span class="math-container">$$ T_1=  E~P\to q  = (\forall r.~(\forall t.~P~t \to r)\to r)\to q $$</span></p>
</li>
<li><p>Squint at <span class="math-container">$(\exists t.~P~t) \to q$</span> and notice that it should be just a function <span class="math-container">$P~t \to q$</span> but <em>universally</em> quantified in <span class="math-container">$t$</span>. So, we should have: <span class="math-container">$$ T_2 = \forall t.~(P~t \to q) $$</span></p>
</li>
</ol>
<p>I want <strong>to prove that the types  <span class="math-container">$T_1$</span> and <span class="math-container">$T_2$</span> are equivalent</strong>, under appropriate parametricity assumptions.</p>
<p>I don't seem to be able to do that, though.
What I tried:</p>
<ul>
<li><p>Write explicit code for functions <span class="math-container">$\mathrm{out} : T_1 \to T_2 $</span> and <span class="math-container">$\mathrm{in}:T_2\to T_1$</span> and then prove that <code>in</code> and <code>out</code> are inverses.</p>
<pre><code>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
</code></pre>
</li>
</ul>
<p>I can prove that <code>out . in = id</code> (this is just straightforward substitution).</p>
<p>The difficult direction is to prove that <code>in . out = id</code>; this requires some parametricity assumptions. I tried using the naturality law of <span class="math-container">$ E~P$</span> but that does not seem to be enough.</p>
<p>Specifically, after using the naturality law,  it still remains to prove that, for any <span class="math-container">$e : E~P$</span>, that is, <span class="math-container">$e : \forall r.~(\forall t.~P~t \to r)\to r$</span>, we will have: <span class="math-container">$$ e~ (E~ P)~ \mathrm{pack} = e  $$</span></p>
<ul>
<li><p>The Yoneda identities do not apply because of the universal quantifier inside <span class="math-container">$\forall t. ~P~t\to r$</span>.</p>
</li>
<li><p>I have read Wadler's &quot;Recursive types for free&quot; but the techniques in there don't seem to help so far. The identity <code>e (E P) pack == e</code> is superficially similar to the identity  (4) shown in Wadler: <code>fold T in  =  id</code> but the types are different and I can't prove what I need.</p>
</li>
</ul>

<type-theory><typed-lambda-calculus><parametricity>
How to encode a function from an existential type
winitzki
# How to encode a function from an existential type

(Asked by: username_0 on 2024-04-01)

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:

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 $$

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.

**Tags:** type-theory, typed-lambda-calculus, parametricity

---

## 1 answers

### Answer by username_1 on 2024-04-01. Score: 3 | Accepted answer

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.

> **Comments:**
> **username_0**: 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.  

---

