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.

History

Row types and row polymorphism were introduced by Mitchell Wand in the late 1980s as an approach to structurally typing extensible records and variants. The principal motivation for rows (and other structural typing paradigms of that time, most notably subtyping relatons) was to safely type emerging object-oriented patterns for object inheritance and extension. More specifically, Wand defined row types in order to model complete type inference for multiple inheritance of objects. As observed by Rémy, Wand's original type inference algorithm was not complete due to an ambiguity in overlap resolution, which was later corrected by both Rémy and Wand. Wand's original system permitted records to be constructed only by extension (that is, one field at a time), but would later show that type inference remains decidable in the presence of record concatenation, albeit without principal types.

While Wand and Remy's initial row type systems supported variant construction, the bulk of attention focused on record extensibility. Gaster and Jones give a more uniform treatment and additionally introduce type constraints on row variables to specify row equality. In contrast to Remy's presence polymorphism, they likewise use the language of qualified types to specify label presence via a lacks predicate.

Blume et al. 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.

In the modern day, row types are most commonly used to type extensible algebraic effects. For example, (Links, Koka) have used row polymorphism as the type basis of an algebraic effects system, aiming for "free composition" of user-defined effects.

Morris and McKinna generalized row types to partial monoids, dubbed row theories, to uniformly handle varying notions of record and variant-eliminator concatenation in a single theoretical framework. For instance, one application may desire concatenation to overwrite existing fields in case of overlapping labels, while another may want to keep both of them accessible (and have one label scope the other). Their system Rose abstracts over arbitrary row theories, where the particular resolution of label overlaps is subject to the meaning of a row combination predicate, ρ1⊕ρ2∼ρ3, which is satisfied precisely when the combination of rows ρ1 and ρ2 is both (1) well-defined and (2) equal to ρ3. This predicate need not be satisfiable in all cases (hence the monoid is partial). For example, it is not always satisfied in row theories barring label overlap. The authors show that type inference remains decidable for their system.

Theory

Row type systems vary by author and have no universally accepted criteria, however it is generally accepted that a row system should at minimum permit rows and (at least one of) record and variant types. Formally, a row is an association of labels to types. When constructing a record, the labels of a row refer to the accessor (or, destructor) names, while the types in the row refer to the output types. For example, a two-dimensional point may be specified by the row

row Point={x:Int,y:Int}

and a record is constructed via the application of the type operator Π (for product) to this row:

p:ΠPoint

p=(x:=1,y:=2)

Dually, when constructing a variant, the labels of a row refer to constructor names, and the types of a row refer to the input types. The Bool type is a simple variant, with constructors true and false and nullary input, as captured by the following row:

row Bool={True:⊤,False:⊤}

(We use the unit type ⊤ to simulate nullary constructors.) The type constructor Σ (for sum) constructs the Boolean variant. Variants are most typically constructed by injection, which can be expressed either explicitly (as done so below) or implicitly (via a subtyping relation and implicit coercions).

true:ΣBool

true=inj(True=tt)

Row polymorphism refers specifically to the quantification of row type variables, which can be specified via a kind system when necessary. For example, record projection is defined polymorphically over rows ρ1 and ρ2 subject to the condition that the output record (constructed via Πρ1) has a subset of the fields in the input record of type Πρ2.

prj:ρ1≤ρ2⇒Πρ2→Πρ1

(The syntax above presumes a qualified type system, in which the predicate ρ1≤ρ2 constrains the type instantiations of the row variable ρ1 to just rows that contain a subset of fields in (the instantiation of) row variable ρ2). Dually, variant injection is defined polymorphically over rows ρ1 and ρ2 subject to the condition that the input variant (constructed via ρ1) has a subset of the fields in the output variant (constructed via ρ2).

inj:ρ1≤ρ2⇒Σρ1→Σρ2

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.

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:T1,…,ℓn:Tn,absent(f1),…,absent(fm),ρ}. This indicates a record type that has fields ℓi with respective types of Ti (for i=1…n), and does not have any of the fields fj (for j=1…m), while ρ expresses the fact the record may contain other fields than ℓ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,ρ}

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. There is no loss of information: the type ensures that all the fields represented by the variable ρ are present in the return type. In contrast, the type definition {x:Number,y:Number,𝐞𝐦𝐩𝐭𝐲} 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.ℓ, adding a field r[ℓ:=e], and removing a field r∖ℓ can be given row-polymorphic types.

selectℓ=λr.(r.ℓ):{ℓ:T,ρ}→T

addℓ=λr.λe.r[ℓ:=e]:{absent(ℓ),ρ}→T→{ℓ:T,ρ}

removeℓ=λr.r∖ℓ:{ℓ:T,ρ}→{absent(ℓ),ρ}

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.

See also

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 (1987). "Complete Type Inference for Simple Objects" (PDF). LICS. pp. 37–44.
  4. ↑ Rémy, Didier (1989). "Typechecking Records and Variants in a Natural Extension of ML". POPL. pp. 77–88. doi:10.1145/75277.75284.
  5. ↑ Wand, M. (1988). "Corrigendum: complete type interference for simple objects". IEEE Comput. Soc. Press: 132. doi:10.1109/LICS.1988.5111. ISBN 978-0-8186-0853-7. {{cite journal}}: Cite journal requires |journal= (help)CS1 maint: periodical has ISBN (link)
  6. ↑ 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.
  7. ↑ Benedict R. Gaster and Mark P. Jones, A Polymorphic Type System for Extensible Records and Variants, Technical report NOTTCS-TR-96-3, November 1996
  8. ↑ Matthias Blume, Umut A. Acar, Wonseok Chae, Extensible programming with first-class cases, ICFP '06
  9. ↑ 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
  10. ↑ Daniel Hillerström, and Sam Lindley. “Liberating Effects with Rows and Handlers.” TyDe 2016. Nara, Japan. 2016. doi:10.1145/2976022.2976033.
  11. ↑ J. Garrett Morris, James McKinna, "Abstracting extensible data types: or, rows by any other name", POPL 2019
  12. ↑ Jones, Mark P. (1992), Krieg-Brückner, Bernd (ed.), "A theory of qualified types", ESOP '92, vol. 582, Berlin, Heidelberg: Springer Berlin Heidelberg, pp. 287–306, doi:10.1007/3-540-55253-7_17, ISBN 978-3-540-55253-6, retrieved 2026-11-08{{citation}}: CS1 maint: work parameter with ISBN (link)
  13. ↑ 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.
  14. ↑ "8 SML# feature: Record polymorphism‣ Part II Tutorials ‣ SML# Document Version 4.0.0 - SML# Project".
  15. ↑ "A Brief History of SML# - SML# Project".
  16. ↑ 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.
  17. ↑ https://www.cl.cam.ac.uk/teaching/1415/L28/rows.pdf, p. 8
  18. ↑ Giuseppe Castagna, Tommaso Petrucciani, Kim Nguyễn, "Set-theoretic types for polymorphic variants", ICFP 2016
  19. ↑ "Polymorphwhat?". 8 December 2017.
  20. ↑ "Static Duck Typing in F# | Compositional IT".
  21. ↑ "Pattern Matching - PureScript by Example".