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. 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 fields, are the record fields, and are field values. For example, a record containing a three-dimensional cartesian point could be written as.
The row-polymorphic record type is written as, where possibly or. A record has the row-polymorphic record type whenever the field of the record has the type and does not have any of the fields . The row-polymorphic variable expresses the fact the record may contain other fields than.
The row-polymorphic record types allow us to write programs that operate only on a section of a record. For example,
is a function that performs some two-dimensional transformation. Because of row polymorphism, the function may perform two-dimensional transformation on a three-dimensional point, leaving the z coordinate intact. What is more, the function can perform on any record that contains the fields and with type. Note that there was no loss of information: the type ensures that all the fields represented by the variable 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 and fields and nothing else. Thus, a classic record type is obtained.

Typing operations on records

The record operations of selecting a field, adding a field, and removing a field can be given row-polymorphic types.