Refined subtyping and row variables for record types

Draft of December 26, 1996

Didier Rémy INRIA-Rocquencourt^{∗}

Abstract We compare the row variables and subtypes for record types. We show that they are orthogonal to one another and that record types benefit from having both at the same time. We proposed a unifying framework of record types, and show that the several advantages of using an enriched latice of subtypes for record types, in particular this allows for extensible objects in the presence of subtyping.

1 Introduction

Subtyping was introduced by Cardelli 1994 as a means to provided multiple inheritance for object-oriented languages. Objects were seen as simple record of functions. We will take adavantage of this view of objects (now considered as naive), since the strcuture of types is not much affected by the differences. We will base our discussion on record types but we will also illustrate the differences by examples involving objects.

The type of the record {ℓ_{1} = 1, ℓ_{2} = t} is “the record of types” {ℓ_{1} : I, ℓ_{2} : B}. But it is also correct to forget fields of records, and the same record can also be assigned type {ℓ_{1} = 1}. So we could give the following typing rule for records

(Record-Sub)

\frac{A ⊢ a_{i} : τ_{i} ∀i ∈ I J ⊂ I}{A ⊢ \{ℓ_{i} = a_{i}, i ∈ I\} : \{ℓ_{i} : τ_{i}, i ∈ J\}}

A more flexible alternative consists in introducing a subtyping relation between record types.

(Record) ; \frac{A ⊢ a_{i} : τ_{i} ∀i ∈ I}{A ⊢ \{ℓ_{i} = a_{i}, i ∈ I\} : \{ℓ_{i} : τ_{i}, i ∈ I\}}(Sub) ; \frac{A ⊢ a : τ  τ ≤ τ′}{A ⊢ a : τ′}

Intuitively, a record with more fields should be usable whereever a record with fewer fields is required. This leads to the subtyping rule:

\frac{J ⊂ I}{\{ℓ_{i} : τ_{i}, i ∈ I\} ≤ \{ℓ_{i} : τ_{i} ∈ J\}}

(≤-Record-Width)

∗Author’s address: INRIA-Rocquencourt, B.P. 105, F-78153 Le Chesnay Cedex. Email:

Didier.Remy@inria.fr

Using rules record and Sub we can derive that the record defined above has type {ℓ_{1} : I}. The previous subtyping rule is certainly sound. However, it only defines witdth-subtyping. Another possibility for two record types to be in a subtyping relation is that they have the same fields and that their fields are themselves in a subtyping relation.

(≤-Record-Depth)

\frac{τ_{i} ⊂ τ′_{i} ∀i ∈ I}{\{ℓ_{i} : τ_{i}, i ∈ I\} ≤ \{ℓ_{i} : τ′_{i}, i ∈ I\}}

Depth-subtyping also correspond to structural subtyping. Having both of them at the same time is no problem and corresponds in fact to the general subtyping relation of Amber, which has been widely. We will call plain-subtyping this subtyping relation. Plain subtyping is also use for object types in “A theory of primitive objects” [AC94] although variance through self types is more complicated. Lately, there has been several proposal for either restricting subtyping or at least distinguishing between width and depth subtyping. In particular in object types, plain subtyping would be unsound with object extension [?].

When record subtyping was introduced in Amber, it was still an open problem how one could keep type inference with both subtyping and polymorphism, and Amber was a monomorphic language. Wand proposed to used row variables [Wan87] instead of subtyping to provide polymorphic access to record fields. By avoiding a subtyping relation, row variables should allow for type inference. Wand’s idea have been formalized under some restrictions in [JM88, OB88] and solved in the general case in [Rém93b] using a kinded algebra of types taken modulo equations. A very similar proposal, known as tagged types has been used in the language LCS to type processes [Ber93]. In fact, an important issue [?] was to give a more explicit structure of record types. In praticular record type should provide type information for all fields wether they were present or absent. Absent played the role of a top type for fields that existed implicitly when using subtypes. The record introduced earlier is given type

{ℓ_{1} : Pre (I), ℓ_{2} : Pre (B); Abs}

