Type Inference with Extended Pattern Matching and Subtypes

Lalita A. Jategaonkar Laboratory for Computer Science Massachusetts Institute of Technology Cambridge, MA, USA

lalita@theory.lcs.mit.edu

John C. Mitchell Department of Computer Science Stanford University Stanford, CA, USA

mitchell@cs.stanford.edu

Abstract. We study a type system, in the spirit of ML and related languages, with two novel features: a general form of record pattern matching and a provision for user-declared subtypes. Extended pattern matching allows a function on records to be applied to any record that contains a minimum set of fields and permits the additional fields of the record to be manipulated within the body of the function. Together, these two enhancements may be used to support a restricted object-oriented programming style. We define the type system using inference rules, and develop a type inference algorithm. We prove that the algorithm is sound with respect to the typing rules and that it infers a most general typing for every typable expression.

1 Introduction

This paper describes a language design and type inference algorithm that are part of a continuing effort toward flexible type systems for object-oriented programming languages. We are interested in type systems that would be appropriate for a language such as Smalltalk [GR83], although we do not intend to work with Smalltalk specifically. In particular, we would like a type system that would not substantially interfere with the programming techniques that are commonly used in untyped object-oriented programming. In object-oriented programming, the basic computational entities are objects, which are generally grouped together in classes of similar objects. There is a hierarchy of classes, where more specialized objects of a class form subclasses. Operations defined on a class can be inherited, or automatically used, by objects of any subclass. Furthermore, the representation of objects and the associated class operations can be hidden. These features of inheritance and information hiding are often regarded as central to object-oriented programming.

In so-called “strongly typed” languages, every expression has a type that can be checked at compile-time, and there are inflexible rules about combining operations and operands of different types. Compile-time type checking for these languages guarantees that a certain class of errors, known as type errors, will not arise at run-time. Some drawbacks of early strongly typed languages such as Pascal are that they require the programmer to declare the types of all variables, and require a function used at several types to be declared separately for each type. In more recent languages such as ML [Mil78, Mil85], the types of all variables and expressions can be inferred by the compiler from the surrounding context, and thus can be omitted by the programmer. Moreover, the inferred types are “most general” types, from which all valid types can be automatically derived. Languages with type inference thus provide greater flexibility and expressive power than traditional strongly typed languages, while maintaining the same guarantees on run-time behavior.

In recent years, there has been substantial research on type inference for objectoriented programming. The viewpoint developed by [Car84, Car88] and adopted by others [Wan87, Sta88, Rém89, Rém90c] is to consider an object as a record consisting of a set of labeled, typed fields and incorporating some form of subtyping to model subclass relations. Typically, a record type A is considered to be a subtype of record type B if A has at least all of the fields of B, and perhaps more. Type inference in this context involves two problems: there may be no single “most general” typings [Wan88, Wan89], or worse yet, in some variations, typing may be undecidable even when the inference problem is sufficiently constrained to force each expression to have a unique minimal type [Pie92].

Although viewing objects as records captures some aspects of “object-oriented” behavior, it does not permit information hiding. For this reason, it is also useful to think of objects as elements of some form of abstract data types. For example, we can think of objects as “ML-style” abstract data types, which have an associated name, a hidden representation, and associated operations whose implementation is hidden. Importantly, the types of these operations do not reveal the underlying representation of the abstract type; they only refer to the abstract type by name. In order to support both inheritance and information hiding in this framework, we want objects of any subtype to be able to use these operations automatically, without revealing the representation of the subtype. From this point of view, it seems natural to declare subtyping between abstract types. Some relevant work is [Mit84, Mit91], which develop a type system and algorithm for inferring most general types for pure lambda terms in the context of subtype declarations. In [Mit84, Mit91], the system of subtyping relations between simple types is referred to as “atomic subtyping,” and can be thought of as a special case of “bounded quantification” [CW85]. In Section 9.2, we outline the design of an extension of ML-style abstract types with subtyping. While we do not consider this system in the technical portions of the paper, this provides the basic motivation and perspective for the technical development of our type system and algorithm.

The main technical contribution of this paper is a type system and typing algorithm which combines the subtyping ideas of [Mit84, Mit91] with the record typing system of [Wan87]. The main innovations of [Wan87] are the introduction of “row variables”, which allow more flexibility in the typing of records, and an extension of unification [Rob65] that supports row variables. Single most general typings do not exist for some typable terms in the system of [Wan87]; in fact, the typing algorithm generally infers a finite, and possibly exponential-sized set of most general typings. By imposing a restriction on records, we avoid the technical difficulties of [Wan87], and our algorithm infers a single most general typing for every typable expression. We note that many of the shortcomings of [Wan87] have been repaired independently in [Rém89], which has some advantages over the system presented here, but does not involve subtyping^{1} . An apparently simple but somewhat subtle extension of [Mit84, Mit91] that we develop here is the inclusion of type constants and polymorphic expression constants. We discuss polymorphic declarations briefly. Although the main ideas behind adding polymorphic declarations to any type inference algorithm of a certain form are explained in [KMM91, Mit90b], there are some complications that arise with subtyping.

1 An earlier conference version of this paper, [JM88], appeared approximately contemporaneously with [Rém89].

In Section 2, we give an informal introduction to our language ML^{+} , which is an extension of a kernel of the programming language ML. The name ML^{+} is intended to suggest that we are “half way” to an object-oriented ML^{++} . Precise syntactic definitions appear in Section 3, and typing rules are given in Section 4. Section 5 presents our extension of unification similar to that of [Wan87], while Section 6 presents a related algorithm for subtype assertions. The type inference algorithm for ML^{+} is presented in Section 7, where we show that our algorithm only infers types derivable by our type system, and generates single most general typings for all typable expressions. In Section 8, we compare this system with related work. Finally, Section 9 describes polymorphic let declarations and an extension of ML-style abstract data type declarations with user-declared subtyping.

An overview of a preliminary version of this material appeared as [JM88].

2 Informal Introduction to ML^{+}

The ML^{+} language is based on a functional subset of ML that includes built-in constants, records, and function abstraction using pattern matching constructs to decompose records into their constituents. We do not include variants (tagged unions), although subtyping of variants involves issues closely related to the subtyping of records [Car84, Car88, Wan87, Sta88, Rém89]. We would expect that incorporating variants into our system would not cause any serious difficulties, but we do anticipate that there could be some technical overhead involved.

We extend this kernel of ML two ways. We develop a form of “extended pattern matching” that lets us apply a function on records to any record containing some minimum set of required fields and permits the additional fields of the record to be manipulated within the body of the function. More specifically, we introduce expression variables denoting elements of Wand’s “rows.” These may be bound by pattern matching to sequences of labeled values (parts of records). Using extended pattern matching, we may define functions that operate “anonymously” on parts of records without knowing the names of the fields involved. In keeping with the spirit of ML, this form of extended pattern matching eliminates the need for conditional statements to decompose arguments passed to functions.

Our second extension to ML involves subtyping relations between atomic types. For built-in atomic types such as int and real, subtyping relationships such as int ⊆ real must be specified as part of the language design. This form of subtyping, combined with record subtyping, provides a framework for subtyping among abstract types.

Some examples will illustrate the flavor of ML^{+} . Following Standard ML, function expressions (lambda abstractions) are written fn P ⇒ M , where P is a pattern, often resembling a record expression, and M is any expression. We use the notation {a = 3, b = true; v} for the record containing at least the fields a and b, with the values 3 and true, and the notation {a = 3, b = true; empty} for the record containing exactly the fields a and b with those values. A function f incrementing the a field of a record may be written as

f : : = fn {a = x; v} ⇒ {a = x + 1; v}

Essentially, the pattern {a = x; v} matches any record with an a field, binding x to the value of a, and binding v to any finite mapping from labels to values extending a = x. If f is applied to {a = 3, b = true; empty}, for example, then x is bound to 3 and v is bound to (b = true; empty) . One type of f in ML^{+} is

{a: int; null} → {a: int; null}

where null indicates that the record contains exactly the fields specified, since f clearly can map records with exactly an a: int field to records with exactly an a: int field. A more general type of f is written

{a: int; X_{{a}}} → {a: int; X_{{a}}}

where X_{{a}} is a “row” variable denoting a sequence of labeled types that does not contain an a field. (This restriction on the a field ensures that a cannot be multiply defined in the record applied to or returned by this function.) The row variable X_{{a}} in this type expression is implicitly universally quantified, so this typing “says” that f has type {a: int; X_{{a}}} →{a: int; X_{{a}}} for all rows X_{{a}} that do not contain an a field. In particular, f also has type

{a: int, b: bool, c: string; null} →{a: int, b: bool, c: string; null}

since (b:bool, c:string; null) is a possible value for X_{{a}}. If we apply f to the record {a = 3, b = true, c = “extra”; empty}, then the “extension” variable v is bound to (b = true, c = “extra”; empty) , and the result of the function application is

f({a = 3, b = true, c = “extra”; empty}) = {a = 4, b = true, c = “extra”; empty}

Using the type above, our typing algorithm gives the result of function application the correct type.

The use of row variables to describe the inherent polymorphism of record operations is due to Wand [Wan87]. However, the row variables in our system differ from those used in [Wan87] in that our row variables are subscripted with sets of labels.

In this paper, we do not investigate the semantics of ML^{+} , either from an operational or denotational point of view; readers interested in these issues are directed towards [Kam88, BL90, Red88, Coo89, BTCGS90, BTCGS91, CHC90, Mit90a]. However, we do have an operational semantics in mind. This “intended” semantics is essentially the usual operational semantics of core ML[MTH90], extended in a couple of ways. In order to treat extended pattern matching appropriately, we expect to modify the β -reduction rule and the notion of “type error” to take pattern matching of flexible records into account. For example, as discussed earlier in this section, if we apply the function fn {a = x; v} ⇒ {a = x + 1; v} to the record {a = 3, b = true; empty}, we get the record {a = 4, b = true; empty}. On the other hand, if we apply this same function to the record {b = true; empty}, we have a “type error.”

We also expect to modify the interpreter to take advantage of subtyping. In particular, we expect to parameterize the interpreter by some set of “valid” subtype assertions between base types, together with corresponding “coercion” functions between values of those types. Furthermore, we expect to have the interpreter automatically apply appropriate coercion functions when “necessary”. For example, if we assume that int ⊆ real , and we apply an equality function to the values 3 and 3.5 , we would expect that the value 3 would be coerced to 3.0 , and that the result of the function application would be the value false. The use of subtype inference to insert such coercions is discussed in [Mit91].

We fully expect our typing system to be sound with respect to an operational semantics defined in such a manner: namely, we expect that no typable expression of ML^{+} will generate a “type error” during evaluation. For a discussion on proving such properties of type systems, the interested reader is directed towards [WF92].

3 Syntax of Types and Terms

3.1 Types

We begin with an infinite set of type variables and some fixed set of type constants, which we call base types. For concreteness, we will use { int, bool, real, string } as our set of base types. The typing rules and algorithm are easily adapted to any set of base types.

There are two forms of structured types: function types and record types. Function types are written using → as usual, so that σ → τ is the type of functions from σ to τ . Record types are written in a slightly unusual way. Intuitively, a record type is determined by a finite function from labels to types. In our system, part of this finite function is given explicitly as part of the record type expression, and part may be given by a function variable. These function variables were introduced in [Wan87] and called row variables. We follow Wand’s terminology and assume an infinite set of row variables along with the single row constant null which denotes the empty function. However, unlike [Wan87], each of our row variables has a subscript which is a finite set L of labels. A row variable with subscript L may denote any finite function from labels to types whose domain is disjoint from L. We sometimes refer to the subscript of a row variable Z as its label set, and write it as labels(Z) . We assume an infinite set of labels, and we define the label set of the row constant null , written labels(null) , to be this entire set of possible labels. Furthermore, for any finite set L of labels, we assume that there is an infinite set of row variables with label set L.

A record type is a pair {h; Z}, where h is a finite (possibly empty) function from labels to types and Z is either a row variable or the row constant null. We call a record type in which Z is a row variable a flexible record type, and a record type in which Z is null fixed. Since we want to prohibit multiply-defined labels within record types, we stipulate that in any record type {h; X_{L}}, L must contain all labels in the domain of h. Any expression that violates this constraint is considered to be ill-formed, and is not a type. For notational convenience, we sometimes simply write {Z} to denote the record {∅; Z}, and sometimes write {l_{1} :τ_{1}, …, l_{n}:τ_{n}; Z} to denote {h; Z}, where h is a (non-empty) function with domain {l_{1}, …, l_{n}} that maps each l_{i} to τ_{i}. For example, we may write {a: σ, b: τ; X_{{a,b,c}}} to denote the record {h; X_{{a,b,c}}}, where h maps a to σ and b to τ . The expressions {a: σ, b: τ; X_{{a,b,c}}} and {b: τ, a: σ; X_{{a,b,c}}} are considered identical since (a: σ, b: τ) and (b: τ, a: σ) are the same finite function. Since the set of labeled fields within any record type written is this manner must denote a function from labels to types, multiply-defined labels are prohibited. For example, {a: σ, a: τ; Z} is not a well-formed record type, nor is {a: σ, a: σ; Z}.

The syntax of types is summarized in Table 1.

Table 1: Summary of Types

b  base types
t  type variables
σ → τ  function types
{h; null} fixed record types
{h; X_{L}} flexible record types

where h is a finite function from labels to types and L ⊇ dom(h)

3.2 Syntax of Expressions

ML^{+} is derived from a subset of ML with pattern matching, function abstraction, records, constants of base type, and built-in, possibly higher-order, constants. For the constants of base type, we assume the set of integers, some suitable subset of the real numbers, the set { true, false } of booleans, and an infinite set of strings. Although there is no explicit construct for declaring recursive functions, it is possible to have a fixed-point operator, fix, as a built-in higher-order constant. As mentioned previously, the two novel features of ML^{+} are an extended form of pattern matching on records, and structural subtyping arising from subtyping assertions about base types.

Extended pattern matching is achieved using an infinite set of extension variables, which play a role in expressions similar to that of row variables in the type system; however, extension variables do not have associated label sets. Formally, extension variables denote finite functions from labels to values, while the extension constant empty denotes the empty function. A record expression is a pair {f; E}, where f is a finite function from labels to expressions and E is an extension variable or empty. We call a record expression in which E is an extension variable a flexible record, and one in which E is empty fixed. For notational convenience, we sometimes simply write {E} to denote the record {∅; E}. Furthermore, if f is a (non-empty) function with domain {l_{1}, …, l_{n}} that maps each l_{i} to M_{i}, we often write {f; E} explicitly as {l_{1} = M_{1}, …, l_{n} = M_{n}; E}, where the l_{i} can occur in any order. Since the set of labeled fields within any record expression written in this manner denotes a function from labels to expression, it is easy to see that multiply-defined labels are prohibited. For example, {a = 3, a = 4; u} does not denote a record expression, nor does {a = 3, a = 3; u}.

