I’m not sure the OP’s problem at hand really needs such an advanced use of OCaml module and type system.
As far as I understand the problem, there is only a finite set of possibilities (namely two), and maybe a simple variant will be sufficient. Something like this:
type t = T1 | T2
(* and then some code that dispatch to the right tool according to the file extension *)
match check_extension file with
| T1 -> (* code using tool1 *)
| T2 -> (* code using tool2 *)
In the case of the shape design problem we have infinitetly many types that share a common behavior. At the heart of my solution there is aristotelian syllogistic, it’s indeed a way to formalise syllogistic in its full generality in OCaml.
At the heart of syllogistic there is the Barbara figure:
- All men are mortal (major)
- All greeks are men (minor)
- All greeks are mortal (conclusion)
And basically, what syllogistic states is that the subtyping relationship is transitive (it’s the meaning of Barbara).
There is also an exemplary version of Barbara where the minor is not a universal proposition, but a singular judgment:
- All men are mortal (major)
- Socrates is a man (minor)
- Socrates is mortal (conclusion)
With OCaml notation, this reasoning can be condensed in this form Socrates : man :> mortal.
In the case of OCaml built-in subtyping relationship, it’s up to the compiler to prove the major (All men are mortal) in order to upcast Socrates to the mortal type. But, it can do it because it considers only what Kant called analytic judgments (and so it’s decidable). Unfortunately, the most interesting majors are those that Kant called synthetic and they are the source of undecidability (see analytic and synthetic judgment in type theory by Per Martin-Löf).
In my solution to the shape design problem, thanks to Curry-Howard, it’s the purpose of the first-class module to be a proof of the major. This way when you wrote:
Shape.make (module Circle : Shape) (c : circle) : shape
you are doing the same syllogism than with Socrates above: the first-class module is a proof of the major (all circles are shapes), the c : circle parameter stands for the minor and therefore you got the conclusion that c is a shape. The Shape.make constructor is a universal structural scheme of all the syllogisms you can do with the shape predicate; and the definition of shape as a GADT only states that a value is a shape if and only if it is the application of this generic scheme to a particular value.
Up to this point, this is similar to OOP, and in fact the type of shape could be defined as an object instead of a GADT (see this thread).
But the most important part is not so much the GADT (or equivalently the object in OOP), it is that you should write generic code against shape not with this interface:
val foo : shape -> foo
but with this one:
val foo : (module Shape with type t = 'a) -> 'a -> foo
(* or with the future modular explicit syntax whose PR is under review *)
val foo : (module S : Shape) -> S.t -> foo
That’s how works the type class system in Haskell, Traits in Rust or Interfaces in Golang. The difference is that in OCaml you have to explicitly pass the proof of the major, whereas in other language it is implicitly instantiated by the compiler (because there can be only one such proof for a given type).
This way you can use the same minor c : circle with as many majors (traits) as you like, which can be very useful from an ecosystem point of view (compare the use of other systems in their respective ecosystems with the use of objects in the Ocaml ecosystem).
let _ = foo (module Circle : Trait1) (c : circle)
let _ = bar (module Circle : Trait2) (c : circle)
(* and so on *)
But, if you start by upcasting your circle in an object according to Trait1 you can’t use it anymore with Trait2 if they are not analytically related (built-in subtyping). Instead, with the more explicit signature, you are upcasting your value only localy in the scope of foo and bar (as if you wrote foo (c : circle :> trait1) and bar (c : circle :> trait2)) without allocating any new object value (as with the built-in :> casting operator that is a no-op).
For a given trait you can study a directed graph of all the majors proofs (the mathematicians called this a category) and there is a particular one that is a truism: All A are A (All shapes are shapes, in the case of the Shape trait). The type that support the module (algebraic structure) of this particular proof is precisely an object in the sense of OOP (the one I defined with a GADT), and this module is called the terminal object of the category: it is useful if you want to upcast different kind of shapes in the same supertype (to put them in a list for instance) as is done in Real World OCaml.
To conclude, I would say that it’s a natural generalisation of what Descartes has done with geometry: he did with algebra what ancient greeks did by reasoning. Descartes laid the foundation stone for a cathedral whose keystone is Curry-Howard.