19
$\begingroup$

I hear often that row-polymorphism is a better approach than subtyping, but I have difficulty finding anything comparing them in detail. I'm especially interested in the perspective of a user of the system.

I did come across this blog post, but it leaves me with more questions than before. For example, it makes a claim that a system with subtyping will assign one type, whereas a system with row typing will assign another; does that mean that if a system that purportedly has subtyping assigns the "row typing" type, that it purports incorrectly?

The one major difference I do see is that row typing makes it possible to align the types of arguments (that is, write a two argument function that concerns itself only with the a field of its arguments, but requires that its arguments have the same fields).

$\endgroup$
9
$\begingroup$

Subtyping says given an expression of one type we can give it also another type. We say the former is a subtype of the latter and this subtyping relationship induces many other relationships. In symbols, $$\frac{\Gamma\vdash E:S\qquad S<:T}{\Gamma\vdash E : T}$$

The key thing here (and the reason I reviewed it) is that the same expression is given two different types. In parametrically polymorphic languages with implicit type instantiation we have the following subtyping relationship: $(\forall \alpha.\tau) <: \tau[T/\alpha]$ for all types $T$. If type instantiation is explicit like in System F, this subtyping relationship doesn't hold.

As a bit of an aside, we could say a language with row types (usually) has subtyping relationships of the form $\{\ell_1:A,\ell_2:B\} <: \{\ell_2:B,\ell_1:A\}$ giving rise to $\{\ell_1:A,\ell_2:B\} \cong \{\ell_2:B,\ell_1:A\}$ where $S \cong T \iff S <: T \land T <: S$. However, the way this is actually handled is by changing the notion of equality of types (i.e. unification) so that $\{\ell_1:A,\ell_2:B\} = \{\ell_2:B,\ell_1:A\}$, i.e. they unify. In this case, the subtype relationship is the trivial $T <: T$ one.

Usually when we talk about a language with subtyping we mean one with a non-trivial subtyping relationship on ground types, i.e. types without free variables (which, of course, can and will generate subtyping relationships for non-ground types). So a system with row polymorphism like Roy's is not a language with subtyping in this sense, though it does have the non-trivial subtype relationship that comes from any implicitly instantiated parametric polymorphic language. Structural subtyping, on the other hand, explicitly states non-trivial subtyping relationships for ground types.

By row types, I'll mean having a non-trivial unification as described above or an equivalent. Without this, row types are little more than nested tuples. Note, row types are independent of parametric polymorphism; I do not mean to imply row variables. From the argument about $(\cong)$ above, structural subtyping implies row types but not vice versa. Parametric polymorphism is orthogonal (in the sense the you can have or not have it, there are definitely interactions) to row types or structural subtyping. A system with structural subtyping + parametric polymorphism subsumes row type + parametric polymorphism (assuming some kind of "record union") in the sense that every term in the latter can be typed with the same type in the former. The former is just able to type with additional types as well. Using Brian's example, in a system with structural subtyping and parametric polymorphism answer would have the same type as in the row typing version, but it would also have the subtyping version's type as well.

So you presumably want to compare row type + parametric polymorphism with structural subtyping without parametric polymorphism. The key benefit of the former (and sometimes drawback) is that it allows you to propagate information globally. When $\rho$ gets instantiated to { c : Number }, everything that ever unified with it gets instantiated as well. This may percolate up to the root of your application. Carrying around row variables through large sections of code is not uncommon. Subtyping's approach is to forget information: going from a subtype to a supertype loses (type) information. This can often be what you want: there's a common type you care about and everything else is irrelevant details. My bias is toward maintaining as much type information as possible and only discarding it explicitly. The downsides of subtyping's approach is often evidenced by programs that are type correct but only because types were pushed to a(n informationless) "top" type, e.g. the empty record. Reiterating, parametric polymorphism (in general) preserves type information, subtyping intentionally loses it.

$\endgroup$
  • $\begingroup$ Thank you for the detailed response! Another question: if structural subtyping + parametric polymorphism subsumes row typing + parametric polymorphism, why would you ever use the latter? $\endgroup$ – Alex R Mar 5 '16 at 4:58
  • $\begingroup$ @AlexR As Brian mentioned in his blog post, subtyping interacts extremely poorly with type inference and many other aspects, such as the ergonomic issue I mentioned. There's also implementation and language complexity issues. To be fair there is a broad design space for both "row types" and subtyping, so the "subsumes" is a rough statement. $\endgroup$ – Derek Elkins Mar 5 '16 at 5:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.