Although extension variables do not have label sets, a property of our typing system is that only appropriately restricted types are derivable for extension variables that appear in record expressions. For example, if both {a = 3; u} and {b = true; u} appear inside a typable ML^{+} expression, then the typing rules ensure that the type of u can never contain an a or a b field.

Patterns are the proper subset of expressions built recursively from variables, fixed record expressions, and flexible record expressions, with the added restriction that all variables and extension variables within the expression must be distinct. In other words, patterns are linear expressions that are abstraction-free, application-free, and constant-free.

As in ML, pattern matching in ML^{+} provides a limited form of equality testing over the structure of types. Specifically, an expression M matches a record pattern of the form {f; u} iff M is a record whose domain contains the domain of f , and corresponding fields of M and f (recursively) pattern-match; the definition is similar Table 2: Summary of Expressions and Patterns

Expressions

c  constants of base type
q  built-in, possibly higher-order, constants
x  variables
fn P ⇒ M abstraction
M N  application
{f; empty} fixed records
{f; u}  flexible records

where f is a finite function from labels to expressions

for record patterns of the form {f; empty} except that additionally, the domain of M and f must be identical. By allowing patterns to contain constants, however, ML also provides an equality test for constants of base type. This leads to a small complication in ML because expressions like (fn 2 => true)5 are typable, but generate an error during evaluation. In order to ensure the soundness of the ML type system with respect to the operational semantics, ML does not consider these “match errors” to be “type errors.” Our language ML^{+} can easily be extended to allow pattern matching over constants of base type; however, we do not do so here for the sake of simplicity.

Expressions and patterns are summarized in Table 2. Since there are quite a few syntactic categories to ML^{+}, our meta-notation is summarized in Table 3.

4 The Typing System

The type system for ML^{+} is given in the form of type inference rules. The typing rules are divided into two groups: rules for deriving subtype assertions, and rules for giving types to patterns and expressions. We begin with the proof system for deriving subtype assertions.

4.1 Proof System for Subtype Assertions

Subtype assertions have the form σ ⊆ τ , where σ and τ are types. We follow [Mit84, Mit91] and adopt the following three rules for deriving subtype assertions.

ref σ ⊆ σ

trans  \frac{σ ⊆ τ, τ ⊆ γ}{σ ⊆ γ}

arrow  \frac{σ ⊆ σ′, τ′ ⊆ τ}{σ′ → τ′ ⊆ σ → τ}

We note that the function type constructor → is antimonotonic (contravariant) in the first argument and monotonic (covariant) in the second.

We have a similar rule for the “subtype” relation on records.

Table 3: Summary of Notational Conventions

M, N  expressions
c  constants of base type
q  built-in, possibly higher-order, constants
x, y, z  variables
u, v  extension variables
w  variables and extension variables
E  extension variables and empty
f  finite functions from labels to expressions
{f; E}  record expressions
{l_{1} = M_{1}, …, l_{k} = M_{k}; E} alternate syntax for record expressions
(note: l_{i} ≠ l_{j} for all i ≠ j )
P  patterns

σ, τ  type expressions
b  base types
r, s, t  type variables
L, L′  finite sets of labels
X_{L} , Y_{L′} , W_{L′}  row variables
Z  row variables and null
h  finite functions from labels to types
{h; Z}  record types
{l_{1} : τ_{1}, …, l_{n} : τ_{n}; Z}  alternate syntax for record types

where l_{i} ≠ l_{j} for all i ≠ j and labels(Z) ⊇ {l_{1}, …, l_{n}}

Note: labels(null)=_{def} the entire set of possible labels

record  \frac{\{∅; Z\} ⊆ \{∅; Z′\} and ∀l ∈ dom(h), h(l) ⊆ h′(l)}{\{h; Z\} ⊆ \{h′; Z′\}}

where dom(h) = dom(h′) ≠ ∅, dom(h) ⊆ labels(Z) and dom(h′) ⊆ labels(Z′)

We say that a subtype assertion σ ⊆ τ is provable from a set C of subtype assertions, written C ⊢ σ ⊆ τ , if σ ⊆ τ can be derived from assertions in C using only the typing rules above. We will write C ⊢ C′ if C ⊢ σ ⊆ τ for every σ ⊆ τ ∈ C′.

In our typing system, we restrict C to consist only of atomic subtype assertions, where we say that a subtype assertion σ ⊆ τ is atomic iff

• Each of σ and τ is a base type or a type variable.

• σ and τ are both {∅; null}.

• σ is of the form {∅; X_{L}} and τ is of the form {∅; Y_{L′}}, where L = L′.

We say that C is atomic or that C is an atomic set if it consists only of atomic subtype assertions.

4.2 Syntax of Typing Statements

Our typing statements for expressions have the form

C, A ⊃ M : σ

where

• C is a set of atomic subtype assertions.

• A is a finite set of associations x:σ between variables and types, and associations u: {h; Z} between extension variables and record types.

• M is an expression and σ is a type.

The typing C, A ⊃ M : σ may be read as, “Given the subtype assertions in C and the assignment of types to variables and extension variables described by A, the expression M has the type σ.”

We consider all type and row variables in a typing statement to be implicitly universally quantified. For example, the typing

{s ⊆ t}, ∅ ⊃ (fn x ⇒ x) : s → t

should be read as, “For all types s and t such that s ⊆ t, the identity function has the type s → t.”

4.3 Proof System for Typing Statements

We begin with the typing axioms for constants of base type.

int C, A ⊃ c: int whenever c is an integer constant (numeral)

The axioms for reals, booleans, and strings are similar.

The typing rules for variables and application are standard:

var C, A ⊃ x: σ whenever x: σ ∈ A

app  \frac{C, A ⊃ M : σ → τ and C, A ⊃ N : σ}{C, A ⊃ MN : τ}

Since lambda abstraction may bind arbitrary patterns in addition to variables, the typing rule for lambda abstraction is somewhat more complicated than usual. The typing rule for function expressions must take the typing of patterns into account, and there is a subtle but important reversal of subtype assertions in the abstraction rule which seems best illustrated by a simplified example. The pattern {a = x; empty} has the typing

{s ⊆ t}, {x: s} ⊃ {a = x; empty} : {a: t; null},

which means that if we give x a value of type s, and s is a subtype t, then the pattern has type {a: t; null}. However, when we lambda abstract over the pattern, we actually bind a value to {a = x; empty} and access its components using the variable x. So, in effect, we use the typing statement about the pattern “backwards.”

The simplest technical adjustment seems to be to reverse the set of subtype assertions before combining them with the typing statement for the function body. If the function body is simply x, for example, then this gives us the typing

{t ⊆ s}, ∅ ⊃ (fn {a = x; empty} ⇒ x) : {a: t; null} → s

while writing s ⊆ t instead would give us an incorrect typing. (An alternative is to reformulate the typing rules for patterns in a way that more accurately reflects their use. However, the current formulation has algorithmic advantages due to the similarities between patterns and expressions.)

In order to state the typing rule for lambda abstraction, we need some preliminary definitions. Since the notion of free variables is important in the typing rule for abstraction, we define vars(M) inductively as:

• vars(x) = x

• vars({f; empty}) = ⋃_{l∈dom(f)} vars(f(l))

• vars({f; u}) = {u} ∪ ⋃_{l∈dom(f)} vars(f(l))

• vars(MN) = vars(M) ∪ vars(N)

• vars(fn P ⇒ M) = vars(M) − vars(P) , where “ − ” is set difference

• vars(q) = vars(c) = ∅

We define vars(A) = {w | w : σ ∈ A}, where w ranges over variables and extension variables, and let A[A′] be the result of modifying A so that every variable and extension variable mentioned in A′ has the type specified by A′ rather than A. More precisely, A[A′] = A′ ∪ {w: σ | w: σ ∈ A and w ∉ vars(A′)}.

Finally, we use the notation C^{op} for the opposite set of subtype relations,

C^{op} = {σ ⊆ τ | τ ⊆ σ ∈ C}

The typing rule for abstraction is then as follows.

abs  \frac{C^{op}, A′ ⊃ P : σ and C, A[A′] ⊃ M : τ}{C, A ⊃ fn P ⇒ M : σ → τ} vars(A′) = vars(P)

The condition vars(A′) = vars(P) ensures that A′ only contains variables that occur in P . This is important, since we want A[A′] to modify A only on variables that become bound by fn. The reader may verify that

\frac{\{s ⊆ t\}, \{x: s\} ⊃ x : t and \{t ⊆ s\}, \{x: s, y : r\} ⊃ \{a = x, b = y; empty\} : \{a: s, b: r; null\}}{\{t ⊆ s\}, \{y : r\} ⊃ (fn x ⇒ \{a = x, b = y; empty\}) : t →\{a: s, b: r; null\}}

is an instance of this rule.

We now introduce the axioms for records whose first component is the empty function.

rec1 C, A ⊃ {∅; empty}: {∅; null} rec2 C, A ⊃ {∅; u}: {h; Z} whenever u: {h; Z} ∈ A

The third typing rule is for records whose first component is a non-empty function. Since extension variables may be assigned arbitrary record types, we have a minor complication since we do not want duplicate labels. To express the rule succinctly, we write h_{1} + h_{2} for the set-theoretic union, h_{1} ∪ h_{2} , of finite functions h_{1} and h_{2} , regarded as sets of ordered pairs in the usual way. If h_{1} ∪ h_{2} is not a function, then we consider h_{1} + h_{2} undefined.

The third rule for records is then as follows.

rec3  \frac{C, A ⊃ \{∅; E\}: \{h_{2}; Z\} and ∀l ∈ dom(f), C, A ⊃ f(l) : h_{1}(l)}{C, A ⊃ \{f; E\}: \{h_{1} + h_{2}; Z\}}

where dom(f) = dom(h_{1}) ≠ ∅, dom(h_{1}) ∩ dom(h_{2}) = ∅ and dom(h_{1}) ⊆ labels(Z)

The side conditions ensure that h_{1} + h_{2} is well-defined and that {h_{1} + h_{2}; Z} is well-formed (assuming that {h_{2}; Z} and all types in the range of h_{1} are well-formed).

Our typing system also allows any set of built-in, possibly higher-order, constants as long as a type and a set of atomic subtype assertions is specified for each constant. For example, suppose we want a built-in constant plus that adds two numerical values, each of some subtype of real. A plausible typing for plus is

{t ⊆ real}, ∅ ⊃ plus : t →(t → t).

It may seem at first glance that this typing does not take full advantage of the power of subtyping. However, as we will see in Section 4.5, it follows from the above typing that

⊢ C, A ⊃ plus : t_{1} →(t_{2} → t),
where C = {t_{1} ⊆ t, t_{2} ⊆ t, t ⊆ real},

and A is any type environment. Thus, if we apply plus to any two numerical values, each of some subtype of real, and instantiate t with any upper bound σ of the two subtypes that is also a lower bound of real, the resulting value will have the type σ. In particular, if int ⊆ real , we can add two integers and get an integer, while we can add an integer and a real and obtain a real. As we shall see in Section 4.6, whenever A is the empty type environment, the typing displayed above is a “most general” typing of plus. (We realize that there is a semantic issue surrounding this typing of plus, pointed out to Bruce and Longo by the second author and discussed in [BL90].)

An equality function eq_{b} over each base type b can also be added as a built-in function with associated typing

∅, ∅ ⊃ eq_{b} : b →(b → bool).

Again, we can derive from this the more general typing

{t_{1} ⊆ b, t_{2} ⊆ b, bool ⊆ t_{3}}, ∅ ⊃ eq_{b} : t_{1} →(t_{2} → t_{3}).

Thus, we can apply eq_{b} to any two values, each of some subtype of b, and obtain a value that is of some supertype of bool. Semantically, we would expect eq_{b} to compare its two arguments as if they are elements of b.

The natural axiom for built-in constants might seem to be

C_{q}, ∅ ⊃ q : τ_{q}

where C_{q} and τ_{q} are, respectively, the specified set of atomic subtype assertions and the specified type for the built-in constant q. However, as will become apparent in the next section, the set of typings that are provable in the resulting system would not be closed under taking “substitution instances.” For this reason, we need to generalize our axiom for built-in constants to be the rule:

const  \frac{C, A ⊃ q : τ is an instance of C_{q}, ∅ ⊃ τ_{q}}{C, A ⊃ q : τ}

The definition of instance will be given in the next section. This sort of inference rule is fairly standard: for example, a similar rule appears in [DM82].

Finally, in order to make use of subtyping, we have the rule

coerce  \frac{C, A ⊃ M : σ and C ⊢ σ ⊆ τ}{C, A ⊃ M : τ}

By this rule, an expression may be considered to be of any “supertype” of its derived type.

4.4 Substitutions and Instances

A substitution S is a function from type variables to types and from row variables to record types that satisfies the following property: if S(X_{L}) = {h; Z} then dom(h)∩L = ∅ and L ⊆ labels(Z) . This property ensures that applying substitutions to types in the natural manner will result in “well-formed” type expressions. We define the result of applying a substitution to a type inductively as:

• Sb = b

• S(σ → τ) = Sσ → Sτ

• St = S(t)

• S{∅; X_{L}} = S(X_{L})

• S{∅; null} = {∅; null}

• S{h; Z} = {(h_{S} + h′); Z′} where {h′; Z′} = S{∅; Z} and h_{S} is (S ∘ h) restricted to dom(h)

It is easy to show that the application of substitutions to types always yields wellformed type expressions, and that the functional composition of substitutions yields well-defined substitutions.

We extend substitutions to type environments and to sets of possibly non-atomic subtype assertions. A substitution S applied to a type environment A is simply the point-wise application of S to the components of A, namely, the assignment SA = {w: Sσ | w: σ ∈ A}, where w ranges over variables and extension variables. Similarly, the application of substitution S to a possibly non-atomic set C is the set SC = {Sτ_{1} ⊆ Sτ_{2} | τ_{1} ⊆ τ_{2} ∈ C}. In general, even if C is atomic, SC may be a non-atomic set, and thus, the (point-wise) application of a substitution to a typing statement may not yield a well-formed typing statement. Thus, in our definition of “substitution instance,” we instead use a “minimal” atomic set S • C that implies SC, and such that any atomic set C′ that implies SC also implies S • C. In order to define this • operation, we begin by showing that an atomic set can imply only matching subtype assertions σ ⊆ τ , where σ and τ have the same “shape.” More precisely, we recursively define the relation match on types as:

