Row polymorphism

In programming language type theory, row polymorphism is a kind of polymorphism that allows one 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 Mitchell Wand.[1][2]

Records and record types

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

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

The row-polymorphic record types allow us to write programs that operate only on a section of a record. For example, ${\displaystyle {\text{transform2d}}:\{x:{\text{Float}},y:{\text{Float}},\rho \}\to \{x:{\text{Float}},y:{\text{Float}},\rho \}}$ 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 ${\displaystyle x}$ and ${\displaystyle y}$ with type ${\displaystyle {\text{Float}}}$. Note that there was no loss of information: the type ensures that all the fields represented by the variable ${\displaystyle \rho }$ are present in the return type.

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

Typing operations on records

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

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

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

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

Notes

1. Wand, Mitchell (June 1989). "Type inference for record concatenation and multiple inheritance". Proceedings. Fourth Annual Symposium on Logic in Computer Science. pp. 92–97. doi:10.1109/LICS.1989.39162.
2. Wand, Mitchell (1991). "Type inference for record concatenation and multiple inheritance". Information and Computation. 93 (Selections from 1989 IEEE Symposium on Logic in Computer Science): 1–15. doi:10.1016/0890-5401(91)90050-C. ISSN 0890-5401.