Existential Types and Data Abstraction

A universal type \forall X.\,T is a promise to the caller: "give me any type X you like, and I will work." Its dual, the existential type \exists X.\,T, is a promise to the implementer: "there exists some type X — and I know which one, but you, the client, do not — such that this bundle of operations has type T." Existentials are how we give a rigorous, type-theoretic account of data abstraction: abstract data types, modules with hidden representations, and objects that keep their state private.

Consider a counter. Its interface is: a starting value, a way to read it as a number, and a way to increment it. Whether the representation is an integer, a string of tally marks, or a pair of half-bytes is nobody's business but the implementer's. The existential \exists X.\ \{\mathsf{init}:X,\ \mathsf{get}:X\to\mathsf{Nat},\ \mathsf{inc}:X\to X\} captures exactly that: it advertises the operations while sealing the representation type X behind an abstraction barrier. This is the foundation on which every module system and every object is built.

pack builds a package; unpack opens it (abstractly)

A value of existential type is a package: a hidden representation type paired with a term that uses it. You build one with \mathsf{pack}, choosing the concrete witness type S but hiding it behind X:

\dfrac{\Gamma \vdash t : [X \mapsto S]\,T} {\Gamma \vdash \mathsf{pack}\ \langle S,\, t\rangle\ \mathsf{as}\ \exists X.\,T \;:\; \exists X.\,T}\;(\textsc{T-Pack})

You consume one with \mathsf{unpack}, which binds a fresh, opaque type name X and the operations x:T for the scope of the client code — but the client may never learn what X really is:

\dfrac{\Gamma \vdash t_1 : \exists X.\,T \qquad \Gamma,\, X,\, x{:}T \vdash t_2 : U \qquad X \notin \mathrm{FV}(U)} {\Gamma \vdash \mathsf{unpack}\ \langle X, x\rangle = t_1\ \mathsf{in}\ t_2 \;:\; U}\;(\textsc{T-Unpack})

The side condition X \notin \mathrm{FV}(U) — X does not occur free in the result type — is the whole game. It forbids the abstract type from escaping the block. The client can juggle values of type X internally, but it cannot return one, because outside the \mathsf{unpack} the name X is meaningless. That is exactly what makes the representation truly private.

The abstraction barrier, drawn

Picture the package as a sealed box. Above the barrier is the public interface every client may use; below it, hidden, is the concrete representation type and the code that manipulates it. Two different implementations can sit behind the identical interface, and no client can tell them apart — representation independence.

\mathsf{pack} is the act of sealing a concrete representation below the line; \mathsf{unpack} lets a client reach in and use the operations without ever crossing below the barrier. Swap the integer rep for the tally-string rep and every client keeps working unchanged — the promise "there exists some X" was all they ever relied on.

An abstract counter you can run

We encode the existential directly. TypeScript has no pack/unpack keywords, but the Church encoding of existentials gives them to us with universals alone (see the next card): a package is a function that hands its hidden operations to a client which must produce a result without mentioning the hidden type. Two representations — a plain number and a string of tally marks — sit behind one interface.

// The public interface, parameterised by the hidden representation X. type CounterOps<X> = { init: X; get: (x: X) => number; inc: (x: X) => X }; // ∃X. CounterOps<X> encoded as ∀R. (∀X. CounterOps<X> -> R) -> R. type Counter = <R>(client: <X>(ops: CounterOps<X>) => R) => R; // pack ⟨S, ops⟩ : choose the witness S, then hand ops to whatever client comes along. function pack<X>(ops: CounterOps<X>): Counter { return (client) => client(ops); } // Implementation A: represent the count as a number. const intCounter: Counter = pack<number>({ init: 0, get: (x) => x, inc: (x) => x + 1, }); // Implementation B: represent the count as a string of tally marks "|||". const tallyCounter: Counter = pack<string>({ init: "", get: (x) => x.length, inc: (x) => x + "|", }); // A single client. Note: it is polymorphic in X and NEVER returns an X, // so it works identically against either representation. const useThrice = (c: Counter): number => c(<X>(ops: CounterOps<X>) => { let s = ops.inc(ops.inc(ops.inc(ops.init))); // three increments, abstractly return ops.get(s); // read out as a number }); console.log("int counter after 3 incs:", useThrice(intCounter)); // 3 console.log("tally counter after 3 incs:", useThrice(tallyCounter)); // 3 console.log("same observable result — representation independence.");

Both counters report 3. The client cannot distinguish an integer from a tally string because the type X is sealed; all it can do is thread values through the supplied init, inc and get. That indistinguishability is data abstraction, and it is enforced statically by the type of the package.

Existentials from universals

We never needed a primitive \exists: it is definable from \forall by a continuation-passing (double-negation) encoding, exactly as in classical logic \exists X.\,P \equiv \lnot\forall X.\,\lnot P:

\exists X.\,T \;\;\triangleq\;\; \forall R.\ \big(\forall X.\ (T \to R)\big) \to R.

Read it operationally. An existential package is a thing that, for any result type R, takes a client — itself polymorphic in X, so it must work for whatever representation is inside — and delivers the client its answer R. Because the client is universally quantified over X and produces an R that cannot mention X, the representation can never leak. The Church encoding is the \mathsf{unpack} discipline in disguise — and it is precisely the code we ran above.

Largely, yes. The influential slogan "objects are existential types" (Pierce & Turner, building on Abadi & Cardelli) reads an object as a package \mathsf{pack}\ \langle \mathsf{State},\ \{\mathsf{state}=s,\ \mathsf{methods}=m\}\rangle: the internal state type is existentially hidden, and the methods are the only way to poke it. It explains so much — why two objects of the same interface can have wildly different internals, why you cannot generally compare their private state, why "encapsulation" is a type-level guarantee and not just a convention. It also explains a famous friction: with the state type hidden, a "binary method" like equals(other) that needs to see another object's private state becomes genuinely awkward to type — which is why binary methods are a perennial headache in object calculi. The costume fits, but it pinches at the seams.

The single rule that makes existentials abstract rather than merely bureaucratic is the side condition X \notin \mathrm{FV}(U) on \textsc{T-Unpack}: the body's result type U may not mention the freshly-unpacked type name X. Forget it and abstraction collapses. If a client could unpack the counter and then return the raw representation value (type X), some other code would receive a value of a type it cannot name — or worse, two packages that happened to choose the same witness could have their internals mixed. The fresh X is generative: each \mathsf{unpack} invents a brand-new opaque name, distinct from every other, so representations from different packages are provably incompatible even if they are secretly identical. Let X leak and you have a module system in name only.