• t_{1} matches t_{2}

• b_{1} matches b_{2}

• t matches b, and b matches t

• σ → τ matches σ′ → τ′ iff σ matches σ′ and τ matches τ′

• {∅; null} matches {∅; null}

• {∅; X_{L}} matches {∅; Y_{L′}} iff L = L′

• {h; Z} matches {h′; Z′} iff {∅; Z} matches {∅; Z′}, dom(h) = dom(h′), and ∀l ∈ dom(h), h(l) matches h′(l)

We note that every atomic subtype assertion is matching. Furthermore, we have that:

Lemma 4.1 For any atomic set C and any types σ and τ , if C ⊢ σ ⊆ τ , then σ matches τ .

The lemma is easily proved by induction on the length of the derivation of σ ⊆ τ from C; we omit the details.

We now wish to show that for any matching subtype assertion σ ⊆ τ , we can compute a “minimal” atomic set ATOMIC(σ ⊆ τ) that implies σ ⊆ τ . However, in order to justify “decomposing” σ ⊆ τ into atomic subtype assertions, we will need to use the following lemmas about the form of derivable subtype assertions.

Lemma 4.2 For any atomic set C and any types σ_{1} → σ_{2} and τ_{1} → τ_{2} , C ⊢ σ_{1} → σ_{2} ⊆ τ_{1} → τ_{2} iff C ⊢ τ_{1} ⊆ σ_{1} and C ⊢ σ_{2} ⊆ τ_{2} .

We have a similar lemma for records.

Lemma 4.3 For any atomic set C and any record types {h; Z} and {h′; Z′}, C ⊢ {h; Z} ⊆ {h′; Z′} iff C ⊢ {ϕ; Z} ⊆ {ϕ; Z′}, C ⊢ h(l) ⊆ h′(l) for all l ∈ dom(h) , and dom(h) = dom(h′) , dom(h) ⊆ labels(Z) , and dom(h′) ⊆ labels(Z′) .

These lemmas are proved by a simple induction on types, which is left to the reader. For any matching types σ and τ , we now define the operation ATOMIC(σ ⊆ τ)

inductively as:

• If σ ⊆ τ is an atomic subtype assertion, then ATOMIC(σ ⊆ τ) = {σ ⊆ τ}.

• If σ ⊆ τ is of the form σ_{1} → σ_{2} ⊆ τ_{1} → τ_{2} , then

ATOMIC(σ ⊆ τ) = ATOMIC(τ_{1} ⊆ σ_{1}) ∪ ATOMIC(σ_{2} ⊆ τ_{2}).

• If σ ⊆ τ is of the form {h; Z} ⊆ {h′; Z′}, then

ATOMIC(σ ⊆ τ) = {{∅; Z} ⊆ {∅; Z′}} ∪ ⋃_{l∈dom(h)} ATOMIC(h(l) ⊆ h′(l)).

The set ATOMIC(σ ⊆ τ) satisfies the desired properties:

Lemma 4.4 Let σ and τ be matching types. Then ATOMIC(σ ⊆ τ) is atomic, ATOMIC(σ ⊆ τ) ⊢ σ ⊆ τ , and for all atomic sets C′, if C′ ⊢ σ ⊆ τ then C′ ⊢ ATOMIC(σ ⊆ τ) .

The proof follows easily by the above lemmas and a simple induction on the structure of σ ⊆ τ . The details are left to the reader.

Before defining the instance relation on typing statements, we need some preliminary definitions. We say that a substitution S is a matching substitution for a set C of possibly nonmatching subtyping assertions iff every Sτ_{1} ⊆ Sτ_{2} ∈ SC is matching.

For any S that is a matching substitution for an atomic set C, we define

S • C = ⋃_{σ⊆τ∈C} ATOMIC(Sσ ⊆ Sτ)

The following lemma shows that this definition of • gives us precisely the desired behavior.

Lemma 4.5 If S is a matching substitution for an atomic set C, then S • C is atomic, S • C ⊢ SC, and for all atomic sets C′, C′ ⊢ SC implies C′ ⊢ S • C.

The lemma follows easily from Lemma 4.4 and we omit the details.

We now define our “instance” relation:

Definition 4.6 A typing C′, A′ ⊃ M : σ′ is an instance of the typing C, A ⊃ M : σ by S if S is a matching substitution for C and

C′ ⊢ S • C, A′ ⊇ SA, and σ′ = Sσ.

We often simply say one statement is an instance of another without mentioning the substitution involved.

We wish to prove ultimately that, for any typable expression M , our type inference algorithm infers a “most general” typing; that is, a provable typing for M whose set of instances is exactly the set of provable typings for M . To this end, we follow [Mit84, Mit91] and show that every instance of a provable typing is provable. Then, simply showing that the typing inferred by the algorithm is provable gives the proof of one direction.

Importantly, if we do not subscript row variables but still only consider record types with no duplicate labels to be well-formed, it is no longer true that all instances of a provable typing are provable. For example, consider the following typing (with subscripted variables)

∅, v : {X_{{a}}} ⊃ (fn {a = x; u} ⇒ {u}){a = 3; v} : {X_{{a}}}

which follows from the typing

∅, v : {X_{{a}}} ⊃ fn {a = x; u} ⇒ {u} : {a: int; X_{{a}}} →{X_{{a}}}

by rule app.

The subscript of X_{{a}} ensures that instances can only be obtained from “substitution functions” that do not map X_{{a}} to record types that contain an a field. However, if we omitted the subscripts on row variables, then the only meaningful restriction is to consider “substitution functions” to be well-defined on a type iff the resulting type is well-formed (i.e., does not have duplicate labels). In this case, the typing statement for the first term is syntactically well-formed if we substitute any record type for X . However, the second typing, which is needed to prove the first, becomes ill-formed if we replace X by {a: bool; Y}, say, since this gives a two types. Thus, if we do not subscript row variables, then for the expression (fn {a = x; u} ⇒ {u}){a = 3; v}, there is a instance of a provable typing that is NOT provable.

4.5 Properties of the Typing System

We show in this section that all instances of a provable typing are provable. We need the following two lemmas that show that adding subtype assertions or adding typing assumptions about variables preserves the provability of a typing.

Lemma 4.7 If ⊢ C, A ⊃ M : σ and C′ ⊢ C, where C′ is an atomic set, then ⊢ C′, A ⊃ M : σ.

We state a slightly more complicated lemma for type environments.

Lemma 4.8 Suppose that ⊢ C, A ⊃ M : σ.

1. If w ∈ vars(M) , then w: τ ∈ A for some τ .

2. If w: τ ∈ B for every w: τ ∈ A with w ∈ vars(M) , then ⊢ C, B ⊃ M : σ.

These lemmas are easily proved by induction on the length of the derivation of ⊢ C, A ⊃ M : σ, and the details are left to the reader.

We also need the following lemma, which shows that the rules for deriving subtype assertions are closed under substitution.

Lemma 4.9 If C is an atomic set with C ⊢ σ ⊆ τ , and S is a matching substitution for C, then SC ⊢ Sσ ⊆ Sτ .

The proof proceeds by a simple induction on the length of the derivation of σ ⊆ τ from C, and is omitted.

We now show that all instances of a provable typing are provable. In Section 7, we will make use of this property to show that our type inference algorithm infers most general typings.

Theorem 4.10 Suppose that C′, A′ ⊃ M : σ′ is an instance of C, A ⊃ M : σ by some substitution S. If ⊢ C, A ⊃ M : σ, then ⊢ C′, A′ ⊃ M : σ′.

Proof By Lemma 4.7 and Lemma 4.8, it is sufficient to show that ⊢ S•C, SA ⊃ M:Sσ. We prove this property by induction on the length of the derivation of ⊢ C, A ⊃ M:σ. We give only a few cases here; the remaining cases are left to the reader.

Suppose that ⊢ C, A ⊃ M : σ is proved by the axiom (const). Then M is a built-in constant q with built-in typing C_{q} and τ_{q}, and C, A ⊃ q: σ is an instance of C_{q}, ∅ ⊃ q : τ_{q} by some substitution T . Thus, σ = T τ_{q} and C ⊢ T • C_{q}. We have by Lemma 4.1, Lemma 4.5, and Lemma 4.9 that S ∘ T is a matching substitution for C_{q} and that S • C ⊢ (S ∘ T) • C_{q}. Thus S • C, SA ⊃ q: Sσ is an instance of C_{q}, ∅ ⊃ q: τ_{q} by S ∘ T , and so by (const), we have that ⊢ S • C, SA ⊃ q : Sσ.

For another case, suppose that the final step of the derivation is (rec3). Then M is of the form {f; E} and σ is of the form {h; Z}, where h = h_{1} + h_{2} for some h_{1} and h_{2} such that dom(f) = dom(h_{1}) ≠ ∅, dom(h_{1}) ∩ dom(h_{2}) = ∅, and dom(h_{1}) ⊆ labels(Z) . Moreover, ⊢ C, A ⊃ M : σ must have followed by the antecedents ⊢ C, A ⊃ {∅; E} : {h_{2}; Z} and ∀l ∈ dom(f), ⊢ C, A ⊃ f(l) : h_{1}(l) . By the induction hypothesis, we can assume that ⊢ S • C, SA ⊃ {∅; E} : S{h_{2}; Z}, and that ∀l ∈ dom(f), ⊢ S • C, SA ⊃ f(l) : S(h_{1}(l)) . Let h_{1}′ = S ∘ h_{1} restricted to dom(h_{1}) and let h_{2}′ = S ∘ h_{2} restricted to dom(h_{2}) . We first note that S{h_{2}; Z} = {(h_{2}′ + h_{S}); Z_{S}}, where {h_{S}; Z_{S}} = S{∅; Z}. Due to our definition of substitution on record types, it is easy to show that the above conditions imply that dom(h_{1}′)∩(dom(h_{2}′)∪dom(h_{S})) = ∅ and that dom(h_{1}′) ⊆ labels(Z_{S}) . Noting that S{h; Z} = {(h_{1}′ + h_{2}′ + h_{S}); Z_{S}}, we can infer by (rec3) that ⊢ S • C, SA ⊃ {f; E}: Sσ, proving this case.

For another case, suppose that the final step of the derivation was (coerce). Then, for some type γ, ⊢ C, A ⊃ M:σ must have followed by the antecedents ⊢ C, A ⊃ M:γ and C ⊢ γ ⊆ σ. By Lemma 4.5 and Lemma 4.9, we have that S • C ⊢ Sγ ⊆ Sσ. Since the proof of ⊢ C, A ⊃ M : γ is shorter than that of ⊢ C, A ⊃ M : σ, we can assume inductively that ⊢ S • C, SA ⊃ M : Sγ. By (coerce), we can infer that ⊢ S • C, SA ⊃ M : Sσ, proving this case.

4.6 Most General Typings

We say that a typing C, A ⊃ M : σ is a most general typing for M iff the set of its instances is exactly the set of provable typings for M .

In ML, all most general typings for a given expression are identical, except for the names of type variables. By definition, all most general typings for a given ML^{+} expression are instances of one another. However, this is more complicated than one might expect. For example,

{t_{1} ⊆ t_{2}}, ∅ ⊃ fn x ⇒ x : t_{1} → t_{2}

and

{r_{1} ⊆ r_{2}, s_{1} ⊆ s_{2}}, ∅ ⊃ fn x ⇒ x : s_{1} → s_{2}

are both most general typings of the identity function, since every typing of fn x ⇒ x is an instance of both of them, even though one has redundant subtyping assertions. The instance relation is decidable and np-hard.

Proposition 4.11 Let instance be the following problem: given any typings C, A ⊃ M : σ and C′, A′ ⊃ M : σ′, is C′, A′ ⊃ M : σ′ an instance of C, A ⊃ M : σ? instance is decidable, but is np-hard.

Proof The procedure for deciding instance uses the algorithms unify and match from the next two sections, and is fairly straightforward. We omit the details.

The proof of np-hardness for instance is a consequence of a result of [WO89], which proves the np-hardness of the problem (po-sat): given a partial order P over base types and a set C of subtype assertions between type variables and base types, is there a ground substitution S from type variables to base types such that P ⊢ SC? It is easy to show that for any such sets P and C, the existence of an arbitrary substitution T (from type variables to ML^{+} types) with P ⊢ T C implies the existence of a ground substitution S with P ⊢ SC. It is then easy to see that po-sat can be reduced to the question of whether P, ∅ ⊃ 3 : int is an instance of C, ∅ ⊃ 3 : int , proving the lemma.

The same result holds for the typing system of [Mit84, Mit91].

5 Unification

A unifier is a substitution that makes two types syntactically equal. More generally, if E is a set of pairs of types, then substitution S unifies E if Sσ = Sτ for every pair ⟨σ, τ⟩ ∈ E. Since such a set of pairs may be regarded as a set of equations to be solved, we often write the pairs ⟨σ, τ⟩ ∈ E in the form σ = τ . Recall that we consider ⟨h, Z⟩ and ⟨h′; Z′⟩ syntactically equal iff h and h′ define the same function from labels to types and Z and Z′ are syntactically equal.

As in ML typing, we use unification to combine most general typing statements about subexpressions. Following [Rob65], we would like to define a most general unifier for a set E of equations as any substitution S that unifies E and has the property that for all substitutions T that unify E, there exists a substitution U with T = U ∘ S. However, a difficulty arises with extended record types. First, since the subscript of a row variable may change during unification, we need to use “fresh” row variables. For example, consider the equation

{a: int; X_{{a}}} = {b: bool; Y_{{b}}}

Clearly, any substitution that unifies these expressions must map Y_{{b}} to a record type that contains at least an a:int field and must map X_{{a}} to a record type that contains at least a b:bool field. Furthermore, the “rest” of X_{{a}} and Y_{{b}} must be identical, and must never contain an a or a b field. Thus, the most general substitution substitution S that unifies this equation is

S = [{b: bool; W_{{a,b}}}/X_{{a}}, {a: int; W_{{a,b}}}/Y_{{b}}]

for some row variable W_{{a,b}} that does not occur anywhere in the set of equations that we are unifying. However, we may have unifying substitutions whose behavior on W_{{a,b}} “conflicts” with the behavior of S. For example, consider the substitution

T = [{b: bool; null}/X_{{a}}, {a: int; null}/Y_{{b}}, {c: real; null}/W_{{a,b}}]

