Existential types are dual to universal types. Universal types occur in polymorphic types. Like length val length : 'a list -> int It works for all value

Existential types are dual to universal types. Universal types occur in polymorphic types. Like length val length : 'a list -> int It works for all values 'a. Really, this is better denoted by an explicit binder val length : forall a . a list -> int and this is what the preceeding quote implies---this variable is "bound" by a universal binder. What it means is that the user of `length` gets to make a choice about what the actual value of `a` is. "Existential types" is short for "existentially bound type variables". For this we might write something like val x : exists a . a list which indicates that we have a list containing some values of type `a`... for some, unknown type `a`! In other words, the following are both, simultaneously valid values at type `x` let x : exists a . a list = [1; 2; 3] let x : exists a . a list = ["foo"; "bar"; "baz] The type system has "forgotten" what the type `a` is. In GADT syntax we write these like type ex = Ex : 'a -> ex Because the type `'a` does not get exposed in the final `ex` type it must be "forgotten" and therefore existentially bound. To make it more clear we can determine the type of the following function: let build a = Ex a which is val build : 'a -> ex and should really drive home the idea of just "forgetting" a type.