7
$\begingroup$

I recently came across this blog post by Brian McKenna explaining row polymorphism. This seemed like a wonderful idea to me, but then I realized it smells an awful lot like bounded parametric polymorphism:

With row-polymorphism:

sum: {x: int, y: int | rho} -> int
function sum r = r.x + r.y

With bounded parametric polymorphism:

sum: forall a <: {x: int, y: int}. a -> int
function sum r = r.x + r.y

Can someone clarify the differences to polymorphism between these two approaches?

Improve this question
$\endgroup$
4
  • 2
    $\begingroup$ Have you tried typing let f x = x with {sum: x.a + x.b} with both? If I understand correctly, row-polymorphism will allow you to keep whatever extra fields are in the x but bounded parametric polymorphism will not because you'd want to say that is has type forall a <: {x: int, y: int}. a -> a_with_a_new_field_sum and I don't think you can express a_with_a_new_field_sum. $\endgroup$
    – xavierm02
    Commented Mar 8, 2017 at 10:38
  • $\begingroup$ Hm, I think it depends on that exact semantics of the with construct. Since that wasn't laid out in the article, I tried to avoid it, because it confuses matters. $\endgroup$
    – gardenhead
    Commented Mar 8, 2017 at 14:51
  • 1
    $\begingroup$ Well (I think that) the expressiveness of row polymorphism comes from the fact that you get a name for "and a bunch of other attributes". So if you don't use the type variable representing that bunch of other attributes in the typing of your function, then you probably don't really need row polymorphism. You could also have some forget operator that takes a record and removes one of its fields. Then, to type fun r -> forget x of r, you'd probably also need row polymorphism. $\endgroup$
    – xavierm02
    Commented Mar 8, 2017 at 15:07
  • $\begingroup$ Without more detail about the systems, I'd say they roughly are equivalent except, of course, bounded polymorphism is more general. Usually row typing also implies some type level operations on rows such as row union or row restriction. I say similar sorts of things in this answer. $\endgroup$
    – Derek Elkins left SE
    Commented Mar 9, 2017 at 4:58

1 Answer 1

Reset to default
3
$\begingroup$

So, there are a few differences:

  • In row polymorphism, you've bound $\rho$ to a name, so you can use it elsewhere. For example, forall rho . rho -> {x : int | rho} is expressible with row polymorphism, but not purely using bounded polymorphism. Likewise, you can even express field deletion this way: forall rho .{x : int | rho} -> rho is a perfectly valid row-polymorphic type, but subtyping doesn't really have a way of expressing this.

    Because row polymorphism lets you add and delete fields this way, usually it works with a "stack" semantics, so that old fields are shadowed when new fields of the same name are added.

  • Bounded subtyping uses, well, subtyping. So with row polymorphism, you can't give x : {x : int, y : int} as argument to a function of type {x : int} ->int. But most systems with bounded subtyping would have non-polymorphic subtyping too, that would allow this, since most systems have {x : int} <: {x : int, y : int}.

Bounded subtyping tends to be bit more precise and flexible, and the "stack" semantics of row polymorphism don't arise that much. But inference is much easier for row polymorphism, and can work in the absence of any type annotations (for example, in Elm), which usually isn't the case in the presence of subtyping.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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