Clearly, T unifies the equation under consideration. However, since any substitution U with T = U ∘ S must map W_{{a,b}} to {null}, the action of U ∘ S on W_{{a,b}} differs from that of T . Therefore, there is no such substitution U , from which it follows that S cannot be the most general unifier for E. Furthermore, since there are an infinite number of substitutions that unify the equation, we cannot choose the “fresh” row variable in S so as to always avoid this problem.

We thus introduce a “restricted” form of equality over substitutions, where we say that S is equal to T with respect to a set Q of type and row variables, written S =_{Q} T , if ∀t ∈ Q, St = T t and ∀X_{L} ∈ Q, S{∅; X_{L}} = T {∅; X_{L}}.

We also need to define what it means for a type or row variable to “occur in” a type, a function from labels to types, a set of equations between types, a set of subtype assertions, or a typing statement. These definitions are just the expected ones, but since they are important in our algorithms and proofs of correctness, we write them in detail here. We give the definition for types inductively as follows:

• t occurs in t

• t occurs in {h; Z} iff t occurs in h(l) for some l ∈ dom(h)

• X_{L} occurs in {h; Z} iff X_{L} occurs in h(l) for some l ∈ dom(h) or X_{L} and Z are the same row variable

• t occurs in σ → τ iff t occurs in σ or t occurs in τ

• X_{L} occurs in σ → τ iff X_{L} occurs in σ or X_{L} occurs in τ

Furthermore, we say that t occurs in a function h from labels to types iff t occurs in h(l) for some l ∈ dom(h) . We say that t occurs in a set E of equations between types iff, for some σ = τ ∈ E, t occurs in σ or τ . The definition is similar for sets C of subtype assertions. Finally, we say that t occurs in a typing statement C, A ⊃ M:σ iff t occurs in C, t occurs in τ for some x: τ ∈ A, or t occurs in σ. All of these definitions are analogous for row variables.

A substitution S is a most general unifier for E with respect to Q iff S unifies E and, for all substitutions T that unify E, there exists a substitution U such that T =_{Q∪Q_{E}} U ∘ S, where Q_{E} is the set of type and row variables occurring in E. The idea behind this restriction is that, while computing S, we may choose “fresh” row variables that are not in Q ∪ Q_{E}. Since we have an infinite number of row variables with any subscript, choosing Q to be a finite set of type and row variables will ensure that we can always choose such “fresh” row variables, thus getting the behavior we desire. (In fact, for the purposes of defining most general unifiers, it is sufficient to have Q be just a finite set of row variables. However, as we shall see in Section 6, a somewhat similar difficulty arises elsewhere in type inference, this time due to “fresh” type variables. Thus, anticipating the later difficulty, we include type variables in our set Q here.)

Our algorithm unify takes a set of equations E between type expressions and a finite set Q of type and row variables and produces a most general unifying substitution for E with respect to Q. If no unifier exists for E, then unify terminates in error. unify is a modification of Robinson’s unification [Rob65], extended to solve equations between extended record types, and is quite similar to the unification algorithm described in [Wan87]. However, a subtle bug in Wand’s algorithm is avoided by the syntactic restriction in ML^{+} prohibiting duplicate field names within a record. Because the language of [Wan87] does not make this syntactic restriction, the algorithm given in [Wan87] for equations between row expressions is incorrect for his system; however, our slightly modified version is correct for our system. Wand’s corrected algorithm, which appears in [Wan88], needs to compute a set of most general unifiers, while our algorithm computes a single most general unifier. Another bug arises in Wand’s algorithm for unifying two extended record types, this time in his proof of termination. As we will discuss in the proof of correctness of our algorithm, Wand’s termination proof is incorrect because his halting measure does not necessarily decrease after every iteration of the algorithm. On the other hand, this halting measure does give a proof of termination for our modified algorithm.

Due to the number of subtle bugs in Wand’s algorithm, we present our unify algorithm in detail in Appendix A, where we also provide the proof of correctness.

Lemma 5.1 Let E be a set of equations of the form σ = τ , where σ and τ are types, and let Q be a finite set of type and row variables. Whenever there is a unifying substitution for E, unify(E, Q) produces a most general unifier for E with respect to Q. Otherwise, unify(E, Q) terminates in error.

6 Matching

Using unification, we can find common substitution instances for our type environments; however, these substitutions may not be matching for our sets of subtyping assertions. Therefore, we need to be able to compute a “most general matching substitution” for this resulting set of possibly non-matching subtype assertions. A useful property of matching is that the problem of finding a most general matching substitution for a set C of subtype assertions can be reduced to the problem of finding a most general unifying substitution for a set E that is closely related to C. The main idea here is that we treat the set C as a set of equations (rather than subtype relations) between types, unify this set of equations, and then replace all occurrences of type variables and row variables in the resulting types by distinct “fresh” type and row variables. There is a minor complication, however, due to base types, since two distinct base types match but do not unify. In order to get around this difficulty, we first replace all base types in C by a special type variable, and then check that the most general unifier merely renames this special type variable.

Due to the “fresh” type and row variables introduced in this process, we must restrict our notion of “most general” in a manner similar to that for unification. In particular, if C is a set of possibly non-matching subtype assertions and Q is a set of type and row variables we say that a substitution S is a most general matching substitution for C with respect to Q iff S is a matching substitution for C and, for all matching substitutions T for C, there exists a substitution U such that T =_{Q∪Q_{C}} U ∘ S, where Q_{C} is the set of type and row variables occurring in C. If we incorporate the set Q appropriately into the above procedure for extracting matching substitutions, we can use the properties of most general unifiers to show that the resulting substitution is a most general matching substitution for C with respect to Q.

Using these ideas, our algorithm match takes a set C of possibly non-matching subtype assertions and a finite set Q of type and row variables and produces a most general matching substitution for C with respect to Q. If no matching substitution for C exists, then match terminates in error. We give the definition of match as well as its proof of correctness in Appendix B.

Lemma 6.1 Let C be a set of subtype assertions of the form σ ⊆ τ , where σ and τ may not necessarily match, and let Q be a finite set of type and row variables.

Whenever there is a matching substitution for C, match(C, Q) produces a most general matching substitution with respect to Q. Otherwise, match(C, Q) terminates in error.

7 The Type Inference Algorithm

Our type inference algorithm, type, is defined inductively on the expressions of ML^{+} . type is written in an applicative, pattern-matching style, and is defined by the mutually recursive clauses given in Table 4. The algorithms unify and match play a crucial role in type, while a subsidiary role is played by the • operation and algorithms for constructing types, applying substitutions, composing substitutions, subtracting two type environments, computing the union of two type environments, and pasting two functions mapping labels to types. All of these subsidiary algorithms are assumed to fail when the desired result is not well-defined. For example, while we may write {h_{1} + h_{2}; Z} when constructing a record type, we assume in our algorithm type that if the record type is not well-formed, then the entire algorithm will terminate in error. This notational convention makes the pseudo-code in Table 4 more readable. type is described informally below.

The behavior of type on constants of base type, variables, and empty fixed records is quite straightforward. For any constant c of base type, type infers that c is of some supertype t of the built-in type of c. For any variable x, type infers that x is of some supertype t of the assumed type s of x. The type of {∅; empty} is simply {∅; null}.

Since we prohibit duplicate labels within record types, the typing of an empty flexible record {∅; u} is somewhat more complicated, and depends on the context of the particular occurrence of u. Namely, if the particular occurrence of u is in a record expression that has labels L = {l_{1}, …, l_{n}}, then we want the type of u to be a record that cannot contain any of the l_{i}. Thus, the type of {∅; u} is essentially a type {∅; X_{L}}. However, since we want to take subtyping into account, we put the assumption u: {∅; X_{L}} into the type environment, and give the type of {∅; u} as some supertype {∅; Y_{L}} of {∅; X_{L}}.

The typing of built-in constants q is fairly straightforward: the type of q is essentially inferred to be of some unspecified supertype t of its built-in typing τ_{q}. However, since τ_{q} ⊆ t is not necessarily matching, type applies an appropriate matching substitution and returns the resulting typing.

For “compound” expressions (namely, non-empty records, function abstractions, and function applications), type computes a typing statement for each of the toplevel components by calling itself recursively. Due to the behavior of type on simple expressions, the same variables s, t, X_{L}, Y_{L} typically occur in the typings of unrelated components of the compound expression; thus, type first renames all type and row variables in different typings to be distinct. Using a series of steps, type combines these typings into a well-formed typing statement for the compound expression. First, type uses unification (i.e., unify) to combine type environments. In particular, if a variable or extension variable occurs in different components, then the type assumptions made about these distinct occurrences are unified. Furthermore, if the expression is a function application MN , then for obvious reasons, the type of M is unified with a function type that maps the type of N to some unspecified type t. Second, type applies the resulting unifiers to the sets of (atomic) subtype assertions in the original typing statements and then uses match to compute a substitution that causes these new subtype assertions to match. The unifier and this matching substitution are composed and applied to the original typing statements, using the • operation on the sets of subtype assertions. Finally, taking a (point-wise) “union” of the corresponding pieces of the resulting typing statements yields a (well-formed) typing statement for the compound expression.

One technicality arises from the fact that unify and match only compute most general substitutions with respect to some set of type and row variables. In order for type to yield most general typings, the “fresh” type and row variables used by unify and match must not occur anywhere in the typings computed previously. type thus keeps track of the set of type and row variables occurring in the typings of the components, adds any new type or row variables that arise, and passes this entire set to unify. Since the call to unify adds some row variables to the typings, the argument to passed to match is actually this set together with the set of “fresh” row variables used by unify.

7.1 Soundness

In this section, we prove that type is sound with respect to the typing system. More precisely, for any expression M , if type(M) yields a typing statement, then every instance of that typing is derivable in the typing system. By Theorem 4.10, it suffices to prove that the typing produced by type(M) is provable. In the proof, we extend unification to type environments and say that S unifies A_{1} and A_{2} if, for all variables and extension variables w, w : α ∈ A_{1} and w : β ∈ A_{2} implies that Sα is syntactically equal to Sβ.

Lemma 7.1 If type(M) succeeds and yields C, A ⊃ M : σ, then ⊢ C, A ⊃ M : σ.

Proof The lemma is proved by induction on the structure of terms. We give the proof for two cases; the remaining cases are left to the reader.

If M is of the form fn P ⇒ M′, then we can assume inductively that ⊢ C_{P} , A_{P} ⊃ P : σ, and that ⊢ C_{M′}, A_{M′} ⊃ M′ : τ . Since type(M) succeeds, we can assume that S is a matching substitution for C_{P} and C_{M′} . Thus, by Theorem 4.10, we have that ⊢ S • C_{P} , SA_{P} ⊃ P : Sσ, and that ⊢ S • C_{M′}, SA_{M′} ⊃ M′ : Sτ . Since, by assumption, S unifies A_{P} and A_{M′} , we have that

(SA_{M′})[SA_{P}] = SA_{P} ∪ SA_{M′}

and is a well-defined set. Thus, by Lemma 4.7 and Lemma 4.8, we can conclude that

⊢ S • C_{P} ∪ (S • C_{M′})^{op} , SA_{P} ⊃ P : Sσ

and that

⊢ (S • C_{P})^{op} ∪ S • C_{M′} , (SA_{M′})[SA_{P}] ⊃ M′ : Sτ.

By a sub-induction on the structure of terms, we can show that vars(A_{P}) = vars(P) , and so vars(SA_{P}) = vars(P) . It then follows easily by a use of rule (abs) and Lemma 4.8 that

⊢ (S • C_{P})^{op} ∪ S • C_{M′} , SA_{M′} − SA_{P} ⊃ fn P ⇒ M′ : S(σ → τ),

proving this case.

Table 4: Mutually recursive clauses for Algorithm type

type(c) = {b ⊆ t}, ∅ ⊃ c: t, where b is the built-in type of c

type(x) = {s ⊆ t}, {x: s} ⊃ x: t

type(q) =

let C_{q}, ∅ ⊃ q : τ_{q} be the built-in typing for q

S = match(C_{q} ∪ {τ_{q} ⊆ t}, Q ∪ {t}) , where t does not occur in C_{q} or in τ_{q} return S • C_{q} ∪ S • {τ_{q} ⊆ t}, ∅ ⊃ q : St

where Q = the set of type and row variables occurring in C_{q} or in τ_{q}

type(MN) =

let C_{M}, A_{M} ⊃ M : σ = type(M)

C_{N}, A_{N} ⊃ N : τ = type(N)

with type and row variables renamed to be distinct from those in type(M) T = unify({α = β | w: α ∈ A_{M} and w: β ∈ A_{N}} ∪ {σ = τ → t}, Q ∪ {t}) , where t ∉ Q S = match(T C_{M} ∪ T C_{N}, Q ∪ Q_{T}) ∘ T

return S • C_{M} ∪ S • C_{N}, SA_{M} ∪ SA_{N} ⊃ MN : St, where Q = the set of type and row variables occurring in C_{M}, A_{M} ⊃ M : σ or in C_{N}, A_{N} ⊃ N : τ and Q_{T} = the set of type and row variables occurring in T t or T {∅, X_{L}}, where t, X_{L} ∈ Q

type(fn P ⇒ M) =

let C_{P} , A_{P} ⊃ P : σ = type(P)

C_{M}, A_{M} ⊃ M : τ = type(M)

with type and row variables renamed to be distinct from those in type(P) T = unify({α = β | w: α ∈ A_{P} and w: β ∈ A_{M}}, Q) S = match(T C_{P} ∪ T C_{M}, Q ∪ Q_{T}) ∘ T

return (S • C_{P})^{op} ∪ S • C_{M}, (SA_{M} − SA_{P}) ⊃ fn P ⇒ M : S(σ → τ) , where Q = the set of type and row variables occurring in C_{P} , A_{P} ⊃ P : σ or in C_{M}, A_{M} ⊃ M : τ and Q_{T} = the set of type and row variables occurring in T t or T {∅, X_{L}}, where t, X_{L} ∈ Q

type({f; E}) =

for all l ∈ dom(f) , let C_{l}, A_{l} ⊃ f(l) : σ_{l} = type(f(l))

with type and row variables renamed to be distinct from those in C_{l′}, A_{l′} ⊃ f(l′) : σ_{l′} for all l′ ∈ dom(f) with l′ ≠ l

if E is empty then let C_{E}, A_{E} ⊃ {∅; E}: {∅; Z} = ∅, ∅ ⊃ {∅; E}: {∅; null} else let C_{E}, A_{E} ⊃ {∅; E}: {∅; Z} =

{{∅; X_{dom(f)}} ⊆ {∅; Y_{dom(f)}}}, {E : {∅; X_{dom(f)}}} ⊃ {∅; E}: {∅; Y_{dom(f)}}

