Row polymorphism

The row-polymorphic record type defines a list of fields with their corresponding types, a list of missing fields, and a variable indicating the absence or presence of arbitrary additional fields. Both lists are optional, and the variable may be constrained. Specifically, the variable may be "empty", indicating that no additional fields may be present for the record.

It may be written as $\backslash \{\backslash ell\_1\; :\; T\_1,\; \backslash dots,\; \backslash ell\_n\; :\; T\_n,\; \backslash text\{absent\}(f\_1),\; \backslash dots,\; \backslash text\{absent\}(f\_m),\; \backslash rho\backslash \}$. This indicates a record type that has fields $\backslash ell\_i$ with respective types of $T\_i$ (for $i\; =\; 1\; \backslash dots\; n$), and does not have any of the fields $f\_j$ (for $j\; =\; 1\; \backslash dots\; m$), while $\backslash rho$ expresses the fact the record may contain other fields than $\backslash ell\_i$.

Row-polymorphic record types allow us to write programs that operate only on a section of a record. For example, one may define a function that performs some two-dimensional transformation that accepts a record with two or more coordinates, and returns an identical type:

$\backslash text\{transform2d\}\; :\; \backslash \{x\; :\; \backslash text\{Number\},\; y\; :\; \backslash text\{Number\},\; \backslash rho\backslash \}\; \backslash to\; \backslash \{x\; :\; \backslash text\{Number\},\; y\; :\; \backslash text\{Number\},\; \backslash rho\backslash \}$

Thanks to row polymorphism, the function may perform two-dimensional transformation on a three-dimensional (in fact, n-dimensional) point, leaving the z coordinate (or any other coordinates) intact. In a more general sense, the function can perform on any record that contains the fields $x$ and $y$ with type $\backslash text\{Number\}$. There is no loss of information: the type ensures that all the fields represented by the variable $\backslash rho$ are present in the return type. In contrast, the type definition $\backslash \{x\; :\; \backslash text\{Number\},\; y\; :\; \backslash text\{Number\},\; \backslash mathbf\{empty\}\backslash \}$ expresses the fact that a record of that type has exactly the $x$ and $y$ fields and nothing else. In this case, a classic record type is obtained.

The record operations of selecting a field $r.\backslash ell$, adding a field $r[\backslash ell:=e]$, and removing a field $r\; \backslash backslash\; \backslash ell$ can be given row-polymorphic 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 \{\ell : T, \rho\}

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

Category:Polymorphism (computer science)