This article provides insufficient context for those unfamiliar with the subject.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..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.
Records and record types
A record value is written as , where the record contains fields (columns), 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 (for ) and does not have any of the fields (for ). 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 (in fact, n-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.
- 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.
- 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.