The shape design problem

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.