why does OCaml use subtyping for polymorphic variants?

Question

I have just read about row polymorphism and how it can be used for extensible records and polymorphic variants.

However, Ocaml uses subtyping for polymorphic variants. Why? Is it more powerful than row polymorphism?

Answer 1

OCaml uses both row polymoprhism and subtyping for polymorphic variants (and objects, for that matter). Row polymorphism is involved for "open" object types < m1 : t1; m2 : t2; .. > (the .. being literally part of the type), or "open" variant types [> `K1 of t1 | `K2 of t2 ]. Subtyping is used to be able to cast between closed, non-polymorphic types <m1:t1; m2:t2> :> <m1:t1> or [ `K1 of t1 ] :> [ `K1 of t1 | `K2 of t2 ].

Row polymorphism allows to avoid the need for bounded quantification to express types such as "take an object that has at least the method m, and return an object of the same type": subtyping is therefore rather simple, explicit, and cannot be abstracted over. On the contrary, row polymorphism is easier to infer and will play better with the rest of the type system. It should be rarely necessary to use closed types and explicit subtyping, but that is occasionally convenient -- and in particular, keeping type closed can produce error messages that are easier to understand.

Answer 2

To complement Gabriel's answer, one way to think about this is that subtyping provides a weak form of both universal and existential polymorphism. When both directions of parametric polymorphism are available, then the expressiveness of subtyping is mostly subsumed (especially when there is no depth subtyping). But that's not the case in Ocaml.

Ocaml replaces the universal aspect by actual universal polymorphism, but keeps subtyping to give you a form of existential quantification that it otherwise doesn't have. That is needed to form e.g. heterogeneous collections, such as a <a: int> list in which you want to be able to store arbitrary objects that at least have an a method of the right type.

I would go even further and say that, while this is usually explained as subtyping in the Ocaml world, you could actually interpret closed rows as existentially quantified over an (unknown) tail. Coercion via :> would then be existential introduction, thereby staying more faithful to the world of parametric polymorphism that rows are built upon. (Of course, under this interpretation, # would do implicit existential elimination.) If I were to design an Ocaml-like system from scratch, I'd probably try to model it that way.