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?

Disharoon

Answer 1

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.

Synesthesia

Thanks! Never thought about subtyping coercions as universal/existential quantification over row variable... – Disharoon

As a matter of fact, we have means to existential quantification in OCaml; through the usual (but heavy) encoding with a double layer of first-class universal quantifiers in polymorphic record fields, or now through first-class records or GADTs. It is right that in their old Objective ML work, Jérôme Vouillon and Didier Rëmy justified closed types in this way; but note that there are usage different with the other existentials we have: with closed types, both packing and unpacking of existentials are implicit (packing is through (inferred) instantiation), others existentials are more explicit. – Foley

Answer 2

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.

Foley