# Is the encoding of existential types in System F adequate?

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.

• 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
Commented Jun 4 at 18:17
• @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. Commented Jun 4 at 19:07
• Good point! I guess the obvious contenders are $\beta\eta$ and observational equivalence.
– cody
Commented Jun 4 at 20:26
• 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). Commented Jun 7 at 12:41
• @Li-yaoXia may have thoughts about this. Can we have proof by normal forms? Commented Jun 7 at 13:55