where X_{dom(f)} and Y_{dom(f)} do not occur in any of the C_{l}, A_{l} ⊃ f(l) : σ_{l}

let E = {α = β | w: α ∈ A_{l} and w: β ∈ A_{l′} for distinct l, l′ ∈ dom(f)}

∪ {α = β | w: α ∈ A_{E} and w: β ∈ A_{l} for some l ∈ dom(f)} T = unify(E, Q) S = match(T C_{E} ∪ ⋃_{l∈dom(f)} T C_{l}, Q ∪ Q_{T}) ∘ T

return (S • C_{E} ∪ ⋃_{l∈dom(f)} S • C_{l}), (SA_{E} ∪ ⋃_{l∈dom(f)} SA_{l}) ⊃ {f; E}: {(h′ + h_{S}); Z_{S}}

where {h_{S}; Z_{S}} = S{∅; Z}, dom(h′) = dom(f) , and ∀l ∈ dom(h′), h′(l) = Sσ_{l} ,

and Q = the set of type and row variables occurring in any of the C_{l}, A_{l} ⊃ f(l) : σ_{l}

or in C_{E}, A_{E} ⊃ {∅; E}: {∅; Z}

and Q_{T} = the set of type and row variables occurring in T t or in T {∅, X_{L}}, where t, X_{L} ∈ Q

If M is of the form {f; E}, then we can assume inductively that for all l ∈ dom(f), ⊢ C_{l}, A_{l} ⊃ f(l) : σ_{l}. If E is empty, it is easy to see that ⊢ C_{E}, A_{E} ⊃ {∅; E}: {∅, Z} is provable by (rec1). Otherwise, E is an extension variable u. By axiom (rec2), we have that ⊢ C_{E}, A_{E} ⊃ {∅; E}: {∅, X_{dom(f)}}, A use of (coerce) then yields ⊢ C_{E}, A_{E} ⊃ {∅; E}: {∅, Z}, as desired. Since type succeeds, we can assume that S is a matching substitution for C_{E} and for all the C_{l}. Thus, by Theorem 4.10, we have that ⊢ S•C_{E}, SA_{E} ⊃ {∅; E}:S{∅; Z} and that for all l ∈ dom(f), ⊢ S•C_{l}, SA_{l} ⊃ f(l):S(σ_{l}) .

Since, by assumption, type(M) succeeds, we can assume that SA_{E} ∪ ⋃_{l∈dom(f)} SA_{l} is a well-defined set. Thus, by Lemma 4.7 and Lemma 4.8, we can infer that

⊢ S • C_{E} ∪ ⋃_{l∈dom(f)} S • C_{l} , SA_{E} ∪ ⋃_{l∈dom(f)} SA_{l} ⊃ {∅; E}: S{∅; Z}

and that

∀l ∈ dom(f), ⊢ S • C_{E} ∪ ⋃_{l∈dom(f)} S • C_{l} , SA_{E} ∪ ⋃_{l∈dom(f)} SA_{l} ⊃ f(l) : S(σ_{l}).

Since type succeeds, we have that dom(h′) ∩ dom(h_{S}) = ∅, and that dom(h′) ⊆ labels(Z_{S}) . If f = ∅, then we are already done. Otherwise, a use of (rec3) yields

⊢ S • C_{E} ∪ ⋃_{l∈dom(f)} S • C_{l} , SA_{E} ∪ ⋃_{l∈dom(f)} SA_{l} ⊃ {f; E}: {h′ + h_{S}; Z_{S}},

as desired.

From Theorem 4.10 and Lemma 7.1, we have the following theorem:

Theorem 7.2 If type(M) succeeds and yields C, A ⊃ M : σ, then every instance of C, A ⊃ M : σ is provable.

7.2 Completeness

This section proves that type is complete with respect to the typing system. More precisely, for any expression M , if a typing for M is derivable in the typing system, then type yields a typing statement of which the provable typing for M is an instance.

Due to the rule (coerce) there may be many possible derivations for a provable typing. However, we show that as in [Mit84, Mit91], every typing derivation may be put in a certain “normal form”, in which the rule (coerce) is used only after the axioms in the typing system. Reasoning about the normal form derivation of provable typings greatly simplifies the proof of Theorem 7.5.

Lemma 7.3 Suppose C, A ⊃ M:σ is provable. Then there is a derivation in which rule (coerce) is used only immediately after the typing axioms (int), (real), (bool), (string), (var), (rec1), (rec2), and (const).

We omit the proof, as it is analogous to [Mit84, Mit91].

In our proof of Theorem 7.5, we will need the following property of substitutions, which shows that substitution composition combines naturally with the operation •.

Lemma 7.4 Suppose that C is a set of subtype assertions between possibly non-matching types. Furthermore, suppose that S, T and W are substitutions with W =_{Q} S ∘ T , where Q contains all type and row variables that occur in C. If W and T are matching substitutions for C, then S is a matching substitution for (T • C) , and S • (T • C) = W • C.

The proof follows by a simple induction on types and is omitted.

We now prove the completeness of algorithm type with respect to the typing rules.

Theorem 7.5 If ⊢ C, A ⊃ M : γ, then type(M) succeeds and produces a typing statement with C, A ⊃ M : γ as an instance.

Proof The theorem is proved by induction on the structure of terms. We give the proof for one record case; the remaining cases are left to the reader.

Suppose that M is of the form {f; E}, where f is non-empty, and that ⊢ C, A ⊃ M : γ. By Lemma 7.3, we can assume without loss of generality that the proof ends in a use of (rec3). Thus, γ = {h_{1} + h_{2}; Z′} for some h_{1} , h_{2} , and Z′ such that dom(f) = dom(h_{1}) , dom(h_{1}) ∩ dom(h_{2}) = ∅, and dom(h_{1}) ⊆ Z′. Furthermore, we have that ⊢ C, A ⊃ {∅; E}: {h_{2}; Z′} and that ∀l ∈ dom(f), ⊢ C, A ⊃ f(l) : h_{1}(l) . We can thus assume inductively that for all l ∈ dom(f) , C, A ⊃ f(l) : h_{1}(l) is an instance of type(f(l)) by some substitution V_{l}. Thus, for all l ∈ dom(f) , V_{l} is a matching substitution for C_{l} and C ⊢ V_{l} • C_{l}, A ⊇ V_{l}A_{l}, and h_{1}(l) = V_{l}(σ_{l}) .

If E is empty, then it follows by the definition of the match relation on types, Lemma 4.1, and Lemma 7.3 that {h_{2}; Z′} = {∅; null}. Let V_{E} = ∅. It is easy to see that V_{E} is a matching substitution for C_{E} , and C ⊢ V_{E}•C_{E}, A ⊇ V_{E}A_{E}, and {h_{2}; Z′} = V_{E}{∅; Z}.

If E is an extension variable u, then by Lemma 7.3, we can assume without loss of generality that the proof consists of a use of (rec2) followed by a use of (coerce). By Lemma 4.8, u must occur in A. Let {h_{3}; Z′′} be the type expression with u:{h_{3}; Z′′} ∈ A, and note that C ⊢ {h_{3}; Z′′} ⊆ {h_{2}; Z′}. By Lemma 4.1, {h_{3}; Z′′} and {h_{2}; Z′} must match. Thus, dom(h_{3}) = dom(h_{2}) , ∀l ∈ dom(h_{3}), h_{3}(l) matches h_{2}(l) , and Z′′ and Z′ are either both null or are both row variables with the same label set. Let V_{E} = [{h_{2}; Z′}/Y_{dom(f)}, {h_{3}; Z′′}/X_{dom(f)}] . By the assumptions above, it is easy to show that V_{E} is a well-defined substitution and is a matching substitution for C_{E} ; thus, by Lemma 4.5, we can conclude that C ⊢ V_{E} • C_{E} . Moreover, since u: {h_{3}; Z_{3}} ∈ A, it follows that A ⊇ V_{E}A_{E} . Finally, it is easy to see that {h_{2}; Z′} = V_{E}{∅; Z}.

Since the type and row variables that occur in the C_{l}, A_{l} ⊃ f(l) : σ_{l} are all distinct and X_{dom(f)}, Y_{dom(f)} do not occur in any of them, there is a well-defined substitution V such that V agrees with V_{E} on X_{dom(f)} and Y_{dom(f)} , and agrees with V_{l} on all type variables and on row variables that occur in the C_{l}, A_{l} ⊃ f(l) : σ_{l}. It is easy to see that V is a matching substitution for C_{E} and for all the C_{l} and that

C ⊢ V • C_{E}, A ⊇ V A_{E}, and V {∅; Z} = {h_{2}; Z′}

and for all l ∈ dom(f) ,

C ⊢ V • C_{l}, A ⊇ V A_{l}, and h_{1}(l) = V (σ_{l}).

Thus, V must unify A_{E} and all of the A_{l}, and so we can conclude by Lemma 5.1 that unify(E, Q) succeeds and that V =_{Q∪Q_{E}} U ∘ T for some substitution U . It is easy to see that U must be a matching substitution for T C_{E} and for all of the T C_{l}. Thus, by Lemma 6.1, we can assume that match(T C_{E} ∪ ⋃_{l∈dom(f)} T C_{l}, Q ∪ Q_{T}) succeeds and that U =_{Q∪Q_{T}} W ∘ match(T C_{E} ∪ ⋃_{l∈dom(f)} T C_{l}, Q ∪ Q_{T}) for some substitution W . Therefore,

V =_{Q} W ∘ match(T C_{E} ∪ ⋃_{l∈dom(f)} T C_{l}, Q ∪ Q_{T}) ∘ T =_{Q} W ∘ S.

Using Lemma 5.1 and Lemma 6.1, it is easy to show that S is a matching substitution for C_{E} and for all the C_{l} and that SA_{E} ∪ ⋃_{l∈dom(f)} SA_{l} is well-formed. We now need to show that {(h′ + h_{S}); Z_{S}} is a well-formed type expression. For one case, suppose that Z = null . Then h_{S} = ∅ and Z_{S} = null , so it is easy to see that the desired conclusion holds. For the other case, we must have that Z = Y_{dom(f)} . By the definition of substitutions, it follows that dom(h_{S}) ∩ dom(f) = ∅, dom(f) ⊆ labels(Z_{S}) , and dom(h_{S}) ⊆ labels(Z_{S}) . Thus, it is easy to show that {(h′ + h_{S}); Z_{S}} is a wellformed type expression, and we can thus conclude that type({f; E}) succeeds. Using Lemma 7.4, it is straightforward to show that C, A ⊃ {f; E} is an instance of type({f; E}) by W , proving this case.

8 Comparison with related work

As mentioned earlier, the use of row variables to describe the inherent polymorphism of record operations is due to Wand [Wan87]. However, the row variables in our system differ from those used in [Wan87] in that our row variables are subscripted with sets of labels. In the terminology of [CM91, HP91], our subscripted row variables impose “negative constraints” on records in which they appear, since no sequence of labeled types that contains a label occurring in the subscript of a row variable can be substituted for that row variable. For example, the record type {a: int, X_{{a,b}}} will not contain a b field under any instantiation of row variables. We have made the further restriction that whenever a row variable appears in a record type, the subscript on the row variable contains the labels of all the fields in the record type. For example, the record type {a : int, X_{{a,b}}} is well-formed, but {a : int, X_{{b}}} is not. If we insist that all labels explicitly appearing in a record be distinct, these restrictions ensure that duplicate labels cannot appear in our record types under any instantiation of row variables. This leads to certain considerations in our typing algorithm, and also the point of departure from Wand’s previous work. While Wand allowed type expressions with multiple occurrences of field names (using order of occurrence to determine precedence), this in fact leads to a set of most general typings. In a sense, the difficulty with Wand’s algorithm begins with his expression language. Wand’s with expression has two informal readings: the expression x with a: = 3 has the effect of either modifying the a field of x if there is one, or adding one if there is not. From a type checking point of view, it is not clear whether we should assume x has an a field or not, and so there are two typings to consider.

We avoid these technical problems associated with Wand’s language by forbidding duplicate labels in a record, subscripting our row variables, and using extended pattern matching instead of with. Together, these two restrictions avoid the ambiguity of Wand’s expressions by compelling the programmer to choose which interpretation he wants his expression to have. For example, the expression λx. (x with a: = 3) in Wand’s system translates to two expressions in ML^{+} , namely fn {a = y; u} ⇒ {a = 3; u} and fn {u} ⇒ {a = 3; u}. The first expression constrains the argument record to have an a field, while the second expression constrains the argument record not to have an a field. This contrasts with the expression in Wand’s system, which allows a record either with or without an a field to be passed as an argument. Aside from translating ambiguous expressions in Wand’s language to sets of expressions, ML^{+} seems to have all of the expressive power of Wand’s system, while generating single most general typings.

We note that this expressive power is due to pattern matching, and making a similar restriction on the records in Wand’s system would greatly restrict the expressive power of that language. For example, the expression λx. (x with a: = x.a + 1) in Wand’s system would not be typable with this restriction, since the result would have two a fields. However, by using extended pattern matching, we can write this expression in ML^{+} as fn {a = y; u} ⇒ {a = y + 1; u}.

There are some functions that we can write in ML^{+} that are not expressible in Wand’s language. One such function is

fn {a = y; u} ⇒ {u}

which removes the a field from a record. Another such expression in ML^{+} is

fn {a = y; empty} ⇒ y.

Although Wand’s language can conceivably be extended to have this expressive power, there are some problems. First, it seems difficult, and perhaps even impossible, to define and type a “ remove_{a} ” operation that removes the a field from a record and prevents the resulting record from later being instantiated with an a field. Second, an operation “ exactly_{L} ” that restricts a record to have exactly a certain set L of labels has precisely the same sort of ambiguity with respect to overwritten fields as that of the with construct, and thus also leads to a set rather than a single most general typing.

Between the time that [JM88] was published and the time that this paper was completed, Rémy [Rém89] has resolved some of the technical difficulties of [Wan87] without imposing any restrictions on duplicate fields in records; see also [Rém90a, Rém90c, Rém90d, Rém90b]. His system also incorporates variants and recursive types. Rémy’s main technical innovation is a new perspective on records in the context of a finite set of labels. All records are assumed to contain fields corresponding to all labels in the (finite) set; however, only some of the fields need to contain values. The fields that do not contain values are considered to be “uninitialized”, but must be written out explicitly. However, in a later paper [Wan89], Wand extends Rémy’s system to an infinite set of labels using row variables, so that only the fields that play a role in a certain expression need be written explicitly. Using flags as well as types, Rémy’s system assigns an “absent” flag to an uninitialized field and either a flag variable ϵ(σ) or a “present( σ)” flag to an initialized field, where σ is the type of the value associated with that field. (The system of [Wan89] is similar, but does not use flag variables.)

