Existential types
Read TAPL 24.
Motivation
In modular and object-oriented programming, an important principle is to separate a module or object into an interface and an implementation. Users of the module or object only see the interface, and are indifferent, if there are multiple implementations, to which implementation is used.
How do we add something like this to the λ-calculus? For example, we can encode Church Booleans in System F:
CBool ≡ ∀Y. Y → Y → Y
ctru ≡ λY. λt:Y. λf:Y. t
cfls ≡ λY. λt:Y. λf:Y. f
ctest ≡ λb:(∀Y.Y→Y→Y). λY. λt:Y. λf:Y. b [Y] t fOr, we could use variants:
VBool ≡ <tru:Unit, fls:Unit>
vtru ≡ <tru=unit>
vfls ≡ <fls=unit>
vtest ≡ λb:<tru:Unit, fls:Unit>. λY. λt:Y. λf:Y.case b of
<tru=z> ⇒ t,
<fls=z> ⇒ fBut we don’t have any way to write a function that can operate on
either CBools or VBools. And a function that
operates on CBools could do unintended things like directly
call tru [Nat] 1 0.
What we want to do is to package up CBool together with
ctru, cfls, and ctest in such a
way that a user only sees an opaque type together with opaque functions
that operate on that type.
Existential types can do this for us. We’ve learned universal types; what’s an existential type?
In logic, 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.” 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 programming languages, 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 (actually,
the only example) of such a mapping is λX. λx:X. x.
In logic, 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.” One way to prove this sentence would be to exhibit
a particular number, 1, and a proof that
1 * 1 = 1. Or, -1 together with a proof that
-1 * -1 = 1.
So, in programming languages, 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 a term of type X→X.” And
the terms that have this existential type would 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. This separation
between an interface (the existential type ∃X. X→X) and
an implementation (Nat and \x. succ x) is
exactly what we want.
Syntax
Maybe I shouldn’t mess with the book’s syntax, but I did:
t ::= ...
{*T1, t2} as ∃X1. T2
let {*X1, x2} = t in t3
T ::= ...
∃X1. T2The first form, sometimes called pack, introduces an
existential. The {*T1, t2} can be thought of as the
implementation, while the ∃X1. T2 is the existential type
and can be thought of as the interface. The {*T1, t2} is
supposed to look like a pair containing a type T1 (marked
with a * to remind you that it’s not a term), which on the
outside is only known as X1, and a term t2,
which on the outside is only known to have type T2.
The second form, sometimes called unpack, takes an
existential t and binds X1 to its first member
and x2 to its second member. Then it evaluates
t3.
The typing and evaluation rules can be found in the book (Figure 24-1).
Example
Because existentials are module-like, it’s common to combine them
with records (TAPL 11.8), which are like tuples with named
members. We omit a formal definition here, but a record type is written
like {l1: T1, l2: T2} where l1 and
l2 are labels, and a record value is written like
{l1 = v1, l2 = v2}. If t is a record then you
access its members as t.l1 and t.l2.
There’s more than one way to make use of existentials, as described in the book, but here would be one way to hide the implementation details of Booleans:
Bools ≡ ∃B. {tru: B, fls: B, test: B → ∀Y. Y → Y → Y}
cbools : Bools
cbools ≡ {*∀Y. Y → Y → Y,
{tru = λY. λt:Y. λf:Y. t,
fls = λY. λt:Y. λf:Y. f,
test = λb:(∀Y.Y→Y→Y). λY. λt:Y. λf:Y. b [Y] t f}} as Bools
vbools : Bools
vbools ≡ {*<tru:Unit, fls:Unit>,
{tru = <tru=unit>,
fls = <fls=unit>,
test = λb:<tru:Unit, fls:Unit>. λY. λt:Y. λf:Y.case b of
<tru=z> ⇒ t,
<fls=z> ⇒ f}} as Bools
Then suppose we want to write the equivalent of
test true 1 0 that works with either implementation:
main : Bools → Nat
main ≡ λbools:Bools. let {*B, r} = bools in
r.test r.tru 1 0
main cbools ⟶* 1
main vbools ⟶* 1Next, suppose we want to add some useful functions. You might think we can write
boolutils = λbools:Bools. let {*B, r} = bools in
{and: λx:B. λy:B. r.test x y r.fls,
or: λx:B. λy:B. r.test x r.tru y,
not: λx:B. r.test x r.fls r.tru}but this would not typecheck, because it tries to let B
“leak” out of the let {*B, r}.
What we can do is unpack an existential and re-pack it with the functions added:
Bools' ≡ ∃B. {tru: B, fls: B, test: B → ∀Y. Y → Y → Y,
and: B → B → B, or: B → B → B, not: B → B}
boolutils : Bools → Bools'
boolutils ≡ λbools: Bools. let {*B, r} = bools in {*B,
{tru: r.tru, fls: r.fls, test: r.test,
and: λx:B. λy:B. r.test x y r.fls,
or: λx:B. λy:B. r.test x r.tru y,
not: λx:B. r.test x r.fls r.tru}} as Bools'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) → YA 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)