Row polymorphism

In programming language type theory, row polymorphism is a kind of polymorphism that allows to write programs that are polymorphic on record field types (also known as rows, hence row polymorphism). A row-polymorphic type system and proof of type inference was introduced by Mitchel Wand.

Records and Record Types

A record value is written as $\{\ell _{1}=e_{1},\dots ,\ell _{n}=e_{n}\}$ where the record contains n field (rows), $\ell _{i}$ are the record fields and $e_{i}$ field values. For example, a record containing a three-dimensional cartesian point could be written as $Point3d=\{x=1,y=2,z=3\}$.

The row-polymorphic record type is written as $\{\ell _{1}:T_{1},\dots ,\ell _{n}:T_{n},\mathrm {(} absent)(f_{1}),\dots ,\mathrm {absent} (f_{m}),\rho \}$. A record $r$ has the row-polymorphic record type whenever the fields of the record $\ell _{i}$ have the type $T_{i}$ and does not have the fields $f_{j}$. The row-polymorphic variable $\rho$ expresses the fact the the record may contain other fields than $\ell _{i}$.

The row-polymorphic record types allows as to write programs that operate only on a section of a record. For example, $\mathrm {transform2d} :\{x:\mathrm {Float} ,y:\mathrm {Float} ,\rho \}\rightarrow \{x:\mathrm {Float} ,y:\mathrm {Float} ,\rho \}$ is a function that performs some two dimensional transformation. Because we are use row-polymorphism, the function may perform two-dimensional transformation on a three-dimensional (in fact, n-dimensional) point leaving the z coordinate intact. In fact, the function can perform on any record that contains the fields $x$ and $y$ with type $\mathrm {Float}$. Note that we did not loose any information, the type ensures that all the fields represented by the variable $\rho$ are present in the return type.

The row polymorphims may be constrained. The type $\{x:\mathrm {Float} ,y:\mathrm {Float} ,\mathbf {empty} \}$ expresses the fact that a record of that type has exactly the $x$ and $y$ fields and nothing else. Thus, a classic record type is obtained.

Typing operations on records

The record operations of selecting a field $r.\ell$, adding a field, $r[\ell :=e]$ and removing a field $r\backslash \ell$ can be given row-polymorhic types.

$\mathrm {select_{\ell }} =\lambda r.(r.\ell )\;:\;\{\ell :T,\rho \}\rightarrow T$

$\mathrm {add_{\ell }} =\lambda r.\lambda e.r[\ell :=e]\;:\;\{\mathrm {absent} (\ell ),\rho \}\rightarrow T\rightarrow \{a:T,\rho \}$

$\mathrm {remove_{\ell }} =\lambda r.\lambda e.r\backslash \ell \;:\;\{\ell :T,\rho \}\rightarrow \{\mathrm {absent} (\ell ),\rho \}$