Row polymorphism crash course

With type inference, structural records types can make a statically typed language feel almost like a scripting language, without giving up type safety:

// Works for any record with the fields width, height : Float
area2d v = v.width * v.height

Row polymorphism can be used to implement this, and can also be used for polymorphic variants, effect systems and stack types in concatenative languages. This post gives a few quick examples of how it works.

Suppose we have two functions that work on row polymorphic records:

f : forall row1. {a: Int, …row1} -> Int
g : forall row2. {b: String, …row2} -> Int

And we want to figure out the type of the following function:

h x = f x + g x

As usual, we instantiate the forall-bound variables — in this case row variables by replacing them with fresh row variables.
The instantiated types for the occurrences of f and g here are thus:

f : {a: Int, …row3} -> Int
g : {b: String, …row4} -> Int

Since x occurs as the argument of both f and g, we know two things about it:

x : {a: Int, …row3}
x : {b: String, …row4}

Thus we must perform unification on those two types:

{a: Int, …row3} = {b: String, …row4}

To solve this, we create a substitution where each of the row variables contain the opposite records fields, as well as a fresh row variable row5:

row3 = {b: String, …row5}
row4 = {a: Int, …row5}

Applying this substitution to the equation above gives us:

{a: Int, b: String, …row5} = {b: String, a: Int, …row5}

Sorting the fields lexicographically by field name gives us syntactically equality:

{a: Int, b: String, …row5} = {a: Int, b: String, …row5}

The final type for h is thus (after generalization):

h : forall row5. {a: Int, b: String, …row5} -> Int

And thus we have inferred a row polymorphic record type by hand.

One thing I like about using row polymorphism for inferring structural types is that it only involves equalities — no inequalities as you get with subtyping, which are much harder to solve for.

Now, what if f and g instead had the same field name, but with different types?

f : {a: Int, …row3} -> Int
g : {a: String, …row4} -> Int

Then we’d need to unify these:

{a: Int, …row3} = {a: String, …row4}

When unifying two records, the types of the common fields are unified, and not included in the substitution of row3 and row4.

In this case, there is exactly one common field a, with a different type on each side. That leads to a unification failure, and thus a type error:

Int = String

We’ve discovered an error in our program! The field a can’t be both an Int and a String.