Hacker News Reader

> For example if a function needs to take a record containing x as a field with type int, it should also accept a record with y as a field that it does not use.

Not sure if I misunderstand what you mean, but this does not require subtyping. One of the key distinguishing features of row polymorphism is that exactly this can be achieved without subtyping. The extra unused fields (`y` in your example) are represented as a polymorphic type variable _instead_ of using subtyping. See for instance page 7 in these slides: https://www.cs.cmu.edu/~aldrich/courses/819/slides/rows.pdf

Functions that use a field called x but do not use a field called y can use the type {x=int, ... 'a}, right?

The main difficulty I see with row polymorphism is with field shadowing. For example if you have a record with type {a=bool, x=int, c=unit}, then set the x field with type string instead, the new type should be {a=bool, x=string, c=unit}.

I suppose if you only have syntax for creating a record with a literal, but do not have syntax for updating an existing record this is not a problem.

I don't exactly understand your concern, but yes the type {x=int, ... 'a} is valid in a language with row polymorphism but without subtyping. If you do have subtyping, dealing with rest (or spread) is unnecessary. But if you remove subtyping, the unification algorithm isn't powerful enough on its own for many intuitive use cases. The easiest example is if a function takes a list of records all of which need an x field of type int, then you cannot pass it a list of records where all contain the x field of int but some also contain an irrelevant y field and others contain an irrelevant z field.

> if a function takes a list of records all of which need an x field of type int, then you cannot pass it a list of records where all contain the x field of int but some also contain an irrelevant y field and others contain an irrelevant z field.

Can you explain that a little more? Intuitively I would imagine that those y and z fields would 'disappear' into the rest part.

With subtyping, the type checker would understand that the list type is covariant and would accept a record with more irrelevant fields, because that's a valid subtype.

Without subtyping, the rest part needs to be identical for each element of the list. In fact you cannot even express the concept of a list with different rest parts. The key thing to understand is that the rest part never really disappears. The type checker always deduces what the rest part should be in every case. In languages like Haskell you can work around this by using existential quantification but that's a whole different extension to the type system, and one that's certainly not as flexible as full subtyping.

> you cannot pass it a list of records where all contain the x field of int but some also contain an irrelevant y field and others contain an irrelevant z field.

Yes you can - that's just a existential type. I'm not sure what the syntax would be, but it could be somthing like:

  List (exists a : {x=int, ...'a})

(In practice (ie if your language doesn't support existential types) you might need to jump through hoops like:

  List ((forall a : {x=int, ...'a} -> b) -> b)

or whatever the language-appropriate equivalent is, but in that case your list will have been created with the same hoops, so it's a minor annoyance rather than a serious problem.)

Why have subtyping when you have row polymorphism? It seems that there's enough overlap that you should pick one or the other.

My whole point is that subtyping or row polymorphism alone is not enough to assign types to many valid programs that people intuitively write. My example about list of records shows you what happens when you only have row polymorphism without subtyping. See my other comment. (Nothing prevents you from designing such a type system that's slightly inconvenient though: it's really about whether users would want this type system. Haskell and OCaml both have enjoyed user acceptance without subtyping.)

If you were to go the other direction and choose only subtyping but not row polymorphism to implement records, then you end up co-opting things like intersection types inappropriately leading to unsoundness.

Your list of records doesn't require subtyping, it requires information hiding, eg. existential types. Subtyping is too powerful.