# How can an existential type be defined in terms of universal type?

In Types and Programming Languages by Pierce, how does the following achieve the definition of an existential type in terms of universal type, by polymorphic version of Church encoding of pairs?

24.3 Encoding Existentials

The encoding of pairs as a polymorphic type in §23.4 suggests a similar encoding for existential types in terms of universal types, using the intuition that an element of an existential type is a pair of a type and a value:

{∃X,T} := ∀Y. (∀X. T→Y) → Y.


That is, an existential package is thought of as a data value that, given a result type and a continuation, calls the continuation to yield a ﬁnal result. The continuation takes two arguments—a type X and a value of type T—and uses them in computing the ﬁnal result.

To complete the quote, the polymorphic version of Church encoding of pairs of numbers is given in Exercise 23.4.8 (p349 p546):

pairNat = λn1:CNat. λn2:CNat.
λX. λf:CNat→CNat→X. f n1 n2;
fstNat = λp:PairNat. p [CNat] (λn1:CNat. λn2:CNat. n1);
sndNat = λp:PairNat. p [CNat] (λn1:CNat. λn2:CNat. n2);


which is further generalized to pairs of elements of any types, on p352

we use the abbreviation Pair X Y (generalizing the PairNat type from Exercise 23.4.8) for the Church encoding of pairs with ﬁrst component of type X and second component of type Y:

Pair X Y = ∀R. (X→Y→R) → R;


The operations on pairs are simple generalizations of the operations on the type PairNat above:

> pair : ∀X. ∀Y. X → Y → Pair X Y
fst : ∀X. ∀Y. Pair X Y → X
snd : ∀X. ∀Y. Pair X Y → Y


Thanks.

• What's the question here? Are you saying that Pair X Y is an encoding of a variant type X + Y? Because it isn't. – Andrej Bauer Sep 7 '19 at 9:09
• typo: variant -> existential – Tim Sep 7 '19 at 10:36
• Well, I answered both :-) – Andrej Bauer Sep 7 '19 at 15:51

As a general recipe, to figure out how to encode a type A, write down

∀Z . (A → Z) → Z


and massage it to something that does not involve A, using basic isomorphisms, such as currying and uncurrying. For example, if we plug in A := X + Y we get:

∀ Z . (X + Y → Z) → Z           ≅
∀ Z . (X → Z) × (Y → Z) → Z     ≅
∀ Z . (X → Z) → (Y → Z) → Z


You can also read the above lines as a sequence of logical equivalences. So this gives us the encoding of X + Y in terms of the universal quantifier.

I do not understand why in your question you speak about existential types, but since you do, it is worth explaining the encoding of ∃ X . B(X) in terms of ∀ this way:

∀ Z . ((∃ X . B(X)) → Z) → Z    ≅
∀ Z . (∀ X . (B(X) → Z)) → Z


Again, you can read the equivalence either as a type isomorphism or a logical equivalence in logic, using the fact that $$(\exists x . \phi(x)) \Rightarrow \psi$$ is equivalent to $$\forall x . (\phi(x) \Rightarrow \psi))$$.