Operations on Records (Extended Abstract)^{∗}

Luca Cardelli Digital Equipment Corporation Systems Research Center

John C. Mitchell Department of Computer Science Stanford University

August 26, 1989

Abstract

We define a simple collection of operations for creating and manipulating record structures, where records are intended as finite associations of values to labels. We study a second-order type system over these operations, supporting both subtyping and polymorphism. Our approach unifies and extends previous notions of records, bounded quantification, record extension, and parametrization by row-variables. The general aim is to provide foundations for concepts found in object-oriented languages, within the framework of typed lambda-calculus.

1 Introduction

Object oriented programming is based on record structures (called objects) intended as named collections of values (attributes) and functions (methods). Collections of objects form classes. A subclass relation is defined on classes with the intention that methods work “appropriately” on all member of subclasses of a given class. This property is important in software engineering because it permits after-the-fact extensions of system by subclasses, without having to modify the systems themselves. The first object oriented language, Simula67, and most of the more recent ones are typed by using simple extensions of the type rules for Pascal-like languages, mainly involving a notion of subtyping. We are interested in more powerful type systems, particularly ones that incorporate parametric polymorphism and integrate it smoothly with subtyping.

Several other type systems for record structures have been formulated recently, following the same motivation. In [Car88], the basic notions of records types were defined in the context of a first-order type system for fixed-size records. Then Wand [Wan87] introduced the concept of rowvariables while trying to solve the inference problem for records; this led to a system with extensible records and limited second-order typing. His system was later refined and shown to have principal types by [Rém89, JM88] and again [Wan89]. The resulting system provides a flexible integration of records types and Milner-style type inference [Mil78].

In a parallel development, [CW85] defined a full second-order extension of the system with fixedsize records, based on techniques from [Mit84]. In that system, a program can work polymorphically over all subtypes B of a given record type A, and it can preserve the “unknown” fields (the ones in B but not in A) of record parameters from input to output. However, some natural functions are not expressible. For example, by the nature of fixed-size records there is no way to add a field to a record and preserve all its unknown fields. Less obviously, a function that updates a record field (in the purely applicative sense of making a modified copy of it) is forced to remove all fields from the result which are not explicitly specified in the result type. Imperative update also requires a careful typing analysis.

∗This extended abstract appears in conjunction with John Mitchell’s invited lecture at this meeting. The lecture is a sequel to Luca Cardelli’s invited lecture at the March, 1989 Workshop on Mathematical Foundations of Programming Language Semantics. Both are based on joint work, with this lecture focusing on results obtained after the March conference. A complete paper, currently in preparation, will appear in the proceedings of Programming Language Semantics meeting.

In this paper we describe a second-order type system that allows more flexible manipulation of records. We believe this approach makes the presentation of record types more natural. The general idea is to extend a polymorphic type system with a notion of subtyping at all types. Record types are then introduced as specialized type constructions with some specialized subtyping rules. These new constructions interact well with the rest of the system. For example, row-variables fall out naturally from second-order type variables, and contravariance of function spaces and universal quantifiers mixes well with record subtyping. In moving to second-order typing we lose the principal type property of weaker type systems, in exchange for some additional expressiveness. However, we gain some perspective on the space of possible operations on records and record types. Since it is not yet clear where the bounds of expressiveness may lay, this perspective should prove useful for comparisons and further understanding. Although previous research provides significant hints [Rém89, JM88, OB88, Wan89], we leave it to future research to determine the precise fragment of our current system which admits automatic type inference.

In this short summary, we will only give an informal description of the type system and some of its properties. A formal presentation of the language and several semantic models are given in the full paper.

2 Record values

A record value is essentially a finite map from labels to values, where the values may belong to different types. Syntactically, a record value is a collection of fields, where each field is a labeled value. To capture the notion of a map, the labels in a given record must be distinct. Hence the labels can be used to identify the fields, and the fields should be regarded as unordered. This is the notation we use:

⟨⟩  the empty record.
⟨x = 3, y = true⟩ a record with two fields, labeled x and y,
equivalent to ⟨y = true, x = 3⟩.

There are three basic operations on record values, extension, restriction, and extraction. These have the following basic properties.

