Existential quantifiers offering an elegant foundation for data abstraction and information hiding.

• An element of $\{\exists X,T\}$ is a value of type $[X\mapsto S]T$ for some type $S$.
• An element of $\{\exists X,T\}$ is a pair, written $\{\ast S,t\}$ of type $S$ and a term t of type $[X\mapsto S]T$

An existentially typed value is introduced by pairing a type with a term, written $\{\ast S,t\}$. (Another common notation is $\mathrm{pack}X=S\mathrm{with}t.$)
The type $S$ is often called the hidden representation type, or sometimes the witness type of the package.

A useful concrete intuition is to think of a value $\{\ast S,t\}$ of type $\{\exists X,T\}$ as a simple form of package or module with one (hidden) type component and one term component.

For example, the package $\{\ast Nat,\{a=5,f=\lambda x:$ Nat. $\mathrm{succ}(x)\}\}$ has the existential type $\{\exists X,\{a:X,f:X\to X\}\}$ (can also has type $\{\exists X,\{a:X,f:X\to Nat\}\}$

The ambiguity shows that , the typechecker cannot make an automatic decision about which existential type a given package belongs to: the programmer must specify which one is intended.

• $p=\{\ast Nat,\{a=5,f=\lambda x:Nat.\mathrm{succ}(x)\}\}\mathrm{as}\{\exists X,\{a:X,f:X\to X\}\}\Rightarrow p:\{\exists X,\{a:X,f:X\to X\}\}$
• $p=\{\ast Nat,\{a=5,f=\lambda x:Nat.\mathrm{succ}(x)\}\}\mathrm{as}\{\exists X,\{a:X,f:X\to Nat\}\}\Rightarrow p:\{\exists X,\{a:X,f:X\to Nat\}\}$