Row polymorphism

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.

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. It may be written as \{\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 \ell_i with respective types of T_i (for i = 1 \dots n ), and does not have any of the fields f_j (for j = 1 \dots m ), while \rho expresses the fact the record may contain other fields than \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: \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 and with type \text{Number} . There is no loss of information: the type ensures that all the fields represented by the variable \rho are present in the return type. In contrast, the type definition \{x : \text{Number}, y : \text{Number}, \mathbf{empty}\} expresses the fact that a record of that type has exactly the and fields and nothing else. In this case, a classic record type is obtained. The record operations of selecting a field r.\ell , adding a field r[\ell:=e] , and removing a field r \backslash \ell can be given row-polymorphic types. \mathrm{select_\ell} = \lambda r. (r.\ell) \;:\; \{ \ell : T, \rho \} \rightarrow T \mathrm{add_\ell} = \lambda r. \lambda e. r[\ell := e] \;:\; \{\mathrm{absent}(\ell), \rho\} \rightarrow T \rightarrow \{\ell : T, \rho\} \mathrm{remove_\ell} = \lambda r. r \backslash \ell \;:\; \{\ell : T, \rho\} \rightarrow \{\mathrm{absent}(\ell), \rho \}

Text derived from https://en.wikipedia.org/w/index.php?oldid=1354080776 under CC BY-SA 4.0; modifications have been made.