In programming language type theory, row polymorphism is a kind of polymorphism that allows one to write programs that are structurally (rather than nominally) polymorphic on record types and/or variants.
History and theory A row-polymorphic type system and proof of type inference for records was introduced by Mitchell Wand. The theoretical treatment of row polymorphism is somewhat complicated by the need to have distinct labels in a record. One approach, taken by Rémy and colleagues (and implicitly present in the presentation below, which is heavily inspired by Wand's), is to consider different kinds of row types, depending on their labels. Gaster and Jones unformely extended the approach to variants as well, by making both the record and variant type constructor map from row kinds to types. Blume et al. proposed to take the approach one step further into the realm of composable extensions by adding "first-class cases" handled by a LetCC construct to compose continuations in the case-matching code. Then, a couple of projects (Links, Koka) have used row polymorphism as the type basis of an algebraic effects system, aiming for "free composition" of user-defined effects. Another approach to the issue of unique labels is to extend system F with a "coherent merge" operator, resulting in calculi with so-called disjoint intersection types. Morris and McKinna generalized row types to row theories to uniformly handle varying notions of (record) extension in a single theoretical framework: for instance one application may desire the operation of extension to overwrite existing fields in case of matching names, another may want to keep both of them accessible, possibly some path-based addressing scheme etc.
Row-polymorphic record type definition 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 { ℓ 1 : T 1 , … , ℓ n : T n , absent ( f 1 ) , … , absent ( f m ) , ρ } {\displaystyle \{\ell _{1}:T_{1},\dots ,\ell _{n}:T_{n},{\text{absent}}(f_{1}),\dots ,{\text{absent}}(f_{m}),\rho \}} . This indicates a record type that has fields ℓ i {\displaystyle \ell _{i}} with respective types of T i {\displaystyle T_{i}} (for i = 1 … n {\displaystyle i=1\dots n} ), and does not have any of the fields f j {\displaystyle f_{j}} (for j = 1 … m {\displaystyle j=1\dots m} ), while ρ {\displaystyle \rho } expresses the fact the record may contain other fields than ℓ i {\displaystyle \ell _{i}} . 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 , ρ } → { x : Number , y : Number , ρ } {\displaystyle {\text{transform2d}}:\{x:{\text{Number}},y:{\text{Number}},\rho \}\to \{x:{\text{Number}},y:{\text{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 and y with type Number {\displaystyle {\text{Number}}} . There is no loss of information: the type ensures that all the fields represented by the variable ρ {\displaystyle \rho } are present in the return type. In contrast, the type definition { x : Number , y : Number , e m p t y } {\displaystyle \{x:{\text{Number}},y:{\text{Number}},\mathbf {empty} \}} expresses the fact that a record of that type has exactly the x and y fields and nothing else. In this case, a classic record type is obtained.
Typing operations on records The record operations of selecting a field r . ℓ {\displaystyle r.\ell } , adding a field r [ ℓ := e ] {\displaystyle r[\ell :=e]} , and removing a field r ∖ ℓ {\displaystyle r\backslash \ell } can be given row-polymorphic types.
… excerpt ends here. Continue reading the full article.