Rémy’s type system, extended to infinite label sets as in [Wan89], is richer than both the system of [Wan87] and our system without atomic subtyping. In fact, in Rémy’s system, all of the typable expressions in the language of [Wan87] have single most general typings. For example, the expression λx. (x with a: = 3) has the type {a : ϵ(t); ρ} →{ρ}, where ρ denotes the rest of the fields of the record, and the flag variable ϵ(t) indicates that the a field may or may not be initialized. In particular, ϵ(t) may be unified with the “absent” flag or with the “present( σ)” flag. (To be technically precise, Rémy introduced three related systems, each of which treats uninitialized fields slightly differently, and thus defines the unification of flag variables with uninitialized flags slightly differently. We omit the details here.) If we omit atomic subtyping from our system, then all expressions that are typable in our system can be translated into Rémy’s language and typed in his system. In particular, expressions corresponding to “forgetting” fields of a record can be translated directly, while expressions denoting that a record must have exactly a certain set of (initialized) fields can be translated into a straightforward extension of his language. Furthermore, Rémy’s system can type expressions that are not typable in either the system of [Wan87] or our complete system. For example, his approach would assign to the expression^{2}

if x then {a = 3, b = true} else {a = 5}

essentially the record type containing an a that may be considered to be an integer field, and in which all other fields are uninitialized. However, under both our approach and the approach of [Wan87], the types of these records are not unifiable, and thus, this expression would not be typable.

Although the system of [Wan87] is a special case of Rémy’s system, the relationship is more complicated for ML^{+} . Although any ML^{+} expression that is typable without atomic subtyping can be translated into a typable expression in Rémy’s language, our system without atomic subtyping is not a special case of Rémy’s system. In particular, our system distinguishes a larger class of type errors than that of Rémy’s system. For example, our type inference algorithm generates a type error if the function fn {u} ⇒ {a = 3; u} is applied to a record with an a field, thus avoiding the situation in which a programmer unwittingly overwrites a field. Since at this moment it is unclear what sorts of languages and type systems are desirable for object-oriented programming, it may turn out later on that the larger class of type errors in ML^{+} is advantageous to programmers. The above example shows that there is some question as to whether the ambiguous expressions in Wand’s system should be typable. For a further argument supporting this point of view, the reader is referred to [CM91].

On the other hand, language designers may consider the system of [Rém89, Rém90c] more desirable than our system, since Rémy’s system types more expressions than ours, his system incorporates variants and recursive types, and his type inference algorithm uses the usual unification algorithm rather than the extension to unification suggested in [Wan87] and repaired here. However, Rémy has not yet incorporated atomic subtyping into his system, although it is conceivable that the two can be merged in a natural manner.

In addition to the three papers discussed in detail above, a host of other papers on this topic have been published in the past few years [Sta88, FM89, FM90, OB88, OB89, Wan89, CCH^{+} 89, CM91, HP91], presenting different languages, type systems, and type inference algorithms that support various “object-oriented” features. We give a brief comparison of these systems here.

If we only consider the core language consisting of variables, records, lambda abstraction, and function application in all the systems, then the system of [Car84, Car88] is incomparable with the system of [Wan87] and our system. For example, the [Car84, Car88] approach would assign the expression

if x then {a: = 3, b: = true} else {a: = 5, b: = λx. x}

the type {a: int}, since this is the least upper bound of the record types {a: = 3, b: = true} and {a: = 5, b: = λx. x}. However, under both our approach and the approach of [Wan87], the types of these records are not unifiable, and thus, this expression is not typable. On the other hand, one cannot translate into Cardelli’s system any expression semantically equivalent to

((λx. x with a: = x.a + 1){a: = 3, b: = y}).b

2 Although an “if” statement is not directly expressible is some of the languages discussed here, it is a simple matter to type such a statement. Namely, the if-clause must be a boolean, and both arms of the statement must have a “least” type in common.

where b is an arbitrary label. In Cardelli’s system, the type of a lambda-bound variable must be declared, and since there is no mechanism to express the “rest of a record”, the type of a lambda-bound record must have a certain fixed set of fields. Thus, the record argument must be coerced to have that same fixed set of fields, and, in general, applying a function to a record with more fields results in the loss of the “extra” fields.

A type inference algorithm for a language based on [Car84, Car88] is presented in detail in [Sta88], which generates a set of subtype relations between records that are satisfied whenever a typing for an expression is derivable. However, no algorithm that checks the satisfiability of sets of such subtype relations is presented, and so, principal types may be empty. As a consequence, given an untypable expression, the algorithm given in [Sta88] does not necessarily indicate that no typing exists for that expression. Furthermore, like that of [Car84, Car88], the language of [Sta88] does not contain any general mechanism for record extension or modification, and so the system of [Sta88] is incomparable to our system as well as the system of [Wan87].

[OB88] presents a somewhat different core language that introduces sets, joins, and projections in the context of subtyping of records, and provides type inference for this language. Because of the restrictions upon the join operation, this system is incomparable to our system and those of [Wan87] and [Rém89, Rém90c], since one cannot translate into the language expressions like λx. x with a: = x.a + 1 . Using the join operation, however, it is possible to translate expressions like λx. x with a: = 3 into this language. [OB89] shows how to extend the system of [OB88] with subtyping of abstract types.

There exist a fair number of languages and type systems that embody some “objectoriented” features, including [CM91, CW85, CCH^{+} 89, FM89, FM90, HP91, Wan89], and these systems differ from one another in some non-trivial technical ways. Although such a comparison is useful, it is important to ask some broader questions. First, which of the different features is it feasible to merge together with the aim of developing a more powerful “object-oriented” language? Second, what further extensions should we aim to develop?

It seems to us that it is feasible to merge most of the approaches discussed above into one system with type inference. However, we feel that abstract data types capture an important property of object-oriented programming and should be incorporated into such typed languages. Other important features that should be considered are multiple inheritance, “self”, and “method specialization.”

9 Declarations

Although our current formal analysis only covers the fragment of ML^{+} without declarations, the reader may be interested in the larger design. This section sketches an extension to ML^{+} that supports abstract type declarations and subtyping between abstract types.

9.1 Declarations and Environments

Before considering type declarations, we give the typing rule and extension to the type inference algorithm for polymorphic let declarations. These expressions have the form let val P = M in N , where P is a pattern and M and N are expressions. To illustrate the main ideas, we begin with the simpler case of let-bound variables, then generalize to patterns.

Declarations can be explained relatively simply using macro-expansion. Consider an expression let val x = M in N . Provided that M is typable, this expression has the same types as [M/x]N , the result of substituting M for x in N . The reason for this is that in typing [M/x]N , each occurrence of M will be typed independently, generating the desired polymorphism. Now consider an expression let val P = M in N binding a pattern P to a value M . This should be typed in the same way as some substitution instance of N , provided we generalize “substitution” appropriately. Performing a substitution “ [M/P]N ” requires that M and P have a “similar form”, so that each variable and extension variable in P can be associated with the corresponding subexpression of M . Since P is a pattern, it can can be thought of as shorthand for applying destructors to M . Thus, the subexpression of M associated with a variable or extension variable w of P is simply the result of the function application P_{w}(M) , where P_{w} : : = fn P ⇒ w. If every such function application P_{w}(M) type-checks, we write [[M/P]]N for the result of replacing variables and extension variables from P that occur in N , with the corresponding function applications. Otherwise, [[M/P]]N is undefined. From a typing point of view, [[M/P]]N should be equivalent to the let expression above, since all occurrences of the expressions in M will be typed independently, achieving the desired polymorphism. Using substitution, we can describe let using the following typing rule.

let  \frac{C, A ⊃ M : τ and C^{op}, A′ ⊃ P : τ and C, A ⊃ [[M/P]]N : σ}{C, A ⊃ let val P = M in N end : σ}

It is easy to show that ⊢ C, A ⊃ M : τ and ⊢ C^{op}, A′ ⊃ P : τ together imply that C, A ⊃ P_{w}(M):A′(w) for every variable or extension variable w in P . Thus, [[M/P]]N is a well-defined substitution, and so this typing rule is “well-formed.”

The typing of expressions of the form let val rec P = M in N follows from the above rule, assuming a fixed-point combinator. Our typing rules can be extended to support recursive functions using let.

While macro-expansion of let provides the necessary polymorphism, substitution is not appropriate for a typing algorithm since the same expression may have to be typed many times. The equivalence of this and a more efficient approach is discussed in [Mit90b].

9.2 Informal Introduction to Abstype and Subtype Declarations

There are two ways that the type system and algorithm in this paper might be used. The first is that we might have some programming language with a set of built-in types and some subtype relationship between them. In this relatively simple situation, we may use the given subtype assertions about base types in any deduction of coercions, essentially treating each coercion set as if it contains these assertions. The second possibility is to use the type system and algorithm in a language where we can declare types and declare that one type is a subtype of another. To experiment with this kind of language, we have implemented a type checker for a language that allows declarations of abstract data types and subtypes of abstract data types. Since we have not carried out a full analysis of the resulting type system, we will only summarize aspects of this language here.

Table 5: Example ML^{+} abstract type and subtype.

abstype point = p of { x:int, y:int; NULL }
  with
     val new-point = fn (a, b) ⇒ p { x=a, y=b; EMPTY }
     val move1 = fn p { x=a, y=b; u } ⇒ p { x=a+1, y=b+1; u }
     val draw = fn . . . ⇒ . . .
  end;
subtype colored-point of point = s of { x:int, y:int, z:color;NULL }
  with
     val new-cp = fn (a, b, c) ⇒ s { x=a, y=b, z=c; EMPTY }
     val color= fn s { x=a, y=b, z=c;u } ⇒ c

…

  end

The abstract type and subtype declarations we consider are most easily explained by example. For simplicity, we use the common example of point and colored-point. Since the points of this example are meant to be drawn on a screen, each point has integer x and y coordinates. The operations on point include new-point, which creates a new point, and an operation to “move” points. A colored-point is similar to a point, except that each colored point has a specific color. Since a colored point is a particular kind of point, we will declare colored-point a subtype of point. The basic operations on points will be “inherited” by colored points, which means that they will have the same effect on elements of the subtype as if we had defined them to act on colored points in the first place.

The ML^{+} point and colored-point declarations are outlined in Table 5.

As in Standard ML, constructors are used in abstype declarations to designate “abstract” occurrences of the representation type. For point, the constructor is p. This means that p{x = a, y = b; EMPTY} is a value of type point, as opposed to a record. Constructors may be used in patterns, so that as a pattern, p{x = a, y = b; EMPTY} matches an element of the abstract type. Since elements of declared subtypes will be represented by records with additional fields, we allow the pattern p{x = a, y = b; u} to match any element of any subtype, binding u to any additional fields beyond x and

y.

The function new-point takes x, y -coordinates and returns a new point with these coordinates, while move1 “translates” a point diagonally, one unit in the x direction and one unit in the y direction. The most novel function in this example is move1, which uses extended pattern matching to bind u to any additional fields of the function argument besides x and y.

The subtype declaration is similar to an abstype declaration, except that a list of supertypes may be supplied. One of the typing constraints on subtypes is that the subtype values must be represented by records that contain all of the fields of all of the supertypes. Since the subtype declaration in Table 5 declares colored-point ⊆ point, the function move1 is automatically applicable to colored points. More importantly, extended pattern matching guarantees that the result of applying move1 to a colored point will be a point with the same color as the function argument. In fact, move1 maps values from any subtype of point to values belonging to the same subtype. Practically, this is very important. If we first implement a drawing program using point, and then buy a color display, we would like to use all of the original operations on colored-points without making the screen go black-and-white.

The typing algorithm automatically infers types for the functions given in each declaration. Although the types we actually use are somewhat more general, the behavior of our algorithm on this example may be explained using the bounded quantification notation of [CW85]. In this notation, the types inferred for the two declarations are at least as general as the following types.

    new-point:  int × int → point
    move1: ∀t ⊆ point. t → t
    new-cp:  int × int × color → colored-point
    color: ∀t ⊆ colored-point. t → color

It is especially important to notice that the type of move1 reflects its true functionality. The bounded quantified type gives move1 the type t → t for all subtypes of point, including colored-point. Without extended pattern matching and bounded quantification, the type of move1 would be point → point . This would still allow move1 to be applied to any colored point, since colored-point ⊆ point. However, since the value returned would have type point, we could no longer apply the function color to determine color.

9.3 Type Inference, Subtyping, and Abstract types

An abstract type declaration consists of a type name, representation, value constructor, and set of operations. In ML^{+} , the representation must be a fixed record type. The value constructor is a function that takes any record that is a subtype of the representation and “packages” that record to be a corresponding subtype of the abstract type. To simplify the presentation, we do not consider nested abstype and subtype declarations.

An abstract type has different forms outside its type declaration and inside its type declaration. Outside of its declaration, an abstract type is simply an atomic type denoted by the name of the abstract type; the representation of the abstract type is hidden. On the other hand, within its type declaration, the representation is exposed, and the abstract type is associated with its name, representation, and value constructor.

Similarly, the form of subtyping relations involving abstract types differs inside and outside the declaration. Consider an abstract type and a subtype of that abstract type. The subtype has “extra” fields not possessed by its parent type. Within the type declaration of the abstract type, these fields are “exposed,” in the sense that we may name them by an extension variable. Outside of the type declaration, extra fields are hidden.

The main idea behind our typing algorithm for abstype and subtype is that in typing a function declaration within a type declaration, we keep track of the form of each type that arises. However, when the type checker returns a type for the function, any type that is an extension of the abstract type being declared is given a new name, and a subtype constraint forcing this to be a subtype of the abstract type is generated. This may be illustrated using the function move1. Instead of writing point for the type p {x : int, y : int; NULL}, we will use this as an a type expression, and also consider any type of the form p {x : int, y : int; X_{L}} a well-formed type expression, provided L includes x and y . With this form of type expression, which does not complicate the type inference algorithm since we just treat the form p {…} in the same way as the usual record type expression form {…}, the type our algorithm infers for

         val move1 = fn p{x = a, y = b; u} ⇒ p{x = a + 1, y = b + 1; u}

is

            move1 : p{x : int, y : int; X_{L}} → p{x : int, y : int; X_{L}}

Since any declared subtype of point must have a representation type that has the form p′ {x : int, y : int; Z}, for some constructor p′ and additional fields Z, we can see that move1 maps any subtype of point that we can possibly declare to itself. Therefore, it is sound to return the typing

                        t ⊆ point, ∅ ⊃ move1 : t → t

