Row Polymorphism

In programming language type theory, row polymorphism is a kind of
polymorphism that allows one to write programs that are polymorphic on row types such as
record types and polymorphic variants. A row-polymorphic type system and proof of type inference was introduced by Mitchell Wand.

Records and record types

A record value is written as $\$, where the record contains $n$ fields (columns), $\ell_i$ are the record fields, and $e_i$ are field values. For example, a record containing a three-dimensional cartesian point could be written as $Point3d = \$.

The row-polymorphic record type is written as $\$, where possibly $n = 0$ or $m = 0$. A record $r$ has the row-polymorphic record type whenever the field of the record $\ell_i$ has the type $T_i$ (for $i = 1 \dots n$) and does not have any of the fields $f_j$ (for $j = 1 \dots m$). The row-polymorphic variable $\rho$ expresses the fact the record may contain other fields than $\ell_i$.

The row-polymorphic record types allow us to write programs that operate only on a section of a record. For example,
$\text : \ \to \$ is a function that performs some two-dimensional transformation. Because of row polymorphism, the function may perform two-dimensional transformation on a three-dimensional (in fact, ''n''-dimensional) point, leaving the ''z'' coordinate intact. What is more, the function can perform on any record that contains the fields $x$ and $y$ with type $\text$. There is no loss of information: the type ensures that all the fields represented by the variable $\rho$ are present in the return type.

The row polymorphisms may be constrained. The type $\$ 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/math>, and removing a field $r \backslash \ell$ can be given row-polymorphic types.

$\mathrm = \lambda r. (r.\ell) \;:\; \ \rightarrow T$

\mathrm = \lambda r. \lambda e. r ell := e\;:\; \ \rightarrow T \rightarrow \

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

Notes

Polymorphism (computer science)