I’ve been working on Roy’s new type system which uses a concept called row variables. I’ve also been thinking about TypeScript’s unsound variance issues with its implementation of structural subtyping. That lead to an interesting discussion on Twitter about row polymorphism compared to structural subtyping.

Both are trying to type code like the following:

let f x = x.a + x.b
f {a: 1, b: 2, c: 100}

Also known as static duck typing.

Structural subtyping of course uses subtyping to achieve the above. Subtyping involves the rule of subsumption:

In English: if we have a term t in our environment of type T1 and T1 is a subtype of T2, then that term also has type T2.

In structural subtyping, a wider record type is subsumed by a narrower one. Due to contravariance of function inputs, we can supply any subsumed record to f:

f :: {a: Number, b: Number} -> Number

Row polymorphism instead achieves the original code is by allowing records to have a special polymorphic variable:

The rho (ρ) represents a variable which can be instantiated to extra fields. That means the type of f is:

f :: {a: Number, b: Number | ρ} -> Number

And when we apply f, ρ is instantiated to contain the extra field, c: Number.

So now to answer the question, is row polymorphism a form of subtyping? No, because of the instantiation of the row variable, we can’t derive the rule of subsumption. It would need a separate instantiation step defined and that means there is no subtyping relationship.

Here’s a simple example of where the row instantiation can cause differences:

let f x = x with {sum: x.a + x.b}
let answer = f {a: 1, b: 2, c: 100}

With structural subtyping, the type is upcast to what f needs and we get back:

answer :: {a: Number, b: Number, sum: Number}

But with row polymorphism, the row variable ρ gets instantiated to contain the c field:

answer :: {a: Number, b: Number, c: Number, sum: Number}

Great. Row polymorphism isn’t subtyping. Who cares? Well, subtyping and type inference just don’t mix. Doing type inference with row polymorphic records is much easier. There’s still undecidability problems but if you’re writing a language with type inference and want records, you should take a look at row variables.