Existential types

Read TAPL 24.

Motivation 1

In C++, you can write a class like this:

class int_bag1 {
public:
  void add(int n) {
    elements.push_back(n);
  }
private:
    vector<int> elements;
};

Or like this:

class int_bag2 {
public:
  void add(int n) {
    counts[n]++;
  }
private:
    map<int, int> counts;
}

And you could write a generic function that operates on either one:

template <typename B>
void add_range(B &bag, int start, int stop) {
  for (int i=start; i<stop; i++)
    b.add(i);
}

This example illustrates

• Data abstraction: There are two ways to implement a bag of integers, and add_range doesn’t care which.

• Information hiding: The classes int_bag1 and int_bag2 don’t let you know how the data structure is actually implemented (because elements and counts are private).

How do we add something like this to the λ-calculus and define semantics for it?

For example, it’s great that we can encode Church Booleans in System F:

CBool ≡ ∀X. X → X → X
  tru ≡ λX. λt:X. λf:X. t
  fls ≡ λX. λt:X. λf:X. f
 test ≡ λb:(∀X.X→X→X). λX. λt:X. λf:X. b [X] t f

But we don’t have data abstraction, because there’s no easy way to plug in different implementations of Booleans, and we don’t have information hiding, because someone could do unintended things like directly call tru [Nat] (succ 0) 0.

Can we package up the encoding of Church Booleans in a way that has these properties? One answer is existential types.

Motivation 2

The motivation in the book is helpful, but perhaps it’s helpful to pursue the analogy with logic a bit further.

The sentence ∀x. x + 0 = x can be thought of as saying, “You give me any number, and I claim that adding 0 to it gives the same number.” More precisely, a proof of ∀x. x + 0 = x gives a way of mapping any particular number, say, 123, to a proof that 123 + 0 = 123.

In (sort of) the same way, the type ∀X. X→X can be thought of as saying, “Give me any type X, and I can give you a term that has type X→X”. One example (really, the only example) of such a mapping is the System F term ∀X. λx:X. x.

The sentence ∃x. x * x = 1 could be thought of as saying, “I have a number – but am not telling you what it is – and squaring it gives 1.” More precisely, one way to prove this sentence would be to exhibit a particular number, 1, together with a proof that 1 * 1 = 1. Or, -1 together with a proof at -1 * -1 = 1.

Similarly, the type ∃X. X→X can be thought of as saying, “I have a type X – but I am not telling you what it is – and there’s a term of type X→X.” And the terms that have this existential type should exhibit one such type, say, Nat, together with a term of type Nat→Nat, say, λx. succ x. Or, Bool, together with a term of type Bool→Bool, say, λx. not x.

So the fact that an existential might have many examples, and the fact that the existential itself doesn’t give any example, make existential types a good way to express data abstraction and information hiding.

Syntax

Maybe I shouldn’t mess with the book’s syntax, but I did:

t ::= ...
      {*X, t} as ∃X. T
      let {*X, x} = t1 in t2

T ::= ...
      ∃X. T

Example

There’s more than one way to make use of existentials, as described in the book, but here would be one way hide the implementation details of Booleans:

 Bool ≡ ∃B. {tru: B, fls: B, test: B → ∀X. X → X → X}
 
CBool ≡ {*∀X. X → X → X,
         {tru = λX. λt:X. λf:X. t,
          fls = λX. λt:X. λf:X. f,
          test = λb:(∀X.X→X→X). λX. λt:X. λf:X. b [X] t f}} as Bool

VBool ≡ {*<tru:Unit, fls:Unit>,
         {tru = <tru=Unit>,
          fls = <fls=Unit>,
          test = λb:<tru:Unit, fls:Unit>. λX. λt:X. λf:X.case b of
                                                          <tru=z> ⇒ t,
                                                          <fls=z> ⇒ f}} as Bool

Then, for example, we could define a not that works with either kind of Boolean.

not ≡ λbool:Bool. let {*B, r} = bool in
                    λb:B. r.test b [B] r.fls r.tru

Encoding existentials

In logic, we have ∃X.ϕ ⟷ ¬∀X.¬ϕ (where X ranges over Booleans), which suggests that we might be able to express existentials in terms of universals. We don’t have any type operator that corresponds to negation (yet), but we do have the following more complicated equivalence not using negation:

∃X.ϕ ⟷ ∀Y. (∀X. ϕ→Y) → Y

A second way to think about this is by analogy with pairs.

                     {T1, T2} ≡ ∀Y. (X1→X2→Y)→Y
                     {v1, v2} ≡ λY. λf:X1→X2→Y. f v1 v2
(letpair {x1, x2} = t3 in t4) ≡ t3 [T4] (λx1. λx2. t3)     (where t4:T4)

Either way, we are led to the following:

                    ∃X.T ≡ ∀Y. (∀X.T→Y) → Y
        {*S, t} as ∃X. T ≡ λY. λf:(∀X.T→Y). f [S] t
(let {*X, x} = t3 in t4) ≡ t3 [T4] (λX. λx:T31. t3)   (where t3:∃X.T31 and t3:T3)