It's easy enough to add row polymorphism if there is no subtyping involved. It is an entirely different matter otherwise. 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. This is just like in traditional OOP if a function takes a base class pointer, you can pass a subclass class pointer instead, just that these subtyping relationships are not explicitly defined by users but inferred by the record contents. There is width subtyping and there is also depth subtyping. And we also need awareness of contravariance and covariance.
I implemented the above as a toy type checker. I found the above combination of features too complicated and they end up being unintuitive for the user: the type errors are difficult to comprehend when type errors are found. My implementation is here: https://gist.github.com/kccqzy/d761b8adc840333af0303e1b822d7... and I mostly followed the paper but I cannot guarantee there aren't bugs.
> 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.
> 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.)
> 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.
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.
I implemented the above as a toy type checker. I found the above combination of features too complicated and they end up being unintuitive for the user: the type errors are difficult to comprehend when type errors are found. My implementation is here: https://gist.github.com/kccqzy/d761b8adc840333af0303e1b822d7... and I mostly followed the paper but I cannot guarantee there aren't bugs.