for move1 . Within the scope of the declaration of point , the identifier move1 is treated exactly as if it were a built-in constant of the language with the typing given above. This typing is equivalent to the bounded quantified type, ∀t ⊆ point. t → t, mentioned earlier, since our axiom for typing a term constant allows any type expression to be substituted for any type variable. Thus the type variable t in the typing of point above is implicitly universally quantified, and bounded by the hypothesis t ⊆ point .

Although the syntax we have used suggests that the representation of point, or any other abstract type, must be a fixed record, there is another way of understanding the representation type. Since we allow any subtype of point with representation of the form {x: int, y: int; Z} to be declared, the true set of values that may have type point is the union of all such subtypes. Another way of putting this is that the elements of point are represented by elements of the “existential type” ∃X_{L}. {x : int, y : int; X_{L}} with an existentially quantified row variable. This suggests that abstract types with subtypes can be related to the standard view of abstract types as existential types [MP88].

10 Conclusion

We have given a set of typing rules and a type inference algorithm that form an extension of a core fragment of ML with a more powerful form of pattern matching on records, and a simple subtyping mechanism. For expressions without declarations, we have given an algorithm that finds most general types. To a first approximation, the algorithm for typing core expressions of ML^{+} is the natural combination of the algorithms presented in [Mit84, Mit91] and [Wan87], with pattern matching substituted for Wand’s with construct.

Our main reason for combining extended pattern matching and subtypes is that with subtype declarations, we can infer bounded quantified types for functions. If we declare a function g with type

{a: int; X_{a}} → {a: int; X_{a}}

as an operation on abstract type t with values represented by records with a : int , we may infer that g has type s → s for every subtype s ⊆ t. The soundness of this inference is based on the language design decision that every subtype of t will be represented by records with types that are instantiations of {a : int; X_{a}}. The bounded quantified type of g is important, since it guarantees that when g is applied to elements of some subtype s, the effect is the same as if g had been declared as part of s to begin with. Although our current algorithm for typing abstype and subtype declarations seems to work well for the examples we have tried, our current justification for this algorithm seems ad hoc. We hope to extend our formal analysis of ML^{+} typing to declarations in the future.

One direction for future research is to extend the abstype/subtype mechanism of ML^{+} to include some form of “method specialization,” as explained in [Coo87, Mit90a]. Another open problem is to develop a semantic model of ML^{+} as it stands. While [BL90] presents a compelling model for the language of [CW85] with bounded quantification, the treatment of bounded quantifiers is too restrictive to justify the typing rules of ML^{+} . In particular, move1 of Section 9.3 does not have type ∀t ⊆ point. t → t in the semantics of [BL90], since their model contains “too many” subtypes of point. While the appropriate repair is unclear, an appropriate guide here may be [Rey80].

Acknowledgments: We would like to thank Val Breazu-Tannen, Kim Bruce, Luca Cardelli, Albert Meyer, Benjamin Pierce, Didier Rémy, Jon Riecke, Jurek Tiuryn, and Mitch Wand for many useful discussions. We also thank an anonymous referee for many helpful suggestions.

The first author would like to acknowledge the support of an AT&T GRPW Fellowship, NSF grant CCR-8819761, and ONR grant N00014-89-J-1988. The second author would like to acknowledge the support of an NSF PYI Award, matching funds from Digital Equipment Corporation, the Powell Foundation, and Xerox Corporation; NSF grant CCR-8814921 and the Wallace F. and Lucille M. Davis Faculty Scholarship.

A Appendix A

This section defines our algorithm unify in detail and gives the proof of correctness. The behavior of the algorithm on equations involving only type variables, base types, function types, and fixed record types is almost identical to the standard unification algorithm [Rob65]. Essentially, the idea is to recursively decompose equations between compound types of the same “shape,” substituting types for type variables when necessary. Since we do not have recursive types, an equation like t = t → t will never have a solution; thus, prior to replacing a type variable by the type with which it is supposed to unify, the algorithm checks that a type variable does not occur in the type. Finally, the algorithm “fails” if it is asked to unify two distinct base types or two compound types with different “shapes.”

On equations involving flexible record types, the algorithm performs substitutions on row variables, and is very similar to that of [Wan87]. There are three cases that arise, corresponding to equations between fixed types and flexible types, equations between flexible types with the same row variable, and equations between flexible types with distinct row variables. Equations between flexible record types with the same row variable are treated essentially the same as equations between fixed record types. The behavior of the algorithm on an equation between a fixed record type and a flexible record type is slightly more complicated. If we hope to make the records syntactically identical, clearly the fixed record type must already contain all the labels of the flexible record type. Furthermore, the “extra” fields of the fixed record must be substituted for the row variable of the flexible record. Of course, since we want to respect our definition of substitution, we must check that this “row” of fields does not “conflict” with the label set of the row variable that it will replace. Furthermore, in order to prevent recursive type equations, the row variable must not occur anywhere in this “row” of fields. If all of these conditions hold, the algorithm performs the substitution, and then decomposes the corresponding fields of the resulting records.

Equations involving flexible types with distinct row variables are somewhat more complicated. The idea here is that in order to make the records syntactically identical, the “extra” fields of each record must be substituted for the row variable of the other record. Again, since we want to respect our definition of substitution, we must check that each of these “rows” of fields does not “conflict” with the label set of the row variable that it will replace. Furthermore, since we want the most general solution, we attach the same new row variable to each of these “rows” of fields; again, the label set of this new row variable must respect the label sets of the original row variables. For the reasons explained in Section 5, this new row variable is chosen so that it is not in the set Q ∪ Q_{E}. Due to technical reasons which we will not explain in detail here, the “occurs” checks for this step are more complicated. The final substitution that we perform at this step is also more complicated: it is actually an double application of the substitution mentioned above. The technical reasons behind this more complicated substitution are given in the proof of Lemma 5.1.

In contrast with Robinson’s and Wand’s algorithms, our algorithm explicitly passes around the set Q and at each step, adds to it all the type and row variables in E that may disappear after that step. Although this may make the pseudo-code in Table 6 slightly harder to read, we need to include this in our algorithm for the reasons mentioned in Section 5.

unify uses subsidiary algorithms for creating types, creating substitutions, applying substitutions and composing substitutions. All of these are assumed to fail when the operation is not defined, and we assume that the entire algorithm will terminate in error. For example, if a type is not well-formed, or a substitution is not well-defined, then the entire algorithm will fail. In the definition of unify, we use the notation h ◁ L, where h is a function from labels to types and L is a set of labels, to denote the restriction of h to the domain dom(h) ∩ L. unify is defined in Table 6.

Before proceeding to prove the correctness of unify, we first develop some technical properties of unification that we will need in that proof. The first such property concerns unifying a type variable with a type.

Lemma A.1 A substitution T unifies E′ ∪ {t = τ} iff t = τ and T unifies E′, or the following conditions hold:

1. t ≠ τ

2. t does not occur in τ

3. there exists a substitution T′ such that T = T′ ∘ [τ/t] and T′ unifies [τ/t]E′.

We omit the proof, as it is quite similar to [Rob65].

We also need the following property about unifying an extended record with a fixed record.

Table 6: Mutually recursive clauses for unify

unify(∅, Q) = ∅

unify(E′ ∪ {b_{1} = b_{2}}, Q) =

if b_{1} ≠ b_{2} then fail else unify(E′, Q)

unify(E′ ∪ {σ_{1} → σ_{2} = τ_{1} → τ_{2}}, Q) = unify(E′ ∪ {σ_{1} = τ_{1}, σ_{2} = τ_{2}}, Q)

unify(E′ ∪ {t = τ}, Q) =

if t = τ then unify(E′, Q ∪ {t})

else if t occurs in τ then fail

else let Q′ = Q ∪ {t} ∪ {the type and row variables occurring in τ} in unify([τ/t]E′, Q′) ∘ [τ/t]

unify(E′ ∪ {{h; null} = {h′; null}}, Q) =

if dom(h) ≠ dom(h′) then fail else unify(E′ ∪ ⋃_{l∈dom(h)}{h(l) = h′(l)}, Q)

unify(E′ ∪ {{h; X_{L}} = {h′; X_{L}}}, Q) =

if dom(h) ≠ dom(h′) then fail else unify(E′ ∪ ⋃_{l∈dom(h)}{h(l) = h′(l)}, Q ∪ {X_{L}})

unify(E′ ∪ {{h; X_{L}} = {h′; null}}, Q) =

if dom(h) ⊈ dom(h′) then fail

else let h_{1} = h′ ◁ (dom(h′) − dom(h))

in if dom(h_{1}) ∩ L ≠ ∅ or X_{L} occurs in {h_{1}; null} then fail

else let Q′ = Q ∪ {X_{L}} ∪ {the type and row variables occurring in h_{1}} in unify([{h_{1}; null}/X_{L}](E′ ∪ ⋃_{l∈dom(h)}{h(l) = h′(l)}), Q′) ∘ [{h_{1}; null}/X_{L}]

unify(E′ ∪ {{h; X_{L}} = {h′; X′_{L′}}}, Q) = (where X_{L} ≠ X′_{L′} )

let h_{1} = h′ ◁ (dom(h′) − dom(h))

h_{2} = h ◁ (dom(h) − dom(h′))

Q_{E} = the type and row variables occurring in E′ ∪ {{h; X_{L}} = {h′; X′_{L′}}}
Y_{L∪L′} be a row variable not in Q ∪ Q_{E}
in if X_{L} occurs in {h_{1}; Y_{L∪L′}} or X′_{L′} occurs in {h_{2}; Y_{L∪L′}}

OR if X_{L} occurs in {h_{2}; Y_{L∪L′}} and X′_{L′} occurs in {h_{1}; Y_{L∪L′}}

OR if dom(h_{1}) ∩ L ≠ ∅ or dom(h_{2}) ∩ L′ ≠ ∅ then fail else let V = [{h_{1}; Y_{L∪L′}}/X_{L}, {h_{2}; Y_{L∪L′}}/X′_{L′}] ∘ [{h_{1}; Y_{L∪L′}}/X_{L}, {h_{2}; Y_{L∪L′}}/X′_{L′}]

Q′ = Q ∪ {X_{L}, X′_{L′}, Y_{L∪L′}} ∪ {the type and row variables occurring in h_{1} or h_{2}}

in unify(V (E′ ∪ ⋃_{l∈dom(h)∩dom(h′)}{h(l) = h′(l)}), Q′) ∘ V

unify(E′ ∪ {σ = τ}, Q) =

if σ = τ is an equation between any other types then fail

Lemma A.2 A substitution T unifies E′ ∪ {{h; X_{L}} = {h′; null}} iff

1. dom(h) ⊆ dom(h′)

2. dom(h_{1}) ∩ L = ∅, where h_{1} = h′ ◁ (dom(h′) − dom(h))

3. X_{L} does not occur in {h_{1}; null}

4. there exists a substitution T′ such that T = T′ ∘ [{h_{1}; null}/X_{L}] and T′ unifies [{h_{1}; null}/X_{L}](E′ ∪ ⋃_{l∈dom(h)}{h(l) = h′(l)}) .

Again, we omit the proof, as it uses the same sort of reasoning as the proof of the Lemma A.1.

The final property that we will need concerns unifying two extended records.

Lemma A.3 A substitution T unifies E′ ∪ {{h; X_{L}} = {h′; X′_{L′}}} iff

1. X_{L} does not occur in h_{1} , where h_{1} = h′ ◁ (dom(h′) − dom(h))

2. X′_{L′} does not occur in h_{2} , where h_{2} = h ◁ (dom(h) − dom(h′))

3. either X_{L} does not occur in h_{2} or X′_{L′} does not occur in h_{1}

4. dom(h_{1}) ∩ L = ∅ and dom(h_{2}) ∩ L′ = ∅

5. for any finite set Q of type and row variables, and for any row variable Y_{L∪L′} that is not in Q ∪ Q_{E}, where Q_{E} is the set of type and row variables occurring in E′ ∪ {{h; X_{L}} = {h′; X′_{L′}}}, there exists a substitution T′ such that T =_{Q∪Q_{E}} T′ ∘ V and T′ unifies V (E′ ∪ ⋃_{l∈dom(h)∩dom(h′)}{h(l) = h′(l)}) , where V = [{h_{1}; Y_{L∪L′}}/X_{L}, {h_{2}; Y_{L∪L′}}/X′_{L′}] ∘ [{h_{1}; Y_{L∪L′}}/X_{L}, {h_{2}; Y_{L∪L′}}/X′_{L′}] .

The proof is tedious but straightforward, and thus omitted.

Using the lemmas above, we now give the proof of Lemma 5.1. Proof In order to prove the Lemma 5.1, it is sufficient to show the following three properties of unify:

1. unify(E, Q) halts.

2. If there is a substitution T that unifies E, then unify(E, Q) succeeds and produces a substitution S such that S unifies E. Furthermore, there exists a substitution U such that T =_{Q∪Q_{E}} U ∘ S.

3. If no substitution unifies E, then unify(E, Q) fails.

In order to prove (1), we define the degree of a set E to be the pair ⟨m, n⟩, where m is the number of distinct type variables and row variables that occur in E, and n is the number of occurrences of → and {}, plus the total number of occurrences of (possibly non-distinct) type variables, row variables, base types, and null that occur in E. (Before applying this definition, we write all record types {h; Z}, where h is non-empty, as {l_{1} : h(l_{1}), …, l_{k} : h(l_{k}); Z}, where dom(h) = {l_{1}, …, l_{n}}.) We say that ⟨m, n⟩ is smaller than ⟨m′, n′⟩ if either m < m′, or m = m′ and n < n′. We will show that each clause of the algorithm reduces the degree of the set E that is passed around. We note here that a set E has degree ⟨0, 0⟩ iff E is empty.

The proof proceeds by induction on the degree of E and case analysis on the structure of σ = τ , where E = E′ ∪ {σ = τ}. In the proof, we let ⟨m, n⟩ be the degree of E. We give the proof for two cases; the remaining cases are left to the reader.

For one case, suppose that σ = τ is of the form {h; X_{L}} = {h′; null}. To prove (1), we observe that if unify succeeds, then the first component of the degree of [{h_{1}; null}/X_{L}](E′ ∪ ⋃_{l∈dom(h)}{h(l) = h′(l)}) is at most m − 1 . To prove (2) and (3), we first note that Q_{E} = Q_{[{h_{1};null}/X_{L}](E′∪⋃_{l∈dom(h)}{h(l)=h′(l)})} ∪ {X_{L}} ∪ {the type and row variables occurring in h_{1}}. Using these properties and Lemma A.2, the proofs of (2) and (3) follow from the inductive hypothesis.

