Row polymorphism

This article provides insufficient context for those unfamiliar with the subject. Please help improve the article by providing more context for the reader. (October 2018) (Learn how and when to remove this message)

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]

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]

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 {\displaystyle x} and y {\displaystyle 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 {\displaystyle x} and y {\displaystyle y} fields and nothing else. In this case, a classic record type is obtained.

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.

s e l e c t ℓ = λ r . ( r . ℓ ) : { ℓ : T , ρ } → T {\displaystyle \mathrm {select_{\ell }} =\lambda r.(r.\ell )\;:\;\{\ell :T,\rho \}\rightarrow T}

a d d ℓ = λ r . λ e . r [ ℓ := e ] : { a b s e n t ( ℓ ) , ρ } → T → { ℓ : T , ρ } {\displaystyle \mathrm {add_{\ell }} =\lambda r.\lambda e.r[\ell :=e]\;:\;\{\mathrm {absent} (\ell ),\rho \}\rightarrow T\rightarrow \{\ell :T,\rho \}}

r e m o v e ℓ = λ r . r ∖ ℓ : { ℓ : T , ρ } → { a b s e n t ( ℓ ) , ρ } {\displaystyle \mathrm {remove_{\ell }} =\lambda r.r\backslash \ell \;:\;\{\ell :T,\rho \}\rightarrow \{\mathrm {absent} (\ell ),\rho \}}

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]