[kccqzy]

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.

[a1369209993]

> 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.)

[hencq]

> 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.

[kccqzy]

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.