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

Question

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 final result. The continuation takes two arguments—a type X and a value of type T—and uses them in computing the final 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 first 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.

Answer 1

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

Answer 2

At chapter 5 of TaPL, we saw that in untyped lambda calculus.

pair f s = \b . b f s 
fst p = p tru 
snd p = p fls 

where 
tru = \t. \f. t
fls = \t. \f. f 

This definition of pair is to be typed now. Here, b takes two arguments f:F and s:S and we assume the resulting type is R. so,

b : F -> S -> R 
b f s : R 

now we apply quantification to this R which can be any type. so we will get the typed version ;

pair f s : ∀R. (F -> S -> R) -> R 

which should result in

Pair F S = ∀R. (F -> S -> R) -> R 

Then assigning F = ∃X, S = T , and R = Y, we get;

Pair (∃X) T = ∀R. ((∃X) -> T -> Y ) -> Y

, and uncurrying can reach the following result;

Pair (∃X) T = ∀R. (((∃X) x T )-> Y ) -> Y

which is the same with

Pair (∃X) T = ∀R. ((∃X. T )-> Y ) -> Y 

and it is equivalent to

Pair (∃X) T = ∀R. (∀X. T -> Y ) -> Y