0
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Sep 7 at 9:09
  • $\begingroup$ typo: variant -> existential $\endgroup$ – Tim Sep 7 at 10:36
  • $\begingroup$ Well, I answered both :-) $\endgroup$ – Andrej Bauer Sep 7 at 15:51
1
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.