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