saying that on fields a and b the record is defined and carries values of type I and B and on other fields it is undefined. The type information, here Abs, placed on the rightmost and without any associated label in a record type describes the type of all fields that have not been explicitly mentionned on its left.

The simplest of the record operations is polymorphic access. We say that a language with records has polymorphic access given any field, it is possible to write a function fun r → r.ℓ that can access records with different set of fields, but at least field ℓ. In object-oriented languages, polymorphic access is the basic mecanism for sending messages to object with different interfaces. ML implementations do not usually provide polymorphic access, but simple records. Subtypes and row variables can both type polymorphic access, respectively with types:

{ℓ : α} → α {ℓ : α; α′} → α

In the former case, the domain is the smallest possible type. Then any possible argument should have a type which is a subtype of {s : τ}. With the variables, the type is implicitly quantified on variables α′ (and also α) and the domain of all its instances range other all possible types for the argument.

At first glance, row variables and subtypes might be considered as two equivalent alternative for typechecking polymorphic access. However, as soon as their expressive power is tested on other kinds of record operations it appears that they describe orthogonal aspects of record types. While the use of subtyping is more flexible, since for instance records of incompatible domains can be put in the same list, its fails with extensible records. Polymorphic extension is the ability to write a function fun r x → r @ {ℓ = x} that extends any record on field ℓ, possibly overriding it. This function can be given type

{ℓ : α; α′} → α′′ → {ℓ : Pre α′′; α′}

It says that whatever field ℓ was in the argument record, the result will posses a field ℓ with type α′′, otherfields been unchanged. With subtypes, it is only possible to type a restriction of this function, which simply overrides field ℓ with a value of the same type. Moreover, it requires the use of bounded-quantification.

∀ α′ ≤ {ℓ : α}. α′ → α → α′

The restriction is very strong since it also forces the updated value to be of the same type. There has been a few proposals for adding some form of row variables to records with subtypes, but most of them used and ad hoc approach [?, HP90, ?]. These proposal simultaneously added some kind negative information that enables to tell that a record value does not posses a field. Similar features have also been added to object types so that both subtyping and object extension could cohabitate [?]. Other extensions have also proposed adding polarity to the types of record fields that expresses the ability to read or write their fields. Such refinement usually enables more arrow types to be in a subtyping relation [KPT95, ?].

In this article, we show that most versions of record types can be presented in a unifyied framework. Viewing record types as total vs. partial function from labels to types is always preferable. It first allows to solve the problem for one-field records, the solution extending in most cases to multiple-field records in a systematic way. This view does not require row variables although they appear very naturally. Reducing the problem to one-field records also points out a misunderstanding of record types. A more refined structure appears naturally, and transported to multiple fields records, it will provide better solution for existing problems. Another advantage is the separation of two different concepts in record types. The step provides restricted infinite product of fields. The second step provide subtyping on fields. That is subtyping is defined at the level of fields and derived for records by general structural rules.

In section ??, we summarized the ideas behind row-variables, and illustrates their power on examples. In section 3, we focus on the classical approach with plain subtypes. We will introduce a syntactic translation of record types into the row variables presentation (without using row-variables). In section 4 we show that records with both subtypes and row variables are strictly more powerful. Even though, enriching the lattice of types will allow for typing more constructs (section ). Last, we consider row variables and subtyping in higher order type systems in section .

2 Row Variables

The concept of row variables have been introduced by Mitchell Wand [Wan87]. We present here row variables of [Rém89] that formalize Wand’s idea without any restriction. In fact, a more detailed presentation can be found in [Rém93b] and the underlying theory of record algebras in [Rém93a] and [?] shows how ML type inference can be extended to cope with record types. An intuitive introduction to record types is given in [Rém89, Rém93a]. We will keep here to introduce the essential ideas of record types.

We summarize the intuition on the following example. describe the types involved in the application of the function fun r → r.ℓ to the record {a = 1; b = t}. Let τ be the type of the record and τ′ → τ′′ the one of the function. We first asume that the set of labels is reduced to a and b. In a first approximation, records are pairs. However, records have the ability to forget fields. Therefore, each component of the pair type should say explicitly whether the field they represent is accessible or not.

