Row polymorphism
![]() | This article provides insufficient context for those unfamiliar with the subject.(October 2018) |
![]() | 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.[1][2]
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.
Notes[]
- ^ 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.
- Polymorphism (computer science)