Row polymorphism

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 \{\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 x and y 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 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.\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 \} == Implementations ==

Row polymorphism is not supported in Standard ML, but is in some extensions or derivatives such as SML# and Ocaml. The very existence of SML#'s first version was motivated by adding row polymorphism, based on a SIGMOD '89 paper by Ohori et al., which introduced the "Machiavelli" extension to SML, although its name was changed later to "SML# of Kansai", before settling on the shorter name. The '#' in the name bears no relationship with F#, but is due to the # operator used to implicitly define the row-polymorphic types on field access. In Ocaml, row polymorphism is used by Ocaml's object types and also by its polymorphic variants. Ordinary record types are not row-polymorphic in Ocaml. Castagna et al. have criticized Ocaml for lacking flow-sensitive typing, which is particularly noticeable in the type inference for polymorphic variants. They also note that since Ocaml lacks true, untagged union types, some of the inferred types for polymorphic variants are too restrictive, in particular when product types are used in combination with polymorphic variants. F# can simulate row polymorphism using its "Statically Resolved Type Parameters" (SRTP) mechanism, which has also been informally called "static duck typing". This however is limited to inline F# functions, so that they are not exported to the .NET type system, which itself does not support such a feature. Row polymorphism is also supported in PureScript. == Notes ==