THE EXISTENTIAL TYPE abstract types have existential type — hide the representation, keep the interface
A universal type says “for all a” (the caller picks the type). An existential type says “there exists some a” (the implementation picks it, and hides it): ∃a. {value : a, ops : a → ...}. You pack a concrete representation with the operations that work on it, and the client can unpack and use the operations but can never see or depend on the hidden type. This is exactly a module / abstract data type / object: the representation is sealed behind an interface. Mitchell & Plotkin's slogan says it all — abstract types have existential type.
THE TECHNIQUE pack (hidden rep + ops); the client uses ops, never the rep
A package hides a representation and exposes an operation. The demo unpacks and applies the hidden op — the client sees the result, never the type inside: live demo
HISTORY & CREDIT Mitchell & Plotkin, 1988
“An abstract type is a comment that says don't touch the fields.” — it is a type that makes touching them impossible: the representation is existentially quantified, so no client can even name it. Encapsulation is a theorem, not a convention. cited
1988 · John Mitchell & Gordon Plotkin — “Abstract Types Have Existential Type” (TOPLAS): modules/ADTs as existential quantification. lineage · the type-theoretic account of information hiding (Parnas' modules, CLU clusters). now · ML modules, Haskell exists/GADTs, Rust dyn Trait, every object with a hidden field.
Hide the type and you hide everything that depends on it: the client is forced to program to the interface. Existentials make “you cannot rely on my representation” a fact the checker enforces. Mitchell-Plotkin 1988
RECOMMEND FOR I-13 unpack-and-apply the hidden op, computed
On the canonical compiler, a package hiding square applied to 6 yields 36 — the client uses the op without seeing the representation:
$ i13 run t_existential.i13 # unpack {hidden op} and apply to 6
result = 36 -- client applies the packed op; the type inside stays hidden
Recommend: i13 gets existentials' runtime behavior (a function can close over data a caller never sees — the demo computes 36 through a sealed op) but not its guarantee. Without a type system, “you cannot depend on my representation” is a convention, not a checked fact: nothing stops a caller from reaching around the interface, because to i13 there is no interface, just f64 and arrays. Information hiding as a theorem — the thing existentials buy — is another line under types: NOT COVERED.