Extension ⟨r|x = a⟩ adds a field of label x and value a to a record r, provided a field of label x is not already present. This restriction will be enforced statically by the type system. The additional brackets placed around the operator help to make the examples more readable; we also write ⟨r|x = a|y = b⟩ for ⟨⟨r|x = a⟩|y = b⟩.

Restriction r\x removes the field of label x, if any, from the record r. We write r\xy for (r\x)\y.

Extraction r.x extracts the value corresponding to the label x from the record r, provided a field having that label is present. This restriction will be enforced statically by the type system.

We have chosen these three operations because they seem to be the fundamental constituents of more complex operations. In particular, the extension operation is not required to check whether a new field is already present in a record: its absence is guaranteed statically. The restriction operation has the task of removing unwanted fields and fulfilling that guarantee. This separation of tasks has advantages for efficiency, and for static error detection since fields cannot be overwritten unintentionally by extension alone.

Here are some simple examples:

⟨⟨x = 3⟩|y = true⟩ = ⟨x = 3, y = true⟩ extension
⟨x = 3, y = true⟩\y = ⟨x = 3⟩  restriction (canceling y)
⟨x = 3, y = true⟩\z = ⟨x = 3, y = true⟩ restriction (no effect)
⟨x = 3, y = true⟩.x = 3  extraction
⟨⟨x = 3⟩|x = 4⟩  invalid extension
⟨x = 3⟩.y  invalid extraction

Some additional operators may be defined in terms of the ones above.

Renaming] r[x ← y] {def \atop =} ⟨r\x|y = r.x⟩ changes the name of a record field.

Overriding ⟨r ← x = a⟩ {def \atop =} ⟨r\x|x = a⟩. If x is present in r, replace its value with one of a possibly unrelated type, otherwise extend r with x = a (compare with [Wan89]). Given adequate type restrictions, this can be seen as an updating operator, or a method overriding operator. We write ⟨r ← x = a, y = b⟩ for ⟨⟨r ← x = a⟩ ← y = b⟩.

It is clear that any record may be constructed from the empty record using extension operations. In fact, it is convenient to regard the syntax for a record of many fields as an abbreviation for iterated extensions of the empty record, e.g.,

⟨x = 3, y = true⟩ {def \atop =} ⟨⟨⟨⟩|x = 3⟩|y = true⟩.

This approach to record values allows us to express the fundamental properties of records using combinations of simple operators of fixed arity, as opposed to n-ary operators. Hence we never have to use schemas with ellipses, such as ⟨x_{1} = a_{1}, ..., x_{n} = a_{n}⟩, in our formal treatment.

Since r\x = r whenever r lacks a field of label x, we may write ⟨x = 3, y = true⟩ using any of the following expressions:

⟨⟨⟩|x = 3|y = true⟩ = ⟨⟨⟨⟩\x|x = 3⟩\y|y = true⟩ = ⟨⟨⟩, x = 3, y = true⟩

The latter forms match a similar definition for record types, given in the next section.

3 Record types

In describing operations on record values, we made positive assumptions of the form “a field of label x must occur in record r” and negative assumptions of the form “a field of label x must not occur in record r”. These constraints will be verified statically by the type system. To accomplish this, record types must convey both positive and negative information. Positive information describes the fields that members of a record type must have, while negative information describes the fields the members of that type must not have. Within these constraints, the members of a record type may or may not have additional fields or lack additional fields. It is worth emphasizing that both positive and negative constraints restrict the elements of a type, hence increasing either kind of constraint will lead to smaller sets of values. The smallest amount of information is expressed by the “empty” record type ⟨⟨⟩⟩. The “empty” record type is empty only in that it places no constraints on its members – every record has type ⟨⟨⟩⟩, since all records have at least no fields and lack at least no fields. Here are some other examples.

⟨⟨⟩⟩  the type of all records.

Contains, e.g., ⟨⟩ and ⟨x = 3⟩.

⟨⟨⟩⟩\x  the type of all records which lack a field labeledx.

E.g., ⟨⟩, ⟨y = true⟩, but not ⟨x = 3⟩.

⟨⟨x: Int, y: Bool⟩⟩ the type of all records which have at least fields

labeled x and y, with values of types Int and Bool.

E.g.,⟨x = 3, y = true⟩, ⟨x = 3, y = true, z = str⟩ but not ⟨x = 3, y = 4⟩, ⟨x = 3⟩.

⟨⟨x: Int⟩⟩\y  the type of all records which have at least a field

