<p>This is somewhat related to <a href="https://cstheory.stackexchange.com/questions/54124">How to encode a function from an existential type</a></p>
<p>Existential types can be encoded in System F. If <span class="math-container">$P$</span> is any type constructor, not necessarily covariant, then the existential type <span class="math-container">$\exists t.~P~t$</span> is encoded as:  <span class="math-container">$$\forall r.~(\forall t.~P~t \to r)\to r $$</span></p>
<p>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>.</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>The main question is: how to show that <em>all values</em> of type <span class="math-container">$E~P$</span> can be obtained using <code>pack</code>. This is to show that <code>pack</code> is surjective; or that the encoding is &quot;adequate&quot; and there are no System F functions of type <code>E P</code> that do not correspond to some encapsulated type <code>s</code> and a value <code>ps : P s</code>.</p>
<p>Alternatively, how to show that is not true and to give a counterexample: some System F code for a certain function <code>f : E P</code> with a suitable <span class="math-container">$P$</span> such that there are no types <code>s</code> and no values <code>ps : P s</code> satisfying <code>f = pack s ps</code>.</p>
<p>To show that <code>pack</code> is surjective, we may try implementing its left inverse <code>unpack</code> and show that <code>pack (unpack f) == f</code>.</p>
<p>But it does not seem to be possible to extract <code>s</code> and <code>ps</code> from a given value <code>f : E P</code>. Parametricity is built into System F and it prohibits us from getting any specific type out of <span class="math-container">$\forall r.~(\forall t.~P~t \to r)\to r$</span>. So, if <code>pack</code> is surjective, the <code>unpack</code> function needs to violate parametricity (and cannot be implemented in System F). That may not be a problem if we are somehow able to show that <code>pack</code> is surjective by going outside System F. But at this point I do not see how to proceed with any possible proof.</p>

CC BY-SA 4.0
2024-06-04T18:17:42.153Z
You're sort of asking two questions here:

1. "Can I build a value of `E P` that is not (equivalent to) an application of `pack`?" and 
2. Is there a left inverse to `pack`?

These questions could be summarized as "external vs internal surjectivity of `pack`" I strongly suspect that the two questions have different answers.
cody
CC BY-SA 4.0
2024-06-04T19:07:08.410Z
@cody I believe there is another omission in the question: how the equality is defined on System F terms. Existential types have the property that they can be "different values" (judgmentally) and yet equal "for all practical purposes" (extentionally). For example, a value of type ∃.  can be created using `pack` in various ways (`pack Nat 0`, `pack Bool False` etc.) and yet all those values are extentionally the same and equivalent to just the Unit type.
winitzki
CC BY-SA 4.0
2024-06-04T20:26:40.867Z
Good point! I guess the obvious contenders are $\beta\eta$ and observational equivalence.
cody
CC BY-SA 4.0
2024-06-07T12:41:00.993Z
Is it not possible to reason by what a normal Natural Deduction proof of $E P$ must be? It seems like this forces any inhabitant to indeed have form $\lambda r^{*} \lambda c^{\forall t (Pt \to r)} (c s p)$ for some $s:*$ and $p: Ps$, just since (a) eliminations must be higher than introductions in the main branch; and (b) pattern-matching hypotheses and conclusions for identities. (Here I am only thinking in the $(\to,\forall)$ language).
Anupam Das
CC BY-SA 4.0
2024-06-07T13:55:25.067Z
@Li-yaoXia may have thoughts about this. Can we have proof by normal forms?
winitzki
<type-theory><functional-programming><type-systems><typed-lambda-calculus><parametricity>
Is the encoding of existential types in System F adequate?
winitzki
# Is the encoding of existential types in System F adequate?

(Asked by: username_0 on 2024-06-03)

This is somewhat related to How to encode a function from an existential type
Existential types can be encoded in System F. If $P$ is any type constructor, not necessarily covariant, then the existential type $\exists t.~P~t$ is encoded as:  $$\forall r.~(\forall t.~P~t \to r)\to r $$
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$.
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

The main question is: how to show that all values of type $E~P$ can be obtained using pack. This is to show that pack is surjective; or that the encoding is "adequate" and there are no System F functions of type E P that do not correspond to some encapsulated type s and a value ps : P s.
Alternatively, how to show that is not true and to give a counterexample: some System F code for a certain function f : E P with a suitable $P$ such that there are no types s and no values ps : P s satisfying f = pack s ps.
To show that pack is surjective, we may try implementing its left inverse unpack and show that pack (unpack f) == f.
But it does not seem to be possible to extract s and ps from a given value f : E P. Parametricity is built into System F and it prohibits us from getting any specific type out of $\forall r.~(\forall t.~P~t \to r)\to r$. So, if pack is surjective, the unpack function needs to violate parametricity (and cannot be implemented in System F). That may not be a problem if we are somehow able to show that pack is surjective by going outside System F. But at this point I do not see how to proceed with any possible proof.

**Tags:** type-theory, functional-programming, type-systems, typed-lambda-calculus, parametricity
> **Comments:**
> **username_1**: You're sort of asking two questions here:  1. "Can I build a value of `E P` that is not (equivalent to) an application of `pack`?" and  2. Is there a left inverse to `pack`?  These questions could be summarized as "external vs internal surjectivity of `pack`" I strongly suspect that the two questions have different answers.  
> **username_0**: @cody I believe there is another omission in the question: how the equality is defined on System F terms. Existential types have the property that they can be "different values" (judgmentally) and yet equal "for all practical purposes" (extentionally). For example, a value of type ∃.  can be created using `pack` in various ways (`pack Nat 0`, `pack Bool False` etc.) and yet all those values are extentionally the same and equivalent to just the Unit type.  
> **username_1**: Good point! I guess the obvious contenders are $\beta\eta$ and observational equivalence.  
> **username_2**: Is it not possible to reason by what a normal Natural Deduction proof of $E P$ must be? It seems like this forces any inhabitant to indeed have form $\lambda r^{*} \lambda c^{\forall t (Pt \to r)} (c s p)$ for some $s:*$ and $p: Ps$, just since (a) eliminations must be higher than introductions in the main branch; and (b) pattern-matching hypotheses and conclusions for identities. (Here I am only thinking in the $(\to,\forall)$ language).  
> **username_0**: @Li-yaoXia may have thoughts about this. Can we have proof by normal forms?  

---

## 0 answers

