Polymorphic recursive objects types in OCaml

Question

Why exactly is this not possible in OCaml:

type 'a cl = < f : 'b . 'b -> 'b cl >;;

From what I've seen so far, universal quantified types are allowed in object types, but my interpreter yields:

Error: In the definition of cl, type 'b cl should be 'a cl

So, is it in general not possible to have this kind of objects or do I miss some special syntax? And what does that (surprisingly specific) message mean?

Answer 1

There are two forms of recursive types in Ocaml:

• Structural recursive types (also called equi-recursive). These arise when you just define a type synonym, like in your case. For these types, recursion has to be uniform, meaning that all recursive occurrences must use the exact same parameters as the left-hand side. (The fact that you attempt to make the method polymorphic actually is irrelevant.)

• Nominal recursive types (also called iso-recursive). These arise from type declarations that have data constructors. In that case, recursive applications are unrestricted. For example:

  type 'a t = C of 'a list t
  

The reason for the restriction in the first case is that structural type definitions are always replaced by their definitions (at least conceptually). If the recursion was not uniform, this unfolding could be infinitely large (technically, such definitions would describe types that are no longer regular trees).

In the nominal case, this problem does not arise, because they define new types, whose definition is never unfolded implicitly. The price to pay is that you have to "coerce" (more accurately, inject and project) explicitly into/out of those types, by means of applying or matching one of their data constructors.

Edit: so, you could try to define your type as a data type:

type 'a cl = Cl of <f : 'b. 'b -> 'b cl>

However, using this obviously is somewhat more verbose, because you have to manage the Cl constructor.