Row polymorphism

In programming language type theory, row polymorphism is a kind of polymorphism that allows one to write programs that are structurally ^[1] (rather than nominally) polymorphic on record types and/or variants. ^[2]

History and theory

A row-polymorphic type system and proof of type inference for records was introduced by Mitchell Wand. ^{[3] [4]}

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. ^[2]

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. ^[5]

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. ^[6] 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. ^{[7] [8]}

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. ^[9]

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. ^[10]

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 ${\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 ${\displaystyle \ell _{i}}$ with respective types of ${\displaystyle T_{i}}$ (for ${\displaystyle i=1\dots n}$), and does not have any of the fields ${\displaystyle f_{j}}$ (for ${\displaystyle j=1\dots m}$), while ${\displaystyle \rho }$ expresses the fact the record may contain other fields than ${\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:

${\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 ${\displaystyle x}$ and ${\displaystyle y}$ with type ${\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 ${\displaystyle \{x:{\text{Number}},y:{\text{Number}},\mathbf {empty} \}}$ expresses the fact that a record of that type has exactly the ${\displaystyle x}$ and ${\displaystyle 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 ${\displaystyle r.\ell }$, adding a field ${\displaystyle r[\ell$ :=e]}, and removing a field ${\displaystyle r\backslash \ell }$ can be given row-polymorphic types.

${\displaystyle \mathrm {select_{\ell }} =\lambda r.(r.\ell )\;:\;\{\ell :T,\rho \}\rightarrow T}$

${\displaystyle \mathrm {add_{\ell }} =\lambda r.\lambda e.r[\ell$ :=e]\;:\;\{\mathrm {absent} (\ell ),\rho \}\rightarrow T\rightarrow \{\ell :T,\rho \}}

${\displaystyle \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# ^[11] and Ocaml.

The very existence of SML#'s first version was motivated ^[12] by adding row polymorphism, based on a SIGMOD '89 paper by Ohori et al., ^[13] 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. ^[14] 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. ^[15]

F# can simulate row polymorphism using its "Statically Resolved Type Parameters" (SRTP) mechanism, ^[16] which has also been informally called "static duck typing". ^[17] 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. ^[18]

Notes

1. https://www.cs.cmu.edu/~aldrich/courses/819/slides/rows.pdf, p. 12
2. François Pottier and Didier Rémy, "The Essence of ML Type Inference", chapter 10 in Advanced Topics in Types and Programming Languages, edited by Benjamin C. Pierce, MIT Press, 2005. pages 389–489. In particular see p. 466 where record types are discussed and p. 483 where polymorphic variants are discussed.
3. 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.
4. 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.
5. Benedict R. Gaster and Mark P. Jones, A Polymorphic Type System for Extensible Records and Variants, Technical report NOTTCS-TR-96-3, November 1996
6. Matthias Blume, Umut A. Acar, Wonseok Chae, Extensible programming with first-class cases, ICFP '06
7. D. Leijen. Koka: Programming with row polymorphic effect types. In P. Levy and N. Krishnaswami, editors, Proceedings 5th Workshop on Mathematically Structured Functional Programming, MSFP, Grenoble, France, April 2014, volume 153 of EPTCS, pages 100–126, 2014
8. Daniel Hillerström, and Sam Lindley. “Liberating Effects with Rows and Handlers.” TyDe 2016. Nara, Japan. 2016. doi:10.1145/2976022.2976033.
9. Ningning Xie, Bruno C. d. S. Oliveira, Xuan Bi, Tom Schrijvers, Row and Bounded Polymorphism via Disjoint Polymorphism, ECOOP 2020
10. J. Garrett Morris, James McKinna, "Abstracting extensible data types: or, rows by any other name", POPL 2019
11. "8 SML# feature: Record polymorphism‣ Part II Tutorials ‣ SML# Document Version 4.0.0 - SML# Project".
12. "A Brief History of SML# - SML# Project".
13. Ohori, Atsushi; Buneman, Peter; Breazu-Tannen, Val (1989). "Database programming in Machiavelli---a polymorphic language with static type inference". Proceedings of the 1989 ACM SIGMOD international conference on Management of data - SIGMOD '89. pp. 46–57. doi:10.1145/67544.66931. ISBN   0-89791-317-5.
14. https://www.cl.cam.ac.uk/teaching/1415/L28/rows.pdf, p. 8
15. Giuseppe Castagna, Tommaso Petrucciani, Kim Nguyễn, "Set-theoretic types for polymorphic variants", ICFP 2016
16. "Polymorphwhat?". 8 December 2017.
17. "Static Duck Typing in F# | Compositional IT".
18. "Pattern Matching - PureScript by Example".