Thank you for explaining! While I think I understand how your example works and how it's useful, I think I need to read more to understand what “existential types” are, since I’m pretty sure you’re not talking about dudes like Camus. And I’m not totally sure I understand them well enough to write a type checker for them. Which I think means I still don’t really understand GADTs.
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.
