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.[1] A row-polymorphic type system and proof of type inference was introduced by Mitchell Wand.[2] [3]
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
\{\ell1:T1,...,\elln:Tn,absent(f1),...,absent(fm),\rho\}
\elli
Ti
i=1...n
fj
j=1...m
\rho
\elli
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:
transform2d:\{x:Number,y:Number,\rho\}\to\{x:Number,y:Number,\rho\}
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
y
Number
\rho
\{x:Number,y:Number,empty\}
x
y
The record operations of selecting a field
r.\ell
r[\ell:=e]
r\backslash\ell
select\ell |
=λr.(r.\ell) : \{\ell:T,\rho\} → T
add\ell |
=λr.λe.r[\ell:=e] : \{absent(\ell),\rho\} → T → \{\ell:T,\rho\}
remove\ell |
=λr.r\backslash\ell : \{\ell:T,\rho\} → \{absent(\ell),\rho\}