For another case, suppose that σ = τ is of the form {h; X_{L}} = {h′; X′_{L′}}. To prove (1), we observe that if unify succeeds, then Y_{L∪L′} may occur in V (E′ ∪ ⋃_{l∈dom(h)∩dom(h′)}{h(l) = h′(l)}) , but neither X_{L} nor X′_{L′} will occur. Thus, the first component of the degree of V (E′ ∪ ⋃_{l∈dom(h)∩dom(h′)}{h(l) = h′(l)}) is at most m − 1 . To prove (2) and (3), we first note that Q_{E} ⊆ Q_{V (E′∪⋃_{l∈dom(h)∩dom(h′)}{h(l)=h′(l)})} ∪ {the type and row variables occurring in h_{1} or h_{2}}∪{X_{L}, X′_{L′}}. Using these properties and Lemma A.3, the proofs of (2) and (3) follow from the inductive hypothesis, proving the lemma.

As mentioned earlier in this section, our algorithm unify corrects a bug in the unification algorithm of [Wan87]. To unify types of the form {h; X_{L}} and {h′; X′_{L′}}, where X_{L} ≠ X′_{L}, Wand’s algorithm uses the substitution

[{h_{1}; Y_{L∪L′}}/X_{L}, {h_{2}; Y_{L∪L′}}/X′_{L′}]

instead of the substitution

[{h_{1}; Y_{L∪L′}}/X_{L}, {h_{2}; Y_{L∪L′}}/X′_{L′}] ∘ [{h_{1}; Y_{L∪L′}}/X_{L}, {h_{2}; Y_{L∪L′}}/X′_{L′}]

which we call V . However, applying the simpler substitution used by Wand to the set (E′ ∪ ⋃_{l∈dom(h)∩dom(h′)}{h(l) = h′(l)}) does not necessarily decrease the halting measure, since two out of three of X_{L}, X′_{L′} , Y_{L∪L′} may occur in the resulting set of equations. We correct this difficulty by using substitution V .

B Appendix B

As mentioned in Section 6, the problem of finding a most general matching substitution for a set C of possibly non-matching subtype assertions can be reduced to the problem of finding a most general unifying substitution for a set E that is closely related to C. The main idea is that we treat the set C as a set of equations (rather than inequalities) between types, replace all base types in C by a special type variable, unify the resulting set of equations, and check that the most general unifier “merely renames” this special type variable. Furthermore, since we want to ensure only that the resulting subtype assertions are between types that have the same “shape,” we replace all occurrences of type variables and row variables in the resulting types by distinct type and row variables that do not appear in an associated set Q. More precisely, we extract a substitution that chooses variables freely on Q in the following sense:

Definition B.1 A substitution S chooses variables freely on a set Q of type variables and row variables if, for all t ∈ Q and X_{L} ∈ Q, no type variable or row variable in Q occurs in St or S{∅; X_{L}}, and

Table 7: The Algorithm match

match( C, Q)=

let Q_{C} be the set of type variables and row variables that occur in C t_{base} be a type variable not in Q ∪ Q_{C} C′ be the set C with all occurrences of int, real, bool, and string replaced with t_{base} E = {σ′ = τ′ | σ′ ⊆ τ′ ∈ C′} S = unify(E, Q ∪ Q_{C} ∪ {t_{base}})

if St_{base} is not a type variable

then fail

else compute substitutions S_{1} and S_{2} such that S_{1} chooses variables freely on Q ∪ Q_{C} ∪ {t_{base}}, S_{2} is simple,

and S =_{Q∪Q_{C}∪{t_{base}}} S_{2} ∘ S_{1}

return S_{1}

• For each t ∈ Q, no type variable or row variable occurs more than once in St.

• For each X_{L} ∈ Q, no type variable or row variable occurs more than once in S{∅; X_{L}}.

• For any distinct s, t ∈ Q, no type variable or row variable in Ss occurs in St.

• For any finite sets L and L′ and for any distinct X_{L}, Y_{L′} ∈ Q, no type variable or row variable in S{∅; X_{L}} occurs in S{∅; Y_{L′}}.

• For any t, X_{L} ∈ Q, no type variable or row variable in St occurs in S{∅; X_{L}}.

In the procedure for computing most general matching substitutions outlined above, we “factor” a most general unifying substitution into a “most general” substitution that chooses variables freely on some set Q composed with a “simple” substitution that “merely renames type and row variables.” Formally, we say that a substitution S is simple if, for all s ∈ dom(S) , there exists a type variable t such that S(s) = t, and for all X_{L} ∈ dom(S) , there exists a row variable Y_{L′} with L′ = L such that S(X_{L}) = {∅; Y_{L′}}.

The following lemma shows that such “most general factorizations” do indeed exist, and are computable.

Lemma B.2 Let Q be a finite set of type variables and row variables, and let S be a substitution. There are substitutions S_{1} and S_{2} such that S_{1} and S_{2} are computable, S_{1} chooses variables freely on Q, S_{2} is simple, and S =_{Q} S_{2} ∘ S_{1} . Furthermore, if S =_{Q} T_{2} ∘ T_{1} for some substitution T_{1} and some simple substitution T_{2} , then there exists a simple substitution W such that T_{1} =_{Q} W ∘ S_{1} .

The proof is similar to that of [Mit91] and is omitted here.

Our algorithm match uses the algorithm implicit in Lemma B.2 to “factor” substitutions, and also uses subsidiary algorithms for applying substitutions and composing substitutions. match is defined in Table 7.

In our proof of correctness for match, we will need to use the fact that choosing variables freely is preserved under composition of appropriately defined substitutions.

Lemma B.3 Let S be a substitution that chooses variables freely on a set Q of type variables and row variables, and let Q′ be the set of all type variables and row variables occurring in St or in S{∅; X_{L}}, for any t, X_{L} ∈ Q. If T is a substitution that chooses variables freely on Q ∪ Q′, then T ∘ S chooses variables freely on Q.

The proof is straightforward and we omit it.

We now give the proof of Lemma 6.1. Proof For one direction, suppose that there is a matching substitution T for C. We wish to construct from T a unifying substitution for E. To this end, let s_{int}, s_{real}, s_{bool}, and s_{string} be type variables not in Q_{C} ∪ {t_{base}}, and T_{1} be the substitution with domain Q_{C} that maps all type variables t in its domain to T t with all occurrences of int replaced with s_{int} (and similarly for the other base types). The action of T_{1} on row variables in its domain is defined analogously. It is easy to see that T_{1} is a matching substitution for C. Thus, by the construction of T_{1} and C′, it follows that for all σ′ ⊆ τ′ ∈ C′, T_{1}σ′ and T_{1}τ′ differ only in the names of type variables and in the names of row variables with identical label sets. Let Q′ be the set of all type and row variables that occur in T_{1}(t) or T_{1}(X_{L}) for t, X_{L} ∈ dom(T_{1}) . Let T_{2} be the substitution whose domain is Q_{C} ∪ {t_{base}} ∪ Q′ and that maps all type variables in its domain to some fixed type variable t′. Furthermore, let T_{2} map all row variables with label set L in its domain to the record {∅; Y_{L}} for some fixed Y_{L}. It is easy to see that T_{2} is simple, and T_{2} ∘ T_{1} unifies E.

By Lemma 5.1, we can conclude that unify(E, Q∪Q_{C} ∪{t_{base}}) succeeds, and that there exists a substitution U such that U ∘S =_{Q∪Q_{C}∪{t_{base}}} T_{2} ∘T_{1} . Furthermore, since t_{base} ∉ dom(T_{1}) and T_{2} is simple, it follows that T_{2} ∘ T_{1} maps t_{base} to a type variable; thus, this property must also hold true for S. By Lemma B.2, it follows that S_{1} and S_{2} exist and are computable; thus, match(C, Q) succeeds. Furthermore, it is easy to see that the fact that S_{2} is simple implies that S_{1} is a matching substitution for C. By repeated applications of Lemma B.2 together with an application of Lemma B.3, it is straightforward to show show that there is a substitution W such that T =_{Q∪Q_{C}} W ∘S_{1} , proving one direction of the lemma.

For the other direction, suppose that there is no matching substitution for C and suppose for the sake of contradiction that match(C, Q) succeeds. Then by the argument used above, it is easy to show that S_{1} is a matching substitution for C, a contradiction. Thus, match(C, Q) must fail after all, proving the lemma.

References

[BL90] K. Bruce and G. Longo. A modest model of records, inheritance and bounded quantification. Information and Computation, 87(1/2):196–240, 1990.

[BTCGS90] V. Breazu-Tannen, T. Coquand, C.A. Gunter, and A. Scedrov. Computing with coercions. In Proc. ACM Conference on Lisp and Functional Programming, pages 44–61, 1990.

[BTCGS91] V. Breazu-Tannen, T. Coquand, C.A. Gunter, and A. Scedrov. Inheritance as explicit coercion. Information and Computation, 93(1):172–221, 1991.

[Car84] L. Cardelli. A semantics of multiple inheritance. In Proc. Int. Symp. on Semantics of Data Types, Sophia-Antipolis (France), pages 51–68, Berlin, June 1984. Springer LNCS 173.

[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.

[CCH^{+} 89] P. Canning, W. Cook, W. Hill, J. Mitchell, and W. Olthoff. F-bounded quantification for object-oriented programming. In Functional Prog. and Computer Architecture, pages 273–280, 1989.

[CHC90] W. Cook, W. Hill, and P. Canning. Inheritance is not subtyping. In Proc. 17th ACM Symp. on Principles of Programming Languages, pages 125–135, January 1990.

[CM91] L. Cardelli and J.C. Mitchell. Operations on records. Math. Structures in Computer Science, 1(1):3–48, 1991. Summary in Math. Foundations of Prog. Lang. Semantics, Springer LNCS 442, 1990, pp 22–52.

[Coo87] W. Cook. A self-ish model of inheritance. Manuscript, 1987.

[Coo89] W.R. Cook. A Denotational Semantics of Inheritance. PhD thesis, Brown University, 1989.

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

[DM82] L. Damas and R. Milner. Principal type schemes for functional programs. In Proc. 9th ACM Symposium on Principles of Programming Languages, pages 207–212, 1982.

[FM89] Y. Fuh and P. Mishra. Polymorphic subtype inference: closing the theory-practice gap. In Proc. Theory and Practice of Software Development, pages 167–184, March 1989.

[FM90] Y. Fuh and P. Mishra. Type inference with subtypes. Theor. Computer Science, 73, 1990.

[GR83] A. Goldberg and D. Robson. Smalltalk–80: The language and its implementation. Addison Wesley, 1983.

[HP91] Robert Harper and Benjamin Pierce. A record calculus based on symmetric concatenation. In Proc. 18th ACM Symp. Principles of Programming Languages, pages 131–142, January 1991. Extended version available as Carnegie Mellon Technical Report CMU-CS-90-157.

[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.

[Kam88] S. Kamin. Inheritance in smalltalk-80: a denotational definition. In ACM Symp. Principles of Programming Languages, pages 80–87, 1988.

[KMM91] P.C. Kanellakis, H.G. Mairson, and J.C. Mitchell. Unification and ML type reconstruction. In Computational Logic, Essays in Honor of Alan Robinson, pages 444–478. MIT Press, 1991.

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

[Mil85] R. Milner. The Standard ML core language. Polymorphism, 2(2), 1985. 28 pages. An earlier version appeared in Proc. 1984 ACM Symp. on Lisp and Functional Programming.

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

[Mit90a] J.C. Mitchell. Toward a typed foundation for method specialization and inheritance. In Proc. 17th ACM Symp. on Principles of Programming Languages, pages 109–124, January 1990.

[Mit90b] J.C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B, pages 365–458. North-Holland, Amsterdam, 1990.

[Mit91] J.C. Mitchell. Type inference with simple subtypes. J. Functional Programming, 1(3):245–286, 1991.

[MP88] J.C. Mitchell and G.D. Plotkin. Abstract types have existential types. ACM Trans. on Programming Languages and Systems, 10(3):470–502, 1988. Preliminary version appeared in Proc. 12th ACM Symp. on Principles of Programming Languages, 1985.

[MTH90] Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, 1990.

[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.

[OB89] A. Ohori and P. Buneman. Static type inference for parametric classes. In Proc. ACM Conference on Object-Oriented Programming Systems, Languages, and Applications, pages 445–456, October 1989.

[Pie92] B. Pierce. Bounded quantification is undecidable. In Proc. 19th ACM Symp. Principles of Programming Languages, pages 305–315, 1992. Available as Carnegie Mellon Technical Report CMU-CS-91-161.

[Red88] U.S. Reddy. Objects as closures: Abstract semantics of object-oriented languages. In Proc. ACM Symp. Lisp and Functional Programming Languages, pages 289–297, July 1988.

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

[Rém90a] Didier Rémy. Algèbres Touffues, Application au Typage Polymorphe des Objects Enregistrements dans les Langages Fonctionnels. Thèse de doctorat, Université de Paris 7, France, 1990.

[Rém90b] Didier Rémy. Extending ML type system with a sorted equational theory. Technical report, University of Pensylvania, 1990. Also in [Rem90a], chapter 3.

[Rém90c] Didier Rémy. Typechecking records in a natural extension of ML. Technical report, University of Pensylvania, 1990. Also in [Rem90a], chapter 4.

[Rém90d] Didier Rémy. Unification in syntactic theories and its application to the record extension of a free sorted algebra. Technical report, University of Pensylvania, 1990. Also in [Rem90a], chapter 2.

[Rey80] J.C. Reynolds. Using category theory to design implicit conversions and generic operators. In N.D. Jones, editor, Semantics-Directed Compiler Generation, pages 211–2580. Springer LNCS 94, Berlin, 1980.

[Rob65] J.A. Robinson. A machine oriented logic based on the resolution principle. JACM, 12(1):23–41, 1965.

[Sta88] R. Stansifer. Type inference with subtypes. In Proc. 15th ACM Symp. on Principles of Programming Languages, pages 88–97, January 1988.

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

[Wan88] M. Wand. Corrigendum: Complete type inference for simple objects. Proc. IEEE Symp. on Logic in Computer Science, 1988.

[Wan89] M. Wand. Type inference for record concatenation and multiple inheritance. In Proc. IEEE Symp. on Logic in Computer Science, pages 92–97, 1989. To appear in Information and Computation.

[WF92] A.K. Wright and M. Felleisen. A syntactic approach to type soundness. Technical Report TR91-160, Rice University, 1992.

[WO89] M. Wand and P. O’Keefe. On the complexity of type inference with coercion. In Proc. ACM Conf. Functional Programming and Computer Architecture, pages 293–298, 1989.