The solution [Rém93b] does not just rely the idea of row variables. In order to avoid confusion, we will call them explicit record types. The most important idea is that records types should be considered as total functions from the set of labels to the set of types. There are not any such functions, though. First, they have only a finite subdomain whose fields are given explicitly while on the rest of the domain all images are isomorphic. This allows for a finite representation of record types as described

{ℓ_{1} : τ_{1}; … ℓ_{n} : τ_{n}; τ}

The first part lists explicit fields with their types; the last component τ, and τ is a row that describe the type of the other fields. Explicit record types are also restricted in another way since types of fields are of another sort that usual types. For a given field ℓ_{i}, τ_{i} must first tell whether a record of that type must have a field ℓ_{i} and if such what type of value it is carrying on that field or may not be defined on that field. Last, a variable would mean either option is possible. The structure of field types is thus

τ ::= Pre τ | Abs | α

The row τ of the above type is also distinguished. Technically, it could be any of the above three alternatives as well, but one is would allow for inhabited types since a record value can never be defined on all fields. Since it slightly simplifies the presentation, we will assume that the structure of templates is simply

τ ::= Abs | α

Variable α is a so-called row variable. It is important that row variables are no the essential idea here, but just comes naturally as a consequence of view record types by field-by-field. For instance, we shall see below that row variables are optional and removing them in the above definition makes record types isomorphic to the more standard notation.

In general, the expression {(ℓ : τ_{ℓ})_{ℓ∈I}; τ′_{∞}} should be read as

∏_{ℓ∈L} (ℓ : \{ \begin{matrix}τ_{ℓ} & if ℓ ∈ I \\ τ′_{ℓ} & otherwise, where τ′_{ℓ} is a copy of τ′_{∞} \end{matrix} )

We have shown in the introduction the types of {a = 1, b = t} and the function fun x → x.ℓ. They are respectively

{a : Pre (I); b : Pre (B); Abs} {a : Pre α; α′} → α

In ML, in order the function to the record, we need the two types {a : Pre α; α′} and {a : Pre (I); b : Pre (B); Abs} be identical. This is the case after subtituting α′ by (b : Pre (B); Abs). We may also need to read the type of a record on that it does not explicitly mention. For instance, we could try to exptend this record on field c. We should of course say that the record also has type {a : Pre (I); b : Pre (B); c : Abs; Abs}. In ML, without subtyping, the option is to identify its two types by adding the equation Abs = (ℓ : Abs; Abs) for any^{1} label ℓ.

Formally, the language of types is

τ ::= α | τ → τ | {τ} | ℓ : τ; τ | Abs | Pre τ

However, the formation of types is twice rectricted by sorts. The first signature, build over the atomic sorts T ype and F ield is:

\begin{aligned}( → ) & :: T ype × T ype ⇒ T ype \\ \{ \} & :: F ield ⇒ T ype \\ (ℓ : ; ) & :: F ield × F ield ⇒ F ield \\ Pre ( ) & :: T ype ⇒ F ield \\ Abs & :: F ield \end{aligned}

The second restriction is by the signature built over atomic sorts T ype and Row(L) where L range over finite sets of labels. The sort Row(L) say for row expressions what labels they should not define.

\begin{aligned}( → ) & :: T ype × T ype ⇒ T ype \\ \{ \} & :: Row(∅) ⇒ T ype \\ (ℓ : ; ) & :: T ype ⊗ Row(ℓ.L) ⇒ Row(L) \\ Pre ( ) & :: T ype ⇒ T ype \\ Abs & :: u ⇒ u \end{aligned}

In the sort of present, u stands for any sort. This signature is overloaded. Howver, symbols could be superscript with their sort so that the signature is not overloaded any more. Moreover, given a type an a sort, there would be at most one annotation of the superscript so that the type is well-formed. This shows that in any context were the sort is known, superscript can be inferred. For simplicity of presentation we omit superscripts. More details can be found in [Rém93a]. It is also important to say that variables can be of any kind.

Types are also taken modulo the equations

ℓ_{1} : τ_{1}; (ℓ_{2} : τ_{2}; τ) = ℓ_{2} : τ_{2}; (ℓ_{1} : τ_{1}; τ) Abs = (ℓ : Abs; Abs)

Remark in the last equation that the sorts of all occurences of Abs are different in this equation. The first equation is left commutativity and simply means that fields can be reordered.

We can now shows what programs row variables can types and where they fail.

3 Plain Subtypes

With plain subtyping, types have the more implicit structure {ℓ_{1} : τ_{1}, … ℓ_{n} : τ_{1}} where non listed fields are visible with type as specified and other fields are non visible. Implicit record types are also identified modulo reordering of fields.

1This is not quite true, since each template is given a sort saying what labels it does not represents. Then label ℓ should not belong to the sort of Abs it expands

Implicit record types are in fact a subcase of explicit record types, since they are isomomorphic to the subset of explicit record types that do no use any row variable (i.e. variables of the kind Row(L)). The encoding is quite obvious: it represents {ℓ_{1} : τ_{1}, … ℓ_{n} : τ_{n}} as {ℓ_{1} : τ_{1}; … ℓ_{n} : τ_{n}; Abs} and it is homomorphic on all other symbols. The encoding clearly preserve the equality, and it is in fact an isomomorphism if we restrict the image to types of the sort T ype (but we allow subterms of other sorts).

We show that this isomorphism is compatible with the usual ordering of implicit record types. That is, the ordering induced by the translation can be defined at a lower level as an ordering between types of fields and lifted to record types by congruence.

The plain subtyping relation is defined as the smallest relation such that:

(≤-Record-Width)

\frac{J ⊂ I}{\{ℓ_{i} : Pre τ_{i}, i ∈ I; Abs\} ≤ \{ℓ_{i} : Pre τ_{i}, i ∈ J; Abs\}}

(≤-Record-Depth)

\frac{τ_{i} ≤ τ′_{i} ∀i ∈ I}{\{ℓ_{i} : Pre τ_{i}, i ∈ I; Abs\} ≤ \{ℓ_{i} : Pre τ′_{i}, i ∈ I; Abs\}}

(≤-Arrow) ; \frac{τ′_{1} ≤ τ_{1} τ_{0} ≤ τ′_{0}}{τ_{1} → τ_{0} ≤ τ′_{1} → τ′_{0}}

We can replace the width and depth subtyping rules by

(≤-Field) ; \overline{Pre τ ≤ Abs}

(≤-Pre)

\frac{τ ≤ τ′}{Pre τ ≤ Pre τ′}

(≤-Record) ; \frac{τ_{i} ≤ τ′_{i} ∀i ∈ I τ ≤ τ′}{\{τ_{i}, i ∈ I; τ\} ≤ \{τ_{i}, i ∈ I; τ\}}

Remark that the two right rules are strandard structural rules. These rules define the same inclusion relation between regular types (the also allow inclusion between types of the sort Field). For sake of comparison, we will use only explicit record types for now on.

4 Unifying row variables and subtypes

We have shown that plain subtypes can be viewed as removing row variables from explicit subtypes then by adding a subtyping relation. We have also given evidence that explicit records types without subtyping and plain subtyping are incomparable. It is then natural to have both row variables and subtyping at the same time in explicit record types. We obtain a strictly more powerful language.

5 Better subtypes

When adding subtyping to explicit record types, we have in fact lost the important property of knowing the exact shape of values from its type. Indeed a record of type {ℓ : Pre I; Abs} must have a ℓ field and no other field at all. So it is a value of the form {ℓ = }. This is important in several situations, since it may provide better documentations, or also allow for more optimizations. It is also essential for some operations on records, for instance the concatenation of two records may be typed as long as the type of the second one is known

Plain subtyping invalidate these nice properties. However, this no not due to subtyping itself, but the way we added subtyping by translation from implicit record types. Working directly with expplicit records types, it would have been more natural to keep Abs and Pre τ two incompatible types but allow both of them to be coerced to a new type symbol Either Graphically:

τ ::= … | Either

                                                Either

[figure]

                                           Abs        Pre τ

The subtyping rule ≤-Field is replaced by

                         (≤-Abs) ; \overline{Abs ≤ Either}

(≤-Pre)

                                     Pre τ ≤ Either

As we mentionned earlier, row terms may be restricted by the sorts to be only Abs or variables. Therefore, the preceeding rules only concerns types that are not row expressions.

We can type both programs that could be typed earlier. We can also type more. This diagram has been used in typing record concatenation in the famework of constrained types [?].

A similar subtyping relation is used for objects in [AC94], although only width subtyping is allowed. Width-only subtyping of records is obtained by removing rule ≤-Pre: as a result two types of the shape Pre τ and Pre τ′ can only be equal if τ and τ′ are. In [AC94], object update only is possible:

\frac{A ⊢ a : \{ℓ : Pre τ_{i}; α\} A ⊕ (x ↦ \{ℓ : Pre τ_{i}; α\}) ⊢ b : \{ℓ : Pre τ_{i}; α\}}{A ⊢ a ← ς(x) b : \{ℓ : Pre τ_{i}; α\}}

The typing rule

\frac{A ⊢ a : \{ℓ : Either; α\} A ⊕ (x ↦ \{ℓ : Pre τ_{i}; α\}) ⊢ b : \{ℓ : Pre τ_{i}; α\}}{A ⊢ a ← ς(x) b : \{ℓ : Pre τ_{i}; α\}}

for object extension would be unsound, because it could be the case that some field has been forgotten and in fact the object update rule should be used, forcing the type of the updated field to be unchanged.

Refined subtyping allows for object extension as well. The typing rules is:

\frac{A ⊢ a : \{ℓ : Abs; α\} A ⊕ (x ↦ \{ℓ : Pre τ_{i}; α\}) ⊢ b : \{ℓ : Pre τ_{i}; α\}}{A ⊢ a ← ς(x) b : \{ℓ : Pre τ_{i}; α\}}

The fact that field ℓ has type Abs now garantees that field ℓ has never been provided. The two rules for object update and object extension can be factorize provided the subtyping relation is yet richer:

τ ::= … | Maybe τ

                                                Either

|^{}

                                                Maybe τ

[figure]

                                           Abs         Pre

It allows to forbid the presence, but reminds the type with which the field has possibly been defined.

\frac{A ⊢ a : \{ℓ : Maybe τ; α\} A ⊕ (x ↦: \{ℓ : Pre τ_{i}; α\}) ⊢ b : \{ℓ : Pre τ_{i}; α\}}{A ⊢ a ← ς(x) b : \{ℓ : Pre τ_{i}; α\}}

Thanks to row variables it is now possible to see update as a primitive with the best type:

{ℓ : Maybe α; α′} → α → {ℓ : Pre α; α′}

A further step allows the combination of width and depth subtyping:

τ ::= … | Pre^{+} τ

                                              Either

[figure]

                                                      Pre^{+} τ

[figure: ^{·····}; ·····]

                                       Maybe τ  Pre^{+} τ′

\begin{matrix} \\ | \\ | \end{matrix}
[figure: |]

                                 Abs           Pre τ  Pre τ′

The typing rule for sending messages should now be

\frac{A ⊢ a : \{ℓ : Pre^{+} τ; α\}}{A ⊢ a.ℓ : τ}  instead of  \frac{A ⊢ a : \{ℓ : Pre τ; α\}}{A ⊢ a.ℓ : τ}

That is, subtyping is covariant between (Pre^{+} ) types but invariant between (Pre ) types. In fact, the types Pre^{+} τ and Pre τ encodes the notion of variance introduced in in [AC95] for object types; moreover, in [AC95] fields of object types can also be contra-variant. We could encode them by introducing a new symbol (Pre^{−} ), with a covariant structural typing rule. (Pre^{−} τ) is a also supertype of Pre τ and a subtype of Either. Since variances are carried by fields, the record (or object) constructor { } is itself covariant in all components, and variables ranging other fields whatever their variance do make sense.

Refined subtyping allows for more precise information on object types. Subtyping is obtained through smaller steps which enables types to keep track of how much subtyping has been used, i.e. the compile time type may be from the best possible runtime type. Refine subtypings makes it possible to know where deep subtyping has no been been used and therefore allows for deep subtyping and object update and extension simultaneously. In [AC94], subtyping is only possible between self types, of the form ς(α){τ}, because the ς quantifier will prevent from any further extension. However, this is more restricted that when using refined types the control of refined types acts field-by-field rather than on the whole record. Moreover ς is a quantifier and ς-types are second-order types, which make type inference non obvious, while type inference with refined types should be possible using type constraints.

Another information that has sometimes been added to fields of implicit record types are polarities. They can clearly be added to explicit record types and carried by Pre constructors in a similar fashion.

6 Higher-order types

We have ignored the underlying language of types as much as possible in the previous discussion. There are two interesting type systems where polymorphism and subtypes are merged: constrained types and F_{≤}^{Ω}.

Adding row-variables to types of system F should not be a problem.

7 Conclusion

We have shown that row variables and subtypes are two orthogonal formalism, and both enrich records types in incomparable ways, and are fully compatible. That is, record types gain more powerful types in having simultaneously subtyping and row variables. We have argued that record types should be thought of as infinite products on all fields with only a finite number of distinguished fields, and that the includion relation should be defined field-by-field. We have also shown how the subtyping relation could be refined in interesting ways, while independantly keeping the powerful row-variables.

Row variables and refined record types often allow primitive contructions of the language such as record or object extension to be treated as primitive polymorphic constants and typed as such.

References

[AC94] Martín Abadi and Luca Cardelli. A theory of primitive objects. In International Symposium on Theoretical Aspects of Computer Software, April 1994.

[AC95] Martín Abadi and Luca Cardelli. An imperative object calculus. In P.D.Mosses, M.Nielsen, and M.I.Schwartzbach, editors, Theory and Practice of Software Development, number 915 in Lecture Notes in Computer Science, pages 471–485. Springer-Verlag, May 1995.

[Ber93] Bernard Berthomieu. Tagged types, a theory of order sorted types for tagged expressions. Research Report 93083, LAAS, 7, Avenue du Colonnel Roche, 31077 Toulouse, France, March 1993.

[GM93] Carl A. Gunter and John C. Mitchell. Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design. The MIT Press, 1993. To appear.

[HP90] Robert W. Harper and Benjamin C. Pierce. Extensible records without subsumption. Technical Report CMU-CS-90-102, Carnegie Mellon University, Pittsburg, Pensylvania, February 1990.

[JM88] Lalita A. Jategaonkar and John C. Mitchell. ML with extended pattern matching and subtypes (preliminary version). In Proceedings of the ACM Conference on Lisp and Functional Programming, pages 198–211, Snowbird, Utah, July 1988.

[KPT95] Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner. Linearity and the pi-calculus. Extended abstract, 1995.

[OB88] Atsushi Ohori and Peter Buneman. Type inference in a database langage. In ACM Conference on LISP and Functional Programming, pages 174–183, 1988.

[Rém89] Didier Rémy. Typechecking records and variants in a natural extension of ML. In Proceedings of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, pages 242–249. ACM, January 1989. To appear in [GM93].

[Rém93a] Didier Rémy. Syntactic theories and the algebra of record terms. Research Report 1869, Institut National de Recherche en Informatique et Automatisme, BP 105, F-78 153 Le Chesnay Cedex, 1993.

[Rém93b] Didier Rémy. Type inference for records in a natural extension of ML. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects Of Object-Oriented Programming. Types, Semantics and Language Design. MIT Press, 1993.

[Wan87] Mitchell Wand. Complete type inference for simple objects. In D. Gries, editor, Second Symposium on Logic In Computer Science, pages 207–276, Ithaca, New York, June 1987. IEEE Computer Society Press.