Row polymorphism

This article provides insufficient context for those unfamiliar with the subject. Please help by providing more context for the reader. (October 2018) (Learn how and when to remove this template message)

This article needs attention from an expert in Mathematics. The specific problem is: The notation is obscure with no explanation of how n in the first formula relates to n and m in the second formula, or how either can be 0, or what all those extra fields are.. WikiProject Mathematics may be able to help recruit an expert. (October 2018)

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[]