labeled x of type Int, and no field with label y. E.g.,⟨x = 3, z = str⟩, but not ⟨x = 3, y = true⟩.

These examples illustrate that in general a record type is characterized by a finite collection of “positive” type fields, which are labeled types, and “negative” type fields, which are labels that must not occur in any record of that type. For simplicity, we often say “fields” for “type field.” The positive fields must have distinct labels and should be considered unordered. Negative fields are also unordered and must be distinct in any “normalized” record type expression.

As with record values, we have three basic operations on record types.

Extension ⟨⟨R|x: A⟩⟩ This type denotes the collection obtained from R by adding x fields with values in A in all possible ways (provided that none of the elements of R have x fields). More precisely, this is the collection of those records ⟨r|x = a⟩ such that r is in R and a is in A, provided that a positive type field x is not already present in R (this will be enforced statically). We sometime write ⟨⟨R|x: A|y: B⟩⟩ for ⟨⟨⟨⟨R|x: A⟩⟩|y: B⟩⟩.

Restriction R\x This type denotes the collection obtained from R by removing the field x (if any) from all its elements. More precisely, this is the collection of those records r\x such that r is in R. We write R\xy for (R\x)\y.

Extraction R.x This is the type associated to label x in R, provided R has such a positive field. This provision will be enforced statically.

Again, several derived operators can be defined from these.

Renaming R[x, y] {def \atop =} ⟨⟨R\x|y = R.x⟩⟩ changes the name of a record type field.

Overriding ⟨⟨R ← x: A⟩⟩ {def \atop =} ⟨⟨R\x|x: A⟩⟩ if a type field x is present in R, replaces it with a field x of type A, otherwise extends R. Given adequate type restrictions, this can be used to override a method type in a class signature (i.e. record type) with a more specialized one, to produce a subclass signature.

One crucial formal difference between these operators on types and the similar ones on values is that ⟨⟨⟩⟩\y ≠ ⟨⟨⟩⟩, since records belonging to the “empty” type may have y fields, whereas ⟨⟩\y = ⟨⟩. In forming record types, one must always make a field restriction before a type extension, as illustrated in the examples below.

⟨⟨⟨⟨x: Int⟩⟩\y|y: Bool⟩⟩ = ⟨⟨x: Int, y: Bool⟩⟩ extension
⟨⟨x: Int, y: Bool⟩⟩\y = ⟨⟨x: Int⟩⟩\y  restriction (canceling y)
⟨⟨x: Int, y: Bool⟩⟩\z = ⟨⟨x: Int, y: Bool⟩⟩\z restriction (no effect)
⟨⟨x: Int, y: Bool⟩⟩.x = Int  extraction
⟨⟨⟨⟨⟩⟩|x: Bool⟩⟩  invalid extension
⟨⟨x: Int⟩⟩.y  invalid extraction

It helps to read the examples in terms of the collections they represent. For example, the first example for restriction says that if we take the collection of records that have x and y (and possibly more) fields, and remove the y field from all the elements in the collection, then we obtain the collection of records that have x (and possibly more) but no y. In particular, we do not obtain the collection of records that have x and possibly more fields, because those would include y.

The way positive and negative information is formally manipulated is actually easier to understand if we regard record types as abbreviations, as we did for record values:

⟨⟨x: Int, y: Bool⟩⟩ {def \atop =} ⟨⟨⟨⟨⟨⟨⟩⟩\x|x: Int⟩⟩\y|y: Bool⟩⟩

Then, when considering ⟨⟨y: Bool⟩⟩\y, we actually have ⟨⟨⟨⟨⟩⟩\y|y: Bool⟩⟩\y. If we allow the outside positive and negative y labels to cancel, we are still left with ⟨⟨⟩⟩\y. The inner y restriction reminds us that y fields have been eliminated from records of this type.

4 Summary

The record and record-type operations discussed in the preceding sections are incorporated in a typed calculus with subtyping. The subtyping rules for record types are essentially that every record type is a subtype of ⟨⟨⟩⟩, and the subtyping relation respects the type operations of extension, restriction and extraction. Writing A <: B for A is a subtype of B, we have the following examples.

⟨⟨x: Int, y: Bool⟩⟩ <: ⟨⟨⟩⟩
⟨⟨R|x: A⟩⟩ <: ⟨⟨S|x: A⟩⟩ if R <: S <: ⟨⟨⟩⟩\x
R\x <: S\x  if R <: S <: ⟨⟨⟩⟩
R.x <: S.x  if R <: S <: ⟨⟨x: A⟩⟩

In general, a record type R will be a subtype of another record type S if every positive constraint (labeled field) associated with R is also a positive constraint imposed by S, and similarly for negative constraints (fields required to be absent). There are some subtleties. For example, ⟨⟨R\x|x: Int⟩⟩ is not necessarily a subtype of R, and never a subtype of R\x, even though this might seem consistent with the point of view expressed in [Car88], for example.

There are several variants of the typed calculus, each described in the full paper. In the basic calculus, any collection of records might reasonably be regarded as a type, as illustrated by a simple semantic model. One natural extension of the calculus is obtained by imposing the condition that whenever R is a type of records with x field (i.e., whenever R <: ⟨⟨x: A⟩⟩ for some type A), we must have R = ⟨⟨R\x|x: R.x⟩⟩. In category-theoretic terms, this equation says that R must be the cartesian product of R\x and R.x. This equation may fail if we allow arbitrary collections of records as types. For example,

R = {⟨x = 1, y = true⟩, ⟨x = 0, y = false⟩

is not the cartesian product of R\x = {⟨y = true⟩, ⟨y = false⟩} and R.x = {0, 1}. By omitting certain sets of records, we may construct a semantic model in which every record type is the appropriate cartesian product.

A second extension of the basic calculus is obtained by adding the equational axiom

r = s : ⟨⟨⟩⟩

which equates all records of type ⟨⟨⟩⟩. This extensionality axiom makes good sense, since no operation of the calculus will allow us to distinguish between records r and s of type ⟨⟨⟩⟩. One importnat aspect of the equational theory is that equations must be regarded as triples, consisting of two expressions and a type, rather than pairs. Put another way, we may assert that records r and s are equal records of type R, but not equal when considered with respect to another record type S. In particular, the records r : : = ⟨x = 3⟩ and s : : = ⟨x = 4⟩ belong to types ⟨⟨x: Int⟩⟩ and ⟨⟨⟩⟩. Since we may extract the x field of any record belonging to type ⟨⟨x: Int⟩⟩, records r and s are distinguishable as elements of this type, and so we have

r ≠ s: ⟨⟨x: Int⟩⟩.

However, since we cannot extract the x field of a record belonging to type ⟨⟨⟩⟩, we also have the equation r = s: ⟨⟨⟩⟩. Interpreting types as partial equivalence relations (sets together with equivalence relations), we may construct a semantic model in which every record type is a cartesian product, and extensional equality is satisfied. However, we have not been able to construct a semantic model of extensional equality without restricting record types to cartesian products.

References

[Car88] L. Cardelli. A semantics of multiple inheritance. Information and Computation, 76:138– 164, 1988. Special issue devoted to Symp. on Semantics of Data Types, Sophia-Antipolis (France), 1984.

[CW85] L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4):471–522, 1985.

[JM88] L. Jategaonkar and J.C. Mitchell. ML with extended pattern matching and subtypes. In Proc. ACM Symp. Lisp and Functional Programming Languages, pages 198–212, July 1988.

[Mil78] R. Milner. A theory of type polymorphism in programming. JCSS, 17:348–375, 1978.

[Mit84] J.C. Mitchell. Coercion and type inference (summary). In Proc. 11-th ACM Symp. on Principles of Programming Languages, pages 175–185, January 1984.

[OB88] A. Ohori and P. Buneman. Type inference in a database language. In Proc. ACM Symp. Lisp and Functional Programming Languages, pages 174–183, July 1988.

[Rém89] D. Rémy. Typechecking records and variants in a natural extension of ML. In 16-th ACM Symposium on Principles of Programming Languages, pages 60–76, 1989.

[Wan87] M. Wand. Complete type inference for simple objects. In Proc. 2-nd IEEE Symp. on Logic in Computer Science, pages 37–44, 1987. Corrigendum in Proc. 3-rd IEEE Symp. on Logic in Computer Science, page 132, 1988.

[Wan89] M. Wand. Type inference for record concatenation and simple objects. In Proc. 4-nd IEEE Symp. on Logic in Computer Science, pages 92–97, 1989.