It took me some times to find a response to this question that I hope will be suitable and intelligible.
TL; DR : the existential is the limit of the series of types you will define if you use the technique with extensible variants or polymorphic ones. Each time you add a new shape with one of this technique, you end up with a type which has a finite number of shape’s kind., and any of this finite sum type is a subtype of this existential. In others words, any kind of shape you will ever imagine already belongs to this existential sum type.
A little bit more explanation. Consider this module:
module M : sig
type t
int : int -> t
float : float -> t
end = struct
type t = Int of int | Float of float | String of string
let int i = Int i
let float j = Float j
end
The type int
and float
are subtypes of the type M.t
, and the two functions int
and float
are the way we inject them in it. But for sure, there is non useful constructor String
. Even if M.t
is a common supertype of int
and float
, it is not the best one. Among all their common supertypes, the lowest one is their sum (up to isomorphism). With polymorphic variants, there is a built-in notion of subtyping, but it is very restricted: the only isomorphism it considers is the identity.
Now we have a notion of 'a shape_object
, and we can define for instance a point shape_obejct
, a circle shape_object
and so on. Then comes this question: what is the lowest supertype of this infinity of shape_objects
? Answer: the existential I define.
You can think of this existential as a variant with an infinity of constructors. And you can ask: where are this infinity of constructors? Answer: they are here:
to_shape : (module Shape with type t = 'a) -> 'a -> shape
Hence, the constructor for a point is to_shape (module Point)
, the one for a circle is to_shape (module Circle)
, and so on. No need for extensible variants or polymorphic ones to define this infinity of shape’s kind. To define a new shape’s kind you only need to implement a compilation unit that satisfies the Shape
interface and apply the to_shape
constructor.
When I wrote this
[to_shape (module Point) p1; to_shape (module Circle) r1]
it is conceptually similar to this one:
[(p1 :> shape); (r1 :> shape]
in order to define an homogeneous list of shapes.
I hope this time, it is clear to you what this existential really is.