Objective ML: An effective object-oriented extension to ML

Didier R� emy and J� er � ome Vouillon Authors’ address: INRIA-Rocquencourt, B.P. 105, F-78153 Le Chesnay Cedex, France. Email: Didier.Remy,Jerome.Vouillon@inria.fr

Objective ML is a small practical extension to ML with objects and top level classes. It is fully compatible with ML; its type system is based on ML polymorphism, record types with polymorphic access, and a better treatment of type abbreviations. Objective ML allows for most features of object-oriented languages including multiple inheritance, methods returning self and binary methods as well as parametric classes. This demonstrates that objects can be added to strongly typed languages based on ML polymorphism.\begin{matrix}c \\ ◯ \end{matrix} 1997 John Wiley & Sons

Introduction

We propose a simple extension to ML with class-based objects. Objective ML is a fully conservative extension to ML. A beginner may ignore the object extension. Moreover, he would not notice any difference, even in the types inferred. This is possible since the type inference algorithm of Objective ML, as in ML, is based on �rst-order uni�cation and let-binding polymorphism. Types are extended with object types that are similar to record types for polymorphic access. Both the status and the treatment of type abbreviations have been improved in order to keep types readable.

When using object-oriented features, the user is never required to write interfaces of classes, although he might have to include a few type annotations when de�ning parametric classes or coercing objects to their counterparts in super classes.

Objective ML is a class-based system that provides most features of object-oriented programming. This includes methods returning self and binary methods, of course, but also abstract classes and multiple inheritance. Coercion from objects to their counterparts in super classes is also possible. However, they must be explicit.

The ingredients used, except automatic abbreviations, are not new. However, their incorporation into a practical language, combining power, simplicity and compatibility with ML, is new.

Objective ML is formally de�ned, and its dynamic semantics is proven correct with respect to the static semantics. The language has not been designed to be a minimal calculus of objects, but rather the core of a real programming language. In particular, the semantics of classes is compatible with programming in imperative style as well as in functional style and it allows for ef�cient memory management (methods can be shared between all the instances of a class).

This paper is organized as follows: the �rst section is an overview of Objective ML. Objects and classes are introduced in sections 2 and 3. Coercions are dealt with in section 4. The semantics of the language is described in section 5. Type inference is discussed in section 6. The abbreviation mechanism is explained in sections 7 and 8. Extensions to the core language are presented in sections 9 and 10. In section 11, we compare our proposal with other work.

1. An overview of Objective ML

Objective ML is a core langage. An extended language based on Objective ML has been implemented on top of the Caml Special Light system [19]. This implementation is called Objective Caml. In this article, we completely formalize the core language, i.e. Objective ML. We also use the name Objective Caml to refer to the implementation, especially when describing minor differences or extension to the core language that have not been fully formalized. All examples show below have been process by Objective Caml^{1}. When useful, we display the output of the typechecker in a slanted font. Toplevel de�nitions are implicit let .. in ... For each phrase, the typechecker outputs the binding that will be generalized and added to the global environment before starting to typecheck the next phrase.

The language Objective ML is class-based. That is, objects are usually created from classes, even though it is also possible to create them directly (this is described in the next section). Here is a straightforward example of a class point.

class point x0 = struct
  field x = ref x0

\begin{matrix}c \\ ◯ \end{matrix} (1998) John Wiley & Sons, Inc.

THEORY AND PRACTICE OF OBJECT SYSTEMS, Vol. (Volume Number)((Optional Issue Number)), 1 24 (1998) CCC(cccline information)

  method move d = (x := !x + d; !x)
end;;
class point : int → sig
  field x : int ref
  method move : int → int
end

Class types are automatically inferred. Objects are usually created as instances of classes. All objects of the same class have the same type structure, re�ecting the structure of the class. It is important to name object types to avoid repeating the whole nested, often recursive, structure of objects at each occurrence of an object type. Thus, the above declaration also automatically de�nes the abbreviation:

type point = ⟨move : int → int⟩

which is the type of objects with a method move of type int → int. In practice, this is essential in order to report readable types to the user. The following example shows that these object abbreviations are introduced when the operator new is applied to a class.

new point;;
− : int → point = ⟨fun⟩
let p = new point 3;;
value p : point = ⟨obj⟩

Classes can also be derived from other classes by adding �elds and methods. The following example shows how an object sends messages to itself; for instance, if the scale formula is overridden in a subclass, the move method will use the new scale. Here, methods of the parent class are bound by the super-class variable parent and are used in the rede�nition of the move method (the binary operator # denotes method invocation in Objective ML).

class scaled point s0 = struct
  inherit point 0 as parent
  field  s = s0
  method scale = s
  method move d =
    parent#move (d * self#scale)
end;;
class scaled point : int → sig
  field s : int
  field x : int ref
  method move : int → int
  method scale : int
end

Scaled points have a richer interface than points. It is still possible to consider scaled points as points. This might be useful if one wants to mix different kinds of points with incompatible attributes, ignoring anything but the interface of points:

let points =
 [(new scaled point 2 : scaled point ⟨: point);
   new point 1];;

                                                 value points : point list = [⟨obj⟩; ⟨obj⟩]

A few other examples are given in the paper, and an example using binary methods can be found in the appendix 3.

Notation

A binding is a pair (k, t) of a key k and an element t. It is written k = t when t is a term or k : t when t is a type. Bindings may also be tagged. For instance, if foo is a tag, we write foo u = a or foo u : a. Tags are always redundant in bindings and are only used to remind what kind of identi�er is bound.

Term sequences may contain several bindings of the same key. We write @ for the concatenation of sequences (i.e. their juxtaposition). On the contrary, linear sequences cannot bind the same key several times. We write + for the overriding extension of a sequence with another one, and ⊕ to enforce that the two sequences must be compatible (i.e. they must agree on the intersection of their domains). We write ∅ for the empty sequence.

A sequence can be used as a function. More precisely, the domain of a sequence S is the union, written dom (S), of the �rst projection of the elements of the sequence. An element of the domain k is mapped to the value t so that x : t is the rightmost element of the sequence whose �rst projection is x, ignoring the tags. The sequence S \ foo is composed of all elements of S but those tagged with foo. Finally, we write foo (S) for {k : t | foo k : t ∈ S}, that is, for the subsequence of the elements of S tagged with foo but stripped of the tag foo.

We write t̄ for a tuple of elements (t_{i}^{i∈I}) when indexes are implicit from the context.

2. Objects

We assume that a set of variables x ∈ X and two sets of names u ∈ U and m ∈ M are given. Variables are used to abstract other expressions; x is bound in fun (x) a and let x = a_{1} in a_{2}. Programs are considered equal modulo renaming of bound variables. Names u and m are used to name �eld and method components of objects, respectively. Field names and method names are always free and not subject to α-conversion. The syntax of expressions is provided below.

a ::= x | fun (x) a | a a | let x = a in a
| self | u | {⟨u = a; … u = a⟩} | a#m
| ⟨field u = a; … field u = a;

                                                             method m = a; . . . method m = a⟩

Operations on references could be included as constants k (the ellipsis in syntax de�nitions means that we are extending the previous de�nition; � � marks the positions of arguments around pre�x or in�x constants):

a ::= … | k  and  k ::= ref | ( := ) | (! )

For the sake of simplicity, we omit them in the formalization, although they are used in the examples. An object is composed of a sequence of �eld bindings�the hidden internal state�, and a sequence of method bindings for accessing and modifying these �elds. Fields are also called instance variables. The type of an object is thus the type of the record of its methods. In an object, a method may return the object itself or expect to be applied to another object of the same kind. Types might thus be recursive. We assume given two countable collections of type variables and row variables, written α and ρ, and a collection of type constructors written κ.

\begin{matrix}τ ::= & α | τ → τ | (τ, … τ) κ | rec α.τ | ⟨τ̃⟩ \\ τ̃ ::= & (m : τ; τ̃) | ρ | ∅ \\ σ ::= & ∀ ᾱ. τ \end{matrix}

Object types ending with a row variable are named open object types, while others are named closed object types. In the examples, closed object types are simply written ⟨m_{i} : τ_{i}^{i∈I}⟩, i.e. the ∅ symbol is omitted. The row variables of open object types are also left implicit in an ellipsis ⟨m_{i} : τ_{i}^{i∈I}; ..⟩ (abbreviations explained in section 8 can even be used to share ellipsis). In the formal presentation, we keep both ∅ and row variables explicit. A label can only appear once in an object type. This is easily ensured by sorting type expressions [30]. The distinction between τ and τ̃ can also be guaranteed by sorts. Thus, we omit the distinction and simply write τ below.

Type equality is de�ned by the following family of leftcommutativity axioms:

(m_{1} : τ_{1}; m_{2} : τ_{2}; τ) = (m_{2} : τ_{2}; m_{1} : τ_{1}; τ)

plus standard rules for recursive types [4]:

(Rec)

\frac{τ_{1} = τ_{2}}{rec α.τ_{1} = rec α.τ_{2}}

(Fold-Unfold)

rec α.τ = τ[rec α.τ/α]

(Contract)

\frac{τ_{1} = τ[τ_{1}/α] ∧ τ_{2} = τ[τ_{2}/α] rec α.τ well-formed}{τ_{1} = τ_{2}}

Recursive types rec α.τ are only well-formed if τ is neither a variable nor of the form rec α′.τ′ (this is not too restrictive since rec α.(rec α′.τ′) can always be rewritten rec α.τ′[α/α′]). This guarantees that τ is contractive in α, and ensures that rec α.τ effectively de�nes a regular tree. Types, sorts, and type equality are a simpli�cation of those used in [31], which we refer to for details. Typing contexts are sequences of bindings:

A ::= ∅ | A + x : σ | A + field u : τ | A + self : τ

Typing judgments are of the form A ⊢ a : τ. The typing rules for ML are recalled in appendix 1.

Typing rules for objects are given in �gure 1.

A simple object is just a set of methods. Methods can send messages to the object itself, which will be bound to the special variable self. A simple object could be typed as follows:

\frac{A + self : ⟨m_{j} : τ_{j}^{j∈J}⟩ ⊢ a_{j} : τ_{j}^{j∈J}}{A ⊢ ⟨method m_{j} = a_{j}^{j∈J}⟩ : ⟨m_{j} : τ_{j}^{j∈J}⟩}

However, an object can also have instance variables. Instance variables may only be used inside methods de�ned in the same object. The typechecking of instance variables (field u_{i} = a_{i})^{i∈I} of an object produces a typing environment (field u_{i} : τ_{i})^{i∈I} in which the methods are typed (rules Object and Field).

Instance variables also provide the ability to clone an object possibly overriding some of its instance variables (rule Override). In this rule, types τ_{y} and τ_{i} do not seem to be connected. They are however, thanks to typing rule Object which requires the type τ_{y} of self and the types τ_{i} of instance variables to be related to the same object. This is also ensured by typing the premises in the context A^{⋆} equal to A \ {field, self}. As a result, the expression ⟨field u = a;method m = ⟨method m = u⟩⟩ is ill-typed. This is not a real restriction however, since one can still write the less ambiguous expression ⟨field u = a; method m =

let x = u in ⟨method m = x⟩⟩.

The rule Send for method invocation is similar to the rule for polymorphic access in records: when sending a message m to an object a, the type of a must be an object type with method m of type τ; the object may have other methods that are captured in the row expression τ′. The type returned by the invocation of the method is τ. The type of method invocation may also be seen below:

let send m a = a#m;;
value send m : ⟨ m : α; .. ⟩ → α = ⟨fun⟩

The ellipsis stands for an anonymous row variable ρ, which means that any other method than m may also be de�ned in the object a. Row variables provide parametric polymorphism for method invocation. Instead of using row variables, many other languages use subtyping polymorphism. Since subtyping polymorphism must be explicitly declared in Objective ML (see section 4), row variables are essential here to keep type inference. Row variables also allow to express some kind of matching [7] without F-bounded or higherorder quanti�cation [28, 2, 3]. Here is an example:

let min x y = if x#leq y then x else y;;
value min :
  (⟨ leq : α → bool; .. ⟩ as α) →

α → α = ⟨fun⟩

The binder �as� makes it possible to deal with open object types occurring several times in a type (this will be detailed

(Field)

\frac{field u : τ ∈ A}{A ⊢ u : τ}

(Override)

\frac{(field u_{i} : τ_{i} ∈ A  A ⊢ a_{i} : τ_{i})^{i∈I}  self : τ_{y} ∈ A}{A ⊢ \{⟨u_{i} : a_{i}^{i∈I}⟩\} : τ_{y}}

(Object)

\frac{A^{⋆} ⊢ a_{i} : τ_{i}^{i∈I} A^{⋆} + self : ⟨m_{j} : τ_{j}^{j∈J}⟩ + field u_{i} : τ_{i}^{i∈I} ⊢ a_{j} : τ_{j}^{j∈J}}{A ⊢ ⟨field u_{i} = a_{i}^{i∈I} ; method m_{j} = a_{j}^{j∈J}⟩ : ⟨m_{j} : τ_{j}^{j∈J}⟩}

(This rule will be overridden by the more general rule of same name in �gure 3.)

\frac{A ⊢ a : ⟨m : τ; τ′⟩}{A ⊢ a#m : τ}^{(Send)}

FIG. 1. Typing rules for objects

in section 8). An expanded version of this type is: rec α.⟨leq : α → bool; ρ⟩ →

rec α.⟨leq : α → bool; ρ⟩ → rec α.⟨leq : α → bool; ρ⟩

The function min can be used for any object of type τ with a method leq : τ → bool, since the row variable ρ can always be instantiated to the remaining methods of type τ.

3. Classes

The syntax for classes, introduced in section 1, is formally given in �gure 2. The body of a class is a sequence b of small de�nitions d. We assume as given a collection of class identi�ers z ∈ Z, and a collection of super-class identi�ers written s.

We have also enriched the syntax of objects so that it re�ects the syntax of classes. That is, objects can also be built using inheritance, and �elds need not precede methods.

In practice, classes will only appear at the top level. However, it is simpler to leave more freedom, and let them appear anywhere except under abstraction. Technically, it would be possible to make them �rst-class, that is to allow abstraction of classes; however, class types should be provided explicitly in abstractions. The little gain in practice is probably not worth the complication (a class can still be parameterized by other classes using modules).

The type of a class structure, sig (τ_{y}) φ end, is composed of the type τ_{y} of self (i.e. the type an object of this class would have), and the type φ of its �eld bindings and method bindings. Class types are written γ. Type schemes are extended with class types.

γ ::= sig (τ) φ end | τ → γ
φ ::= ∅ | φ; field u : τ | φ; method m : τ
| φ; super s : φ
σ ::= … | ∀ ᾱ. γ

In the concrete syntax, τ_{y} and φ are combined: methods that appear in τ_{y} but not is φ are �agged virtual (as they are not de�ned); other methods appear both in τ_{y} and φ, with the same type. When necessary, a type variable can also be bound to τ_{y}. For instance, the concrete syntax

sig (α) virtual copy : α method x : int end

expands to

  sig (rec α.⟨copy : α; getx : int; ρ⟩)
    methodgetx : int
  end.

Typing contexts are extended with class variable bindings and superclass bindings:

A ::= … | A + z : σ | A + super s : φ

We add new typing judgments A ⊢ b : φ and A ⊢ d : φ that are used to type class bodies. We also rede�ne A^{⋆} to be A where all field, method, super, and self bindings have been removed. Typing rules are given in �gure 3. We rede�ne A^{⋆} to be A \ {field, self, super}, so that superclass bindings are also removed. Generalization of class types Gen(γ, A) is, as for regular types, ∀ ᾱ. γ where ᾱ are all variables of γ that are not free in A.

Class bodies are typed by adding each component (inheritance clause, �eld, or method) one after the other. Fields are typed in A^{⋆}, since other �elds, self, and super bindings should not be visible in �eld expressions. On the contrary, methods may depend on all �elds and super-classes that were previously de�ned (rule Method). The Inherit rule ensures that self is assigned the same type in both the superclass and the subclass; all bindings of the superclass are discharged in the subclass, and the superclass variable is given the type of the superclass. Superclass variables are only visible while typechecking the body of the class but are not exported in the type of the class itself, as shown by rule Then. The rule Object is more general than (and overrides) the one of �gure 1; it corresponds to the combination of rule Class-Body and rule New.

When a value or method component is rede�ned, its type cannot be changed, since previously de�ned methods might have assumed the old type^{2}. This is enforced by using in rule Then the ⊕ operator which requires that the two argument sequences be compatible on the intersection of their domains. At �rst, this looks fairly restrictive. But it still leaves enough freedom in practice. Indeed, the class type can also be specialized by instantiating some type variables. Methods returning objects of the same type as self are thus correctly typed.

class duplicable () = struct

a ::= … | ⟨b⟩ | class z = c in a | new c | s#m  Expressions
c ::= z | fun (x) c | c a | struct b end  Class expressions
b ::= ∅ | d; b  Class bodies

d ::= inherit c as s | field u = a | method m = a

FIG. 2. Core class syntax

(Field)

\frac{A^{⋆} ⊢ a : τ}{A ⊢ field u = a : (field u : τ)}

(Method)

\frac{A ⊢ self : ⟨m : τ; τ′⟩ A ⊢ a : τ}{A ⊢ method m = a : (method m : τ)}

(Inherit)

\frac{A^{⋆} ⊢ c : sig (τ_{y}) φ end A ⊢ self : τ_{y}}{A ⊢ inherit c as s : φ + (super s : φ)}

\overline{A ⊢ ∅ : ∅}^{(Basic)}

(Then)

\frac{A ⊢ d : φ_{1} A + (φ_{1} \ method) ⊢ b : φ_{2}}{A ⊢ d; b : (φ_{1} \ super) ⊕ φ_{2}}

(Class-Body)

\frac{A^{⋆} + self : τ_{y} ⊢ b : φ}{A ⊢ struct b end : sig (τ_{y}) φ end}

(New)

\frac{A ⊢ c : sig (τ_{y}) φ end τ_{y} = ⟨method (φ)⟩}{A ⊢ new c : τ_{y}}

(Super)

\frac{super s : φ ∈ A method m : τ ∈ φ}{A ⊢ s#m : τ}

(Object)

\frac{A^{⋆} + self : τ_{y} ⊢ b : φ τ_{y} = ⟨method (φ)⟩}{A ⊢ ⟨b⟩ : τ_{y}}

(Class-Inst)

\frac{z : ∀ ᾱ. γ ∈ A}{A ⊢ z : γ[τ̄/ᾱ]}

(Class-Fun)

\frac{A + x : τ ⊢ c : γ}{A ⊢ fun (x) c : τ → γ}

(Class-App)

\frac{A ⊢ c : τ → γ A ⊢ a′ : τ}{A ⊢ c a′ : γ}

(Class-Let)

\frac{A ⊢ c : γ A + z : Gen(γ, A) ⊢ a : τ}{A ⊢ class z = c in a : τ}

FIG. 3. Typing rules for classes

method copy = {⟨ ⟩}

end;;

class duplicable : unit → sig (α)
method copy : α
end

In this class type, α is bound to the type of self. Thus, objects of any subclass of this class have types that match rec α.⟨copy : α; ..⟩. Class duplicable can then be inherited, and method copy still have the expected type (that is, the type of self).

class duplicable point x = struct
inherit duplicable () inherit point x
end;;
class duplicable point : int → sig (α)
field x : int ref
method copy : α
method move : int → int
end

Note that ancestors are ordered, which disambiguates possible method rede�nitions: the �nal method body is the one inherited from the ancestor appearing last.

Rule Class-Let, Class-Inst, Class-Fun and Class-App are similar to the rules Let, Inst, Fun and App for core ML (described in appendix 1). The two rules Class-Let and Class-Inst are essential since polymorphism of class types enables method specialization during inheritance, as explained above.

As an illustration of the typechecking rules we give a detailed derivation of the typing of the class scaled point in the appendix 2.

4. Coercion

Polymorphism on row variables enables one to write a parametric function that sends a message m to any object that has a method m. Thus, subtyping polymorphism is not required here. This is important since subtyping is not inferred in Objective ML.

There is still a notion of explicit subtyping, that allows explicit coercion of an expression of type τ_{1} to an expression of type τ_{2} whenever τ_{1} is a subtype of τ_{2}. As shown in the last example of section 1, this enables one to see all kinds of points just as simple points, and put them in the same data-structure.

The language of expressions is extended with the following construct:

a ::= … | (a : τ <: τ)

The corresponding typing rule is:

\frac{τ ≤ τ′  A ⊢ a : θ(τ)}{A ⊢ (a : τ <: τ′) : θ(τ′)}^{(Coerce)}  θ substitution

The premise τ ≤ τ′ means that τ is a subtype of τ′. As far as typechecking is concerned, we could have equivalently introduced coercions as a family of constants ( : τ <: τ′) of respective principal types ∀ ᾱ. τ → τ′ where ᾱ are free variables of τ and τ′ indexed by all pairs of types (τ, τ′) such that τ ≤ τ′.

The subtyping relation ≤ is standard [4]. We choose the simpler (and algorithmically more ef�cient) presentation of [16]. The constraint τ ≤ τ′ is de�ned on regular trees as the smallest transitive relation that obeys the following rules:

Closure rules

τ_{1} → τ_{2} ≤ τ′_{1} → τ′_{2} ⟹ τ′_{1} ≤ τ_{1} ∧ τ_{2} ≤ τ′_{2}
⟨τ⟩ ≤ ⟨τ′⟩ ⟹ τ ≤ τ′
(m : τ_{1}; τ_{2}) ≤ (m : τ′_{1}; τ′_{2}) ⟹ τ_{1} ≤ τ′_{1} ∧ τ_{2} ≤ τ′_{2}

Consistency rules

τ ≤ τ_{1} → τ_{2} ⟹ τ is of the shape τ′_{1} → τ′_{2}
τ ≤ ⟨τ_{0}⟩ ⟹ τ is of the shape ⟨τ′_{0}⟩
τ ≤ (m : τ_{1}; τ_{2}) ⟹ τ is of the shape (m : τ′_{1}; τ′_{2})
τ ≤ ∅ ⟹ τ = ∅
τ ≤ α ⟹ τ = α,

Our subtyping relation does not enhance subtyping assumptions on variables, and it is thus weaker than the subtyping relation used in [12], except on ground types.

For instance, the expression fun (x) x has type ∀ α, α′ | α ≤ α′. α → α′ in [12], while we can only type the equivalent expression fun (x) (x : τ <: τ′) for particular instances (τ, τ′) of (α, α′) such that τ ≤ τ′.

5. Semantics

We give a small step reduction semantics to our language. Values are of two kinds: regular expression values are either functions or object values. Class values are either class functions or reduced class structures. Object values and reduced class structures are composed of methods and �elds which are themselves values; �elds must precede methods and neither can be overridden in values. Values, evaluation contexts, and reduction rules are given in �gure 4.

The �rst reduction rule shows that objects are just a restricted view of classes where instance variables have been hidden.

We have chosen to reduce inheritance in objects rather than classes. It would also be possible to reduce inheritance inside classes, and reorder methods and �elds as well. Our choice is simpler and more general, since classes can also be inherited in objects.

The reduction of object expressions to values is performed in two steps, described by the four rules for objects: inheritance and evaluation of value components are reduced top-down (�rst rule, we remind that the meta-notation @ stands for the concatenation of sequences); the components are then re-ordered (last rule) and redundant components removed bottom-up (two middle rules).

The invocation of a method ⟨w⟩#m evaluates the corresponding expression w(m) after replacing self, instance variables, and overriding by their current values. That is, the following substitutions are successively applied:

1. [⟨w⟩/self] replaces self by ⟨w⟩,

2. [w(u)/u]^{u∈dom (w)} replaces each outer instance variable u by its actual value. Inner instances of u, i.e. those appearing inside an object ⟨w′⟩, are not replaced since they are related to the inner object. Note that w(u) is a value and does not contain free �elds.

3. [⟨w @ (field u = a_{u}^{u∈V})⟩/{⟨u = a_{u}^{u∈V} ⟩}]^{V ⊂U} replaces each outer occurrence of an overriding {⟨u = a_{u}^{u∈V} ⟩} by a new object built from w by overriding �elds u ∈ V by (field u = a_{u})^{u∈V}. Inner occurrences, i.e. those appearing inside an object ⟨w′⟩, are not replaced since they are related to the inner object. Note that a_{u} is not necessarily a value, and may contain other outer overriding of �elds, that should be replaced simultaneously, or equivalently in a bottom-up fashion (deeper occurrences being replaced �rst).

Coercion behaves as the identity function: the coercion of a value reduces to the value itself. Subject reduction can then only be proved by extending the type system with an implicit subtyping rule:

A ⊢ a : τ τ ≤ τ′ (Sub)

A ⊢ a : τ′

This means that a well-typed expression that has been reduced may not always be typable without rule Sub. This is not surprising since explicit subtyping may disappear during reduction. Thus, implicit subtyping may be required after reduction. It is possible however to keep explicit subtyping information during reduction, and avoid the need for rule Sub. This would be obtained by replacing the rule

(a : τ <: τ′) ⟶ a

by the following rules

(v : ⟨m_{i} : τ_{i}^{i∈I}⟩ <: ⟨m_{i} : τ′_{i}^{i∈J}⟩)

⟶ ⟨m_{i} = (v#m_{i} : τ_{i} <: τ′_{i})^{i∈J}⟩

(fun (x) a : τ_{1} → τ_{2} <: τ′_{1} → τ′_{2})

⟶ fun (x) (a[(x : τ′_{1} <: τ_{1})/x] : τ_{2} <: τ′_{2})

The counterpart is that types, although not actively participating, would be kept during reduction. The formulation we have chosen has a simpler semantics and makes it clearer that the reduction is actually untyped.

Values

v ::= … | fun (x) a | ⟨w⟩

v_{c} ::= fun (x) c | struct w end

w ::= ∅ | w_{d} ; w  field components preceed method components, no overridings
w_{d} ::= method m = a | field u = v

Evaluation contexts

E ::= [] | let x = E in a | E a | v E | E#m | ⟨F ⟩ | new E | class z = E_{c} in a
E_{c} ::= [] | E_{c} a | v_{c} E | struct F end
F ::= [] | F_{d} ; b | w_{d} ; F

F_{d} ::= inherit E_{c} as s | field u = E

From classes to objects

new (struct w end) ⟶ ⟨w⟩

Reduction of objects

inherit (struct w end) as s; b ⟶ w @ (b [w(m)/s#m]^{m∈dom (w)})
field u = v ; w ⟶ w  if u ∈ dom (w)
method m = a; w ⟶ w  if m ∈ dom (w)
method m = a; (field u = v ; w) ⟶ field u = v ; (method m = a; w)

Reduction of method invocation (U = dom (w))

⟨w⟩#m ⟶ w(m)[⟨w⟩/self][w(u)/u]^{u∈U}[⟨w @ (field u = a_{u}^{u∈V})⟩/{⟨u = a_{u}^{u∈V} ⟩}]^{V ⊂U}

Reduction of coercions

(a : τ <: τ′) ⟶ a

Reduction of other expressions

let x = v in a ⟶ a[v/x]  class z = v in a ⟶ a[v/z]
(fun (x) a) v ⟶ a[v/x]  (fun (x) c) v ⟶ c[v/x]

Context reduction

E[a] ⟶ E[a′] if a ⟶ a′  E[b] ⟶ E[b′] if b ⟶ b′
E[c] ⟶ E[c′] if c ⟶ c′

FIG. 4. Semantics of Objective ML

The soundness of the language is stated by the two following theorems.

Theorem 1 (Subject Reduction) Reduction preserves typings (i.e. for any A, if A^{⋆} ⊢ a : τ and a ⟶ a′ then A^{⋆} ⊢ a′ : τ.)

Theorem 2 (Normal forms) Well-typed irreducible normal forms are values (i.e. if ∅ ⊢ a : τ and a cannot be reduced, then a is a value.)

See appendix 4 for proofs of these theorems.

These results easily extend to cope with constants, as in core ML, provided δ-rules for constants are consistent with their principal types.

6. Type inference

Types of Objective ML are a restriction of record types. First-order uni�cation for record types is decidable, and solvable uni�cation problems admit principal solutions, even in the presence of recursion [31].

The uni�cation algorithm is a simpli�cation of the one used in ML-ART [31]. It is described in �gure 5 as a rewriting process over uni�cation problems. This formalism was introduced in [15] and has already been used for record types in [30]. A uni�cation problem also called a uni�cand, is a multi-set of multi-equations preceded by a list of existentially quanti�ed variables. It is written ∃ α_{1}, … α_{p}. e_{1} ∧ … e_{q}. A multi-equation e is a multi-set of types written τ_{1} ˙= … τ_{n}. The algorithm assumes that recursive types μα.τ have been encoded using equations ∃ α. α ˙=τ.

A substitution is a solution of a multi-equation if it makes all its types equal. A solution of a uni�cand is the restriction of a common solution to all its multi-equations outside of the existentially quanti�ed variables.

\frac{α ˙=e ∧ α ˙=e′}{α ˙=e ˙=e′}^{(Fuse)}

(Decompose (1) )

\frac{f(α_{i}^{i∈I}) ˙=f(α′_{i}^{i∈I}) ˙=e}{f(α_{i}^{i∈I}) ˙=e ∧ (α_{i} ˙=α′_{i})^{i∈I}}

(Generalize (2) )

\frac{e[τ/α] α ∉ τ}{∃ α. e ∧ α ˙=τ}

\frac{(m_{1} : α_{1}; α′_{1}) ˙=(m_{2} : α_{2}; α′_{2}) ˙=e}{∃ α′. (m_{2} : α_{2}; α′_{2}) ˙=e ∧ α′_{1} ˙=(m_{2} : α_{2}; α′) ∧ α′_{2} ˙=(m_{1} : α_{1}; α′)}^{(Mutate)}

(1) In Rule Decompose, f is any type symbol, including (m : ; ) as well.

(2) To ensure termination, rule Generalize must be restricted to the case where τ is not a variable and α appears in e but not as a term variable of e.

FIG. 5. Uni�cation as solving multi-sets of multi-equations

Uni�cands can be simpli�ed by applying the rewriting rules given in �gure 5. Structural rules have been omitted: they include associativity and commutativity of both ∧ and ˙= and the extrusion and renaming of existential variables. Rules Fuse, Decompose and Generalize are standard. Rule Fuse merges two multi-equations that have a variable in common. Rule Decompose decomposes terms of a multi-equations into smaller ones. Rule Generalize splits terms into smaller terms. Thus, uni�cands can always be rewritten so that terms are of depth at most one. This permits maximal sharing during uni�cation. It also ensures termination of rewriting in the presence of recursive types. The only difference with uni�cation in a free algebra is the mutation rule Mute for left-commutativity. It identi�es two terms (m_{1} : τ_{1}; τ′_{1}) and (m_{2} : τ_{2}; τ′_{2}) with different top symbols (m_{1} : ; ) and (m_{2} : ; ) provided their equality can be established by the application of an axiom at the root.

The algorithm proceeds by rewriting multi-sets of multiequations according to the above rules. Each step preserves the set of solutions. Moreover, the process always terminates, reducing any uni�cand to a canonical form.

A uni�cand is in a solved form if all of its multi-equations are merged and each of them is fully decomposed (i.e. it contains at most one non-variable term). Principal uni�ers can be read directly from solved forms. A canonical uni�cand that is not in a solved formed contains a clash (two incompatible types that should be identi�ed) and is not solvable.

The framework and the meta-theory of uni�cands are standard. The equational theory of object types is a sub-case of the more general algebra of records types; for details and proofs, the reader is referred to [30].

Objective ML does not allow classes as �rst-class values. Indeed, in the expression fun (x) a, variable x cannot be bound to a class (or a value containing a class). Thus, class types never need to be guessed. Polymorphism is only introduced at Let bindings of classes or values. This ensures that type inference reduces to �rst-order uni�cation, as it is the case in ML. Consequently, Objective ML has the principal type property. Type inference for classes is straightforward. The links between �rst-order uni�cation, type inference and principal types are described in a more general setting in [29].

Theorem 3 (Principal types) For any typing context A and any program a that is typable in the context A, there exists a type τ such that A ⊢ a : τ and for any other type τ′ such that A ⊢ a : τ′ there exists a substitution θ whose domain does not intersect the free variables of A and such that τ′ = θ(τ).

7. Abbreviation enhancements

Object types tend to be very large. Indeed, the type of an object lists all its methods with their types, which can themselves contain other object types. This quickly becomes unmanageable [31, 11]. Introducing abbreviations is thus of crucial importance. This section presents the general abbreviation mechanism of Objective ML and the next section focuses on abbreviating object types. The simple type abbreviation mechanism of ML is not suf�ciently powerful: abbreviations are expanded and lost during uni�cation and they do not interact well with recursive types. Several improvements have thus been made to the abbreviation mechanism. First, abbreviations are kept during uni�cation and propagated as much as possible. Second, a larger class of abbreviations are accepted: abbreviations can be recursive and their arguments can be constrained to be instances of some given types.

In our implementation, types are considered as graphs. In particular, when two types are uni�ed, they become identical rather than two separate, equal types. A construct has been added to the syntax to express type graphs: the construct (τ as α) is used to bind α to τ, similarly to the notation rec α.τ. However, a main difference is that with aliases α is also bound outside of τ. As an example, the two types (⟨m : α⟩ as α′) → α′ and ⟨m : α⟩ → ⟨m : α⟩ are different graphs, that represent the same regular tree. There are two reasons for considering types as graphs. First, uni�cation rolls types. For instance, unifying types τ = α and τ′ = ⟨m : α⟩ results in type τ = τ′ = (⟨m : α⟩ as α), rather than instantiating α to ⟨m : α′⟩ as α′ in both types (in the later case, τ′ would become ⟨m : ⟨m : α′⟩ as α′⟩). Second, uni�cation propagates abbreviations. Abbreviations can be considered as names for nodes. Unifying an abbreviated type with another type makes both types abbreviated. For instance, unifying the argument of a functional type to an abbreviated type may propagate the abbreviation to the result type. This is demonstrated in the following example.

let bump x = x#move 1; x;;
value bump :
  (⟨ move : int → β; .. ⟩ as α) → α =
  ⟨fun⟩

Nodes are shared between the argument type and the result type. The ellipsis stands for an anonymous row variable. When typing the expression bump p below, type (⟨move : int → β; ..⟩ as α) and type point are identi�ed. The type of bump p is thus also abbreviated to

point.
let p = new point 7;;
value p : point = ⟨obj⟩
bump p;;
− : point = ⟨obj⟩

Not all the sharing is exposed to the user : sharing reveals too much useless information. So, only aliasing of open object types (thus row variables can be printed as ellipses) and aliasing de�ning recursive types are printed. It would be possible to remove some aliasing during type generalization, so that printed types would exactly re�ect their internal representations. However, this would complicate the implementation needlessly.

Abbreviations can be recursive. That is, in the de�nition of the abbreviation type (ᾱ) κ = τ, the type constructor κ may occur in the body τ, as long as all occurrences have the same parameters ᾱ. This restriction is extended to mutually recursive abbreviations. It ensures that abbreviations expand to regular trees. In the implementation, any type constructor standing for an abbreviation caches the expansions of abbreviations it appears in. Thus, when an abbreviation is expanded several times during the traversal of a type, it expands each time to the same type.

Type abbreviations are generalized to allow constraints on the type parameters of the abbreviations. This is an extension to the abbreviations of LCS [5], that were also used in [31]. In an abbreviation de�nition, parameters are types rather than type variables: type (τ̄) κ = τ_{0}. All free variables of τ must be bound in τ̄. Actual arguments of an abbreviation must always be instances θ(τ̄) (for some substitution θ) of the parameters τ̄. Then, the abbreviation can expand to type θ(τ_{0}). For instance, if the type constructor κ is de�ned as type (α∗α′) κ = α → α′, then (int∗bool) κ will expand to int → bool. To expand an abbreviation, the arguments are usually substituted for the parameters. Instead, we choose to unify the arguments with the corresponding parameters. The constraints need only to be enforced when parsing a type given by the user. Then, expansion is guaranteed to succeed. Indeed, a substitution θ can always be applied to an abbreviation (τ̄) κ. The expansion of θ((τ̄) κ) is equal to the result of applying the substitution θ to the expansion of (τ̄) κ. In particular, constraints are preserved by substitution.

8. Abbreviating object types

We will now describe how the abbreviation mechanism presented in the previous section is used to generate abbreviations for objects. This mechanism is used to automatically abbreviate object constructors: the expression new z will have type τ_{1} → … → τ_{n} → (τ′_{i}) κ_{z}, where κ_{z} is the abbreviation associated with class z.

General type abbreviations, introduced in the previous section, can be used to simplify object types. Rather than sorting types to ensure that object types are well-formed, we require the stronger condition that any two object types that share the same row variable must be equal. This eliminates incorrect types such as ⟨ρ⟩ → ⟨m : τ; ρ⟩. Types such as ⟨m : τ_{1}; ρ⟩ → ⟨m : τ_{2}; ρ⟩, at the basis of record extension, are also rejected. However, no primitive operation on objects exhibits such a type. These types can thus be ruled out without seriously restricting the language. Moreover, all programs keep the same principal types. This restriction was implemented to avoid explaining sorts to the user. It also makes the syntax for types somewhat clearer, as row variables can then always be replaced by ellipsis. Furthermore, sharing can still be described with aliasing. For instance, ⟨m : τ; ρ⟩ → ⟨m : τ; ρ⟩ is written (⟨m : τ; ..⟩ as α) → α. A class de�nition class z = c in … automatically generates an abbreviation for the type of its instances. For specifying it, one actually needs to add type parameters to the class de�nitions, corresponding to the one of the abbreviation. That is, we should write

class (ᾱ) z = c in …  (1)

where the parameters ᾱ must appear in c.

In fact, abbreviations are generated from class types. It follows from type inference that the class de�nition c has a principal class type τ′_{0} → … → τ′_{n} → sig (τ_{y}) φ end. Here, τ_{y} is the type matched by objects in all subclasses. It is always of the form ⟨m_{i} : τ_{i}^{i∈I}; τ⟩ where method (φ) is a subsequence of (m_{i} : τ_{i})^{i∈I} and τ is either ∅ (this is a pathological case, where the class cannot be extended with new methods) or a row variable ρ. If method (φ) is exactly (m_{i} : τ_{i})^{i∈I}, then it is possible to create objects of that class; they will have type τ_{y}[∅/ρ]. Otherwise, the class is virtual and can only be inherited in other class de�nitions. If all free type variables of τ_{y} except ρ are listed in ᾱ, we automatically de�ne two abbreviations:

type (ᾱ, ρ) #κ_{z} = τ_{y} type (ᾱ) κ_{z} = (ᾱ, ∅) #κ_{z}

The former matches all objects of subclasses of c. The latter is a special case of the former, and abbreviates any objects of class c.

Let us consider an example. Class point has type int → sig (⟨move : int → int; ρ⟩) φ end for some φ whose only method is move : int → int. Thus, class point is not virtual. The two following abbreviations are generated for this class:

type ρ #point = ⟨move : int → int; ρ⟩
typepoint = ⟨move : int → int⟩

One can check that the type point is indeed an abbreviation for the type of objects of the class point, and that the type of an object of any subclass of the class point is an instance of the type ρ #point.

In the concrete syntax, the row variable ρ is treated anonymously (as an ellipsis) and is omitted. The former abbreviation #κ_{z} is given a lower priority than the regular ones in case of a clash. It also vanishes as soon as the row variable is instantiated, so as to reveal the value taken by the row variable.

In fact, we allow κ_{z} and #κ_{z} to occur in the de�nition of b. The previous de�nitions can be rewritten to handle the general case correctly.

Constrained abbreviations are natural for abbreviating objects, as, for instance, a sorted list of comparable objects should be parameterized by the type of its elements, which in turn is not a type variable. Moreover this extension makes it possible to avoid row variables as type parameters (as the whole object type can appear as a parameter).

Constrained type abbreviations are also convenient since, in a class de�nition class (ᾱ) z = c in …, class type parameters ᾱ may have been instantiated to some types τ̄_{α} while inferring the class type τ′_{0} → … → τ′_{n} → sig (τ_{y}) φ end. The two abbreviations generated by the class de�nition are thus:

type (\overline{τ_{α}}, ρ) #κ_{z} = τ_{y} type (ᾱ) κ_{z} = (ᾱ, ∅) #κ_{z}

The latter is unchanged except that the constraints of the �rst ones are implicit in the second one.

Class types are shown to the user stripped of their type parameters. The parameters that constraint the type abbreviations are described by constraint clauses:

class α circle (p : α) = struct
field point = p
method center = point
method move m =
if m = 0 then 0 else
point#move (1 + Random.int m)
end;;
class α circle : α → sig
constraint α = ⟨ move : int → int; .. ⟩
field point : α
method center : α
method move : int → int
end

This class de�nes the abbreviation

type (⟨move : int → int; ρ⟩ as α) circle =
⟨center : α; move : int → int⟩

As a result of the abbreviation mechanisms, type inference may reject some class de�nitions whose principal types have free variables. For instance, the following variant of class point is rejected, since the method getx is polymorphic and therefore the class should be parametric.

class point x0 = struct
  field x = x0
  method getx = x
end;;

Of course, one could choose an arbitrary ground class type, for instance:

class point : int → sig
  field x : int
  method getx : int
end

Any other ground type could be used instead of int. We decide to reject those programs. This preserves the property that any typable program has a principal type �and all other useful properties of the type system.

This phenomenon is not new. It already appeared in several extensions of ML. Imperative constructs limit polymorphism. Thus, some variables that are not generalizable may occur in the type of a top level expression. In such a case, most languages would reject the program. For instance, the extension to ML with dynamics [20] rejects fun x → dynamics x, since the dynamic type of x in dynamics x is statically unknown.

All the examples above would have principal types as long as type inference is concerned. We can argue that some programs have been rejected for sake of simplicity and uniformity of the language, but not because of a failure of type inference: For instance, in Objective ML we could just omit the corresponding abbreviation whenever some type parameter is missing, and print a warning message instead of an error message.

9. Extensions

This section lists other useful features of Objective ML that have been added to the implementation. Imperative features have been ignored in the formal presentation since their addition is theoretically well-understood and independent of the presence of objects and classes. Other features are less important in theory, but still very useful in practice: private instance variables, coercion primitives.

Before we explore these extensions, let us consider an interesting restriction of the language. If recursive types are only allowed when the recursion traverses an object type, Objective ML becomes a conservative extension of ML, which we claimed in the introduction. Of course, all ML programs can be de�ned, and behave similarly. Moreover, programs that are syntactically ML programs are now well-typed ML programs if and only if they are well-typed in Objective ML. However, in the implementation Objective Caml, the presence of modules requires the use of recursive abstract types as well. This is because recursive object types may be abstracted. Thus, Objective Caml is not strictly speaking a conservative extension of ML. Still, it is a conservative extension of ML with recursive types.

9.1. Imperative features

We have intentionally used references in the very �rst example. We did not formalize references in the presentation of Objective ML, since we preferred to keep the presentation simple and put emphasis on objects and classes. The addition of imperative features to Objective ML is theoretically as simple and as useful practically as their addition to ML. Both the semantics and the properties of reduction with respect to typing extend to operations on the store without any problem. The formalization copies the one for core ML.

In fact, the implementation Objective Caml also allows �elds to be mutable in a similar way mutable record �elds are treated in Caml [21]. For instance, we could have written:

class point x0 = struct
  field mutable x = x0
  method move d = (x ← x + d; x)
end;;
class point : int → sig
  field mutable x : int
  method move : int → int
end

Objective Caml only allows generalization of values (actually, a slightly more general class of non expansive expressions). The creation of an object from a class c is not considered as a value (as it is the application of function new c to some arguments). Mutable �elds in classes are typed as any other �elds, except that mutability properties are also checked during typechecking.

9.2. Local bindings

As shown by the evaluation rules for objects, both value and method components are bound to their rightmost de�- nitions. All value components must still be evaluated even though they are to be discarded.

Object-oriented languages often offer more security through private instance variables. The scope of a �eld can be restricted so that the �eld is no more visible in subclasses.

This section presents local bindings, that are only visible in the body of the class they appear in. This is weaker than what one usually expects from private �elds, as a class cannot, for instance, inherit a �eld and hide it from its subclasses (see section 10.1).

The syntax is extended as follows:

d ::= … | local x = a in b
F_{d} ::= … | local x = E in b

with the corresponding typing rule:

A^{⋆} ⊢ a : τ A + x : τ ⊢ b : φ (Local)

A ⊢ local x = a in b : φ

Local bindings are reduced top-down, like inheritance:

local x = v in b; b′ ⟶ b[v/x] + b′

In practice, however, local bindings would rather be compiled as anonymous �elds. This would make methods independent of local bindings.

Initialization parameters could also be seen as local bindings in the whole class body, and could also be compiled as anonymous instance variables. For instance, the de�nition

                                                 class point y = struct method x = y end;;

could be automatically transformed into the equivalent program:

                                                 class point y = struct
                                                   local y = y in method x = y
                                                 end;;

That way, the method x becomes independent of the initialization parameter y. Then, classes can be reduced to class values: inheritance is reduced to local bindings, local bindings are �attened, and method overriding is resolved.

9.3. Coercion primitives

Explicit coercions require both the domain and co-domain to be speci�ed. This eliminates the need for subtype inference. In practice, however, it is often suf�cient to indicate the co-domain of the coercion only, the domain of the coercion being a function S of its co-domain.

For convenience, we introduce a collection of coercion primitives:

( <: τ) : ∀ ᾱ. S(τ) → τ

where ᾱ are free variables of S(τ) and τ, and S(τ) is de�ned as follows:

• We call positive the occurrences of a term that can be reached without traversing an arrow from the left hand side. (This is more restrictive than the usual de�nition, where the arrow is treated contravariantly).

• For non recursive terms, we de�ne S_{0}(τ) to be τ where every closed object type that occurs positively is opened by adding a fresh row variable.

• Terms with aliases are viewed as graphs, or equivalently as pairs of a term τ_{0} and a list of constraints α_{i} = τ_{i}. Let θ be a renaming of variables α_{i} into fresh variables. Let τ′_{i} be τ_{i} in which every positive occurrence of each α_{i} is replaced by θ(α_{i}). We return (S_{0}(τ′_{0}), {θ(α_{i}) = S_{0}(τ′_{i}), i ∈ I} ∪ {α_{i} = τ_{i}, i ∈ I}) for S(τ).

For example, S(⟨m_{1} : ⟨m_{2} : int⟩ → ⟨m_{3} : bool⟩⟩) =

⟨m_{1} : ⟨m_{2} : int⟩ → ⟨m_{3} : bool; ρ_{3}⟩; ρ_{1}⟩

S(⟨m : α⟩ as α) = ⟨m : α′; ρ⟩ as α′

S(⟨m : α → α⟩ as α) = ⟨m : (⟨m : α → α⟩ as α) → α′; ρ⟩ as α′

The operator S has the two following properties:

(1) S(τ) ≤ τ (2) ∃θ (θ(S(τ)) = τ ∧ θ(τ) = τ)

The former gives the correctness of the reduction step (a <: τ) ⟶ (a : S(τ) <: τ). The latter shows that if a has type τ then (a <: τ) also has type τ.

There is no principal solution for an operator S satisfying (1). Consider τ to be ⟨m : int⟩ → int. There are only two solutions, ⟨m : int⟩ → int and ⟨⟩ → int and none is an instance of the other. This counter-example shows the weakness of the simulation of subtyping with row variables, especially on negative occurrences. There are other examples of failure on positive occurrences, but only using recursive types. For instance, if τ is ⟨x : α⟩ as α, then both ⟨x : τ; ρ⟩ and ⟨x : β; ρ′⟩ as β are solutions for S(τ), but no solution is more general than both of these. Our choice of S (and correspondingly, our choice of coercion primitives) is somehow arbitrary, but works well in practice. This justi�es the exclusion of semi-explicit coercions from the core language, but leave them as a collection of primitives. In fact, most coercions are of the form (a : S(τ) <: τ). Thus, the domain of a coercion rarely needs to be given.

10. Future work

This short section describes three possible extensions of importance to Objective ML. Each extension requires further theoretical and design investigation before it can be integrated within Objective Caml.

10.1. Restriction of class interfaces

In section 9.2 we have shown that �eld components can be declared local to a class. However, this does not enable class components to be hidden a posteriori. Assume, for instance, that a library provides an implementation of a class z with two �elds x and x′ and two methods m and m′. A module may de�ne a class z′′ that inherits from an imported class z′ whose interface is a restriction of the one of the class z to the �eld x and the method m only. Can class z be used as an import to the module? This problem corresponds to a common situation of interface restriction when reusing code. However, interface restriction is not currently possible.

Private �elds would actually not be dif�cult to hide. However, hiding methods in subclasses con�icts with late binding and a �at method name space. For instance, assume, method m′ is implicitly hidden when inherited in class z′′, and that class z′′ de�nes a method m′, possibly with another type!

Clearly, when a method m is hidden in a class z, selfinvocations of m in all other methods of z should be replaced by calls to a function representing the method m. This is a complex operation that is dif�cult to compile.

Another problem is that method m′ appears in the type of self. Hiding the method thus requires to modify a posteriori the type of self. This would not be correct if, for instance, this type is the type of a method argument.

A partial solution is to give each method a different view of self inside classes. This is usually the case when classes are treated as a collection of pre-methods. Another choice, weaker but still useful, is to split the input and output view of self. The former lists the methods that are required while the latter enumerates methods that are provided. However, in the presence of type inference, such solutions tend to increase the size of a class to a point that may become unreadable [31]. The gain in expressiveness is also weakened by a later detection of errors. Clearly, it is an error if a method has incompatible required and provided types. However, this would only be detected when the object is created. In the design of Objective ML, we have deliberately limited the expressiveness of class types to keep them readable. Many variations are theoretically possible, but very few of them seem to improve expressiveness signi�cantly without sacri�cing simplicity.

Another possibility is to introduce private methods. They would not appear in the type of self, consequently, they should be invoked differently. Private methods could have the same scope as �elds. In particular, they could be hidden a posteriori as well.

The addition of �nal classes could also resolve the problem. These classes could not be inherited. Then, a class could be soundly matched against a �nal class interface that omits some of its methods.

10.2. Polymorphic methods

In a classical programming style, functions and data are clearly separated. Functions are often polymorphic and thus can be applied uniformly to different kinds of data. Data may be structured. It very rarely carries functions, and is usually monomorphic. In objects, data and methods are jointly de�ned and stored or passed as arguments together � at least from a theoretical point of view.

Let-bound top level functions often become methods of λ-bound �rst-class objects. Unfortunately, polymorphism is lost during this transformation. For instance, a class implementing sets, would naturally provide a fold method. The inferred class type would be of the form:

class α set = struct  ...
  method fold : (α → β → β) → β → β
end

However, this is rejected, since variable β is unbound in α set. An attempt to �x the problem would be to parameterize the class set over β as well, that is, to replace α set in the de�nition above by (α, β) set. However, this is not very intuitive, since the object stays parametric in β even when all its �elds have a ground type. Moreover, the method fold becomes monomorphic and thus can only be applied to functions of the same type, whenever the object is λ-bound.

The intuition is of course that the method fold should be polymorphic. That is, the class set should have the following class type:

class α set = struct ...
method fold : All β. (α → β → β) → β → β
end

The addition of polymorphic methods could also be used to reduce the number of explicit coercions. In a class de- �nition methods may have types more polymorphic than expected. For instance, assume that class point has type:

class point (int) = struct
field x : int  method getx : int
end;;

Then, the following subclass of point will not typecheck:

class eq point x = struct
inherit point x
method eq p = p#getx = self#getx
end;;

The parameter p of the method eq does not need to be a point but an object with method getx of type int. Thus, its type ⟨getx : int; ..⟩ → bool has a free row variable. As for the case of set, the row variable in the type of p can be bound in in a constraint type parameter as follows:

class α eq point x = struct
inherit point x
method eq (p:α) = p#getx = self#getx
end;;
class α eq point : int → sig
constraint α = ⟨ getx : int; .. ⟩
field x : int
method getx : int
method eq : α → bool
end

Again, this is not very intuitive and one might prefer to add a stronger type constraint. One choice is to require p to be of the same type as self. However, this unnecessarily makes eq a binary method and so restricts its further use with arguments of type eq point only. Constraining p to be a point in the de�nition of the method eq is another possibility:

class eq point x = struct
inherit point x
method eq (p:point) = p#getx = self#getx
end;;

class eq point : int → sig
  field x : int
  method getx : int
  method eq : point → bool
end

This solution is more general, although it usually requires explicit coercion when invoking the method eq:

let p = eq point 1 in p#eq (p ⟨: point);;

Polymorphic methods would allow a more natural class type for the eq point (�rst de�nition):

class eq point : int → sig
  field x : int
  method getx : int
  method eq p :
      All (⟨getx : int; ..⟩ as α). α → bool
end;;

Moreover, thanks to the polymorphic (anonymous) row variable, messages could then be sent to the method eq with an argument of type either point or eq point.

We consider that the lack of polymorphic methods is a weakness of Objective ML. We believe that polymorphic methods would make most explicit coercions unnecessary.

Some solutions to extend ML with �rst classpolymorphism already exist in the literature. Simple but rudimentary proposals can be found in [31, 24] and better integration of �rst-class polymorphism inside Objective ML has recently been studied in [14].

10.3. Integrating classes and modules

Objects and classes of Objective ML are orthogonal to the other extensions of ML. In particular, the module system of ML extends directly to classes and objects [18]. Indeed, the implementation of Objective ML, called Objective Caml [19], offers a rich language of both modules and classes. Classes and modules share a lot of properties: they offer some form of abstraction; they also help structuring large applications; and they facilitate reusability of code. In fact, they are quite different. Modules are a very general and powerful abstraction. However, it is dif�cult to allow recursion between several modules or to give a meaning to self inside modules. On the other hand, classes are a much more specialized paradigm that has proved extremely convenient for some applications. Objects �nd their limitation with multiple dispatch. Hiding components also remains a dif�cult task.

For historical reasons, libraries of Objective Caml are implemented as modules. In practice, many of these libraries could be rewritten as classes. Choosing one style or another is not insigni�cant, since it is a global commitment to the architecture of the application. The class version and the module version of the same libraries are very similar, but their code cannot currently be shared. This is, of course, unsatisfactory. We hope that more work will allow a better integration of modules and classes.

11. Comparison to other works

The work closest to Objective ML is ML-ART [31]. Here, object types are also based on record types and have similar expressiveness. State abstraction is based on explicit existential types in ML-ART; in Objective ML, it is obtained by scope hiding, but it could also be explained with a simple form of type abstraction. No coercion at all is permitted in ML-ART between objects with different interfaces. Unfortunately, ML-ART has no type-abbreviation mechanism. This was a major drawback, which motivated the design of Objective ML. On the other hand, classes are �rst class values in ML-ART. We, however, do not think this is a major advantage. The restriction is a deliberate choice in the design of Objective ML, to keep the language simpler. In theory, most features of ML-ART could have been kept in Objective ML. In practice, however, it would have changed the language signi�cantly.

Another simpli�cation in Objective ML is that in classes all methods view self with the same type. This is not required by the semantics, and could technically be relaxed by making method types more detailed in classes (see [31]). We found that this extra �exibility is not worth the complication of class types.

Our object types are a simpli�cation of those used in [32]. The simpli�cation is possible since object types are similar to record types for polymorphic access, and do not require the counterpart of record extension. Moreover, as discussed above, our implementation assumes the stronger condition that two object types sharing the same row variable are always identical. With this restriction, object types seem to be equivalent to kinded record types introduced in [25]. Ohori also proposed an ef�cient compilation of polymorphic records (which does not scale up to extensible records) in [26]. However, his approach, based on the correspondence between types and domains of records cannot be applied to the compilation of objects with code-free coercions.

Objects have been widely studied in languages with higher-order types [9, 23, 7, 2, 28, 6]. These proposals signi�cantly differ from Objective ML. Types are not inferred but explicitly given by the user. Type abbreviations are also the user’s responsibility. On the contrary, all these proposals allow for implicit subtyping.

Our calculus differs signi�cantly from Abadi’s and Cardelli’s primitive calculus of objects mostly as a result of design choices. We have chosen primitive classes because inferred types of sets of pre-methods would be too complex to be readable (see [31] for instance). We have emphasized the role of row variables because we have chosen not to infer subtyping, therefore avoiding the more complicated framework of constraint types. On the other hand we have included other features such as instance variables, to avoid their encoding as methods not involving self, and to keep with the more simple state-abstraction mechanism by scope hiding. Technically a major difference, Objective ML does not allow method overriding.

Open record types are connected to the notion of matching introduced by Kim Bruce [7, 8]. Matching seems to be at least as important as subtyping in object-oriented languages. Row variables in object types express matching in a very natural way. While explicit matching may require too much type information, type inference makes object matching very practical.

Palsberg has proposed type inference [27] for a �rst-order version of Abadi and Cardelli’s calculus of primitive objects [1]. However, that language is missing important features from the higher-order version [2]. Type inference is based on subtyping constraints and the technique is similar to the one used in [11]. This latter proposal [11, 12] is closer to a real programming language, and more suited for comparison. Here, the authors use a subtyping relation that is more expressive than ours, as they can prove subtyping under some assumptions. They can also infer coercions. However, the types they infer tend to be too large. Indeed, they do not have an abbreviation mechanism. Their inheritance is weaker than ours since they must explicitly list all inherited methods in subclasses. We think the two proposals are complementary and could bene�t from one another. In particular, it would be interesting to adapt automatic type abbreviations to constraint types. The problem is still nontrivial since inferred type-constraints are hard to read even in the absence of objects.

The remainder of this section is dedicated to the comparison with three other proposals for adding objects to ML. They all use implicit subtyping, which is, however, restricted to atomic structural subtyping [22, 13]. As a result, they all have the same dif�culty with parameterized classes, making it impossible to relate objects created from classes with a different number of parameters, even when the objects have the same interface. For instance, objects of a class string are of incompatible type with objects of a parameterized class vector when the parameter type is character. In Objective ML, such objects could be mixed.

In [6], Bourdoncle and Metz propose a language based on some restricted form of type constraints [12]. However, they do not provide type inference.

The two following proposals include type inference; however, fully polymorphic method invocation cannot be typed. Two different solutions are proposed; they both amount to providing some explicit type information at method invocation.

More precisely, in Duggan’s proposal [10], methods must be predeclared with a particular type scheme. Thus methods carry type information like data-type constructors in ML. For instance, move would be assigned type scheme ∀ α_{y}. α_{y} → int. Type schemes that are assigned to methods are polymorphic in α_{y}: they are arrow types whose domain is always a variable α_{y}, standing for the type of self. Object types only list the methods that objects of that type must accept. For instance, point would be given type ⟨move⟩. The user must provide more type information that in Objective ML. The same method name cannot be used in two different objects with unrelated types. Objects of parameterized classes are treated especially, using constructor kinds. As mentioned above, objects of a parameterized class reveal forever that they are parameterized. For instance, let us consider a class of vectors parameterized over the type α. All methods of that class must be given a type scheme of the form: ∀ α_{κ}^{T ype→T ype}. ∀ α. α α_{κ}→ τ, where variable α_{κ} range over type constructors. That is, instead of the type τ_{y} of self, only the type constructor κ of the type τ_{y} is hidden. This reveals the dependence of τ_{y} on its parameters, and the parameters themselves. As explained above, methods of parameterized classes are incompatible with methods of non-parameterized classes. Conversely, Objective ML does not currently allow polymorphic methods while Duggan’s proposal does. A polymorphic method map could be declared with type scheme: ∀ α_{κ}^{T ype→T ype}. ∀ α. ∀ α_{1}. α α_{κ}→ (α → α_{1}) → α_{1} α_{κ}. Intuitively, map carries implicit universal intros and elims, like data constructors carry arguments of existentially or universally quanti�ed types in [17, 31, 24]. Recursive kinds actually allow some form of polymorphism that is different from polymorphic methods discussed in section 10.

In Object ML [34], Reppy and Riecke treat objects as a generalized form of concrete data-types. Types are also inferred in Object ML, but the authors do not claim a principal type property. Also, method invocation must always mention the class of the object to which the method belongs. Each object is actually tagged with a constructor that carries the class the object originated from. Therefore, objects can be tested for membership to some arbitrary class in some inheritance relationship. Only single inheritance is allowed. The subtyping relationship between objects is declared and corresponds to the inheritance forest. Classes are generative, that is, objects of different classes have different types. Although these types can be related by subtyping, they are never in an instance relationship. Some object coercions, but apparently not all, are implicit. On the contrary in Objective ML, classes are transparent, that is, objects types are structural and only describe the interface of objects: two objects with exactly the same interface have equal types. Two objects of classes in a subclass relationship are not necessarily related, but when they are, one type is simply an instance of the other. Object ML does not provide any inheritance mechanism, except by means of encodings [33]. Typing of binary methods is also a problem, which is solved via runtime class-type tests.

Conclusion

Objective ML has been designed to be the core of a real programming language. Indeed, the constructs presented here have been implemented in Objective Caml. We chose class-based objects since this approach is now well understood in a type framework and it does not require higher-order types.

The original part of the design is automatic abbreviation of object types. Although this is not dif�cult, it is essential for making the language practical. It has been demonstrated before that fully inferred object types are unreadable [31, 11]. On the contrary, types of Objective ML are clear and still require extremely little type information from the user. To our knowledge, all other existing approaches require more type declarations.

Objective ML is also interesting theoretically for the use of row variables [35, 32]. Row variables are very close to matching and seem more helpful than subtyping for the most common operations on objects. Message passing and inheritance are entirely based on row variables, which relegates subtyping to a lower level.

Another interesting aspect of our proposal is its simplicity. This is certainly due to the fact that Objective ML is very close to ML. Speci�cally, most features rely only on ML polymorphism. This leads to very simple typing rules for objects and inheritance. Coercions, based on subtyping, can be explained later. Data abstraction is guaranteed by scope hiding rather than by type abstraction; this is a less powerful but simpler concept.

The main drawback of Objective ML is the need for explicit coercions. Coercions are necessary. However, we think they occur in few places. Thus, explicit coercions should not be a burden. Furthermore, coercions could in theory be made implicit using constraint-based type inference. In our implementation of Objective ML, classes and modules are fully compatible, but orthogonal. That should be particularly interesting to compare these two styles of largescale programming, and help us to better integrate them. This is an important direction for future work.

Acknowledgments

We thank Rowan Davies who collaborated in the implementation and the design of a precursor prototype of Objective ML.

Notes

1. The syntax has been slightly modi�ed here in order to keep the concrete syntax and the abstract syntax closer.

2. One may imagine relaxing this constraint, and allow the type of the rede�ned method to be a subtype of the original method. One would, however, lose a property we believe important: rule Inherit shows that the type a class gives to self is a common instance of the different types of self in its ancestors; as a consequence, the type of self in a class uni�es with the type of any object of a subclass of this class.

References

[1] Mart��n Abadi and Luca Cardelli. A theory of primitive objects: Untyped and �rst-order systems. In Theoretical Aspects of Computer Software, pages 296�320. Springer-Verlag, April 1994.

[2] Mart��n Abadi and Luca Cardelli. A theory of primitive objects: Second-order systems. Science of Computer Programming, 25(2-3):81�116, December 1995. Preliminary version appeared in D. Sanella, editor, Proceedings of European Symposium on Programming, pages 1-24. Springer-Verlag, April 1994.

[3] Mart��n Abadi and Luca Cardelli. A theory of objects. Springer, 1996.

[4] Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. Transactions on Programming Languages and Systems. ACM, 15(4):575�631, 1993.

[5] Bernard Berthomieu. Programming with behaviors in an ML framework, the syntax and semantics of LCS. Research Report 93-133, LAAS-CNRS, 7, Avenue du Colonnel Roche, 31077 Toulouse, France, March 1993.

[6] Franc�ois Bourdoncle and Stephan Merz. Type checking higher-order polymorphic multi-methods. In Proceedings of the 24th ACM Conference on Principles of Programming Languages, pages 302�315, July 1997.

[7] Kim B. Bruce. Typing in object-oriented languages: Achieving expressiveness and safety. To appear.

[8] Kim B. Bruce, Angela Schuett, and Robert van Gent. Polytoil: A type-safe polymorphic object-oriented language. In ECOOP, number 952 in LNCS, pages 27�51. Springer Verlag, 1995.

[9] Peter Canning, William Cook, Walter Hill, Walter Olthoff, and John Mitchell. F-bounded quanti�cation for object-oriented programming. In Fourth International Conference on Functional Programming Languages and Computer Architecture, pages 273�280, September 1989.

[10] Dominic Duggan. Polymorphic methods with self types for ML-like languages. Technical report CS-95-03,, University of Waterloo, 1995.

[11] J. Eifrig, S. Smith, and V. Trifonov. Sound polymorphic type inference for objects. In OOPSLA, 1995.

[12] J. Eifrig, S. Smith, and V. Trifonov. Type inference for recursively constrained types and its application to OOP. In Mathematical Foundations of Programming Semantics, 1995.

[13] You-Chin Fuh and Prateek Mishra. Type inference with subtypes. In ESOP ’88, volume 300 of Lecture Notes in Computer Science, pages 94�114. Springer Verlag, 1988.

[14] Jacques Garrigue and Didier R� emy. Extending ML with semi-explicit higher-order polymorphism. In International Symposium on Theoretical Aspects of Computer Software, Japan, September 1997.

[15] Claude Kirchner and Jean-Pierre Jouannaud. Solving equations in abstract algebras: a rule-based survey of uni�cation. Research Report 561, Universit� e de Paris Sud, Orsay, France, April 1990.

[16] Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Ef�cient recursive subtyping. In Proc. 20th symp. Principles of Programming Languages, pages 419�428. ACM press, 1993.

[17] Konstantin L� aufer and Martin Odersky. An extension of ML with �rstclass abstract types. In Proceedings of the ACM SIGPLAN Workshop on ML and its Applications, 1992.

[18] Xavier Leroy. A modular module system. Research report 2866, INRIA, April 1996.

[19] Xavier Leroy. The Objective Caml system. Software and documentation available on the Web, http://pauillac.inria.fr/ ocaml/, 1996.

[20] Xavier Leroy and Michel Mauny. Dynamics in ML. Journal of Functional Programming, 3(4):431�463, 1993.

[21] Xavier Leroy and Pierre Weis. Manuel de r� ef� erence du langage Caml. Inter � Editions, 1993.

[22] John C. Mitchell. Coercion and type inference. In Eleventh Annual Symposium on Principles Of Programming Languages, 1984.

[23] John C. Mitchell, Furio Honsell, and Kathleen Fisher. A lambda calculus of objects and method specialization. In 1993 IEEE Symposium on Logic in Computer Science, June 1993.

[24] Martin Odersky and Konstantin L� aufer. Putting type annotations to work. In Proceedings of the 23th ACM Conference on Principles of Programming Languages, January 1996.

[25] Atsushi Ohori. Extending ML polymorphism to record structure. Technical Report CSC 90/R24, University of Glasgow, Department of Computer Science, September 1990.

[26] Atsushi Ohori. A polymorphic record calculus and its compilation. ACM Transactions on Programming Languages and Systems, 17(6):844�895, 1996.

[27] Jens Palsberg. Ef�cient type inference of object types. In Ninth Annual IEEE Symposium on Logic in Computer Science, pages 186� 195, Paris, France, July 1994. IEEE Computer Society Press. To appear in Information and Computation.

[28] Benjamin C. Pierce and David N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207�247, April 1994. A preliminary version appeared in Principles of Programming Languages, 1993, and as University of Edinburgh technical report ECS-LFCS-92-225, under the title �Object-Oriented Programming Without Recursive Types�.

[29] Didier R� emy. Extending ML type system with a sorted equational theory. Research Report 1766, Institut National de Recherche en Informatique et Automatisme, BP 105, F-78 153 Le Chesnay Cedex, 1992.

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

[31] Didier R� emy. Programming objects with ML-ART: An extension to ML with abstract and record types. In Masami Hagiya and John C. Mitchell, editors, Theoretical Aspects of Computer Software, volume 789 of Lecture Notes in Computer Science, pages 321�346. Springer-Verlag, April 1994.

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

[33] John H. Reppy and Jon G. Riecke. Classes in Object ML. Presented at the FOOL’3 workshop, July 1996.

[34] John H. Reppy and Jon G. Riecke. Simple objects for Standard ML. In Programming Language Design and Implementation 1996. ACM, may 1996.

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

Appendices

1. Typing rules for core ML

\frac{x : ∀ ᾱ. τ ∈ A}{A ⊢ x : τ[τ̄/ᾱ]}^{(Inst)}  \frac{A + x : τ ⊢ a : τ′}{A ⊢ fun (x) a : τ → τ′}^{(Fun)}

\frac{A ⊢ a : τ′ → τ A ⊢ a′ : τ′}{A ⊢ a a′ : τ}^{(App)}

(Let)

\frac{A ⊢ a′ : τ′ A + x : Gen(τ′, A) ⊢ a : τ}{A ⊢ let x = a′ in a : τ}

Generalization Gen(τ, A) is ∀ ᾱ. τ where ᾱ are all variables of τ that are not free in A.

2. An example of typing derivation

In this section, we give the typing derivation for class scaled point. Our focus here is not to explain type inference, but simply to illustrate the typing rules.

We assume that the class point has already been typed, that is, we type scaled point in the environment A_{0} containing the following class-type (we use #point as an abbreviation for ⟨move : int → int; ..⟩):

int →
sig (#point)
field x : intref
method move : int → int
end

We remind the de�nition of class scaled point:

fun (s_{0})

struct
inheritpoint 0 as parent;
field s = s_{0};

method scale = s;

method move =

fun (d) parent#move(d ∗ self#scale)

end

The remainder of this section is a proof that class scaled point has the following class type (we use #scaled point is an abbreviation for ⟨move : int → int; scale : int; ..⟩):

  int →
      sig (#scaled point)
          field x : int;
          field s : int;
          method move : int → int;
          method scale : int
      end

Let A_{1} for A_{0} extended with s_{0} : int and A_{2} be A_{1} extended with self : #scaled point. The body of the inheritance clause must be typed in A_{2}^{⋆} which is equal to A_{1}. By rule Class-Inst we have:

  A_{1} ⊢ point :
        int →
           sig (#scaled point)
               field x : intref
               method move : int → int
            end

Note that we have chosen an instance of the type of class point where self type is #scaled point (an instance of type #point). Thus, by rule Class-App, we have:

  A_{1} ⊢ point 0 :
        sig (#scaled point)
           field x : intref
           method move : int → int
        end

Applying rule Inherits we get:

  A_{2} ⊢ inheritpoint 0 as parent :
          (field x : int;
          method move : int → int;

super parent :

              (field x : int;
               method move : int → int))  (1)

The rest of the class body must be typed in environment A_{3} equal to A_{2} extended with

  field x : int; super parent :
      (field x : int; method move : int → int)

Since A_{3}^{⋆} is A_{1}, we have A_{3}^{⋆} ⊢ s_{0} : int, and by rule Field,

A_{3} ⊢ field s = s_{0} : field s : int. (2)

The rest of the class body must be typed in A_{4} equal to A_{3} extended with field s : int. Since A_{4} ⊢ s : int, we have by rule Method

A_{4} ⊢ method scale = s : method scale : int. (3)

Using rules Send and Super, we also have A_{4} ⊢ a : int → int where

a =^{def} fun (d) parent#move(d ∗ self#scale)

Thus,

A_{4} ⊢ method move = a : method move : int → int.

By rule Then applied to (3) and the previous judgment, we have

A_{4} ⊢ (method scale = s; method move = a) :

(method scale : int;
method move : int → int)

By rule Then gain, applied to (2) and the previous judgement, we have

A_{3} ⊢ (field s = s_{0}; method scale = s; method move = a) :

(field s : int; method scale : int;
method move : int → int)

Hence, by rule Then again applied to (1) and the previous judgement, we have A_{2} ⊢ b : φ where

b =^{def} (inheritpoint 0 as parent;

field s = s_{0}; method scale = s; method move = a)

φ =^{def} (field x : int; method move : int → int;
field s : int; method scale : int)

Since A_{2} ⊢ self : #scaled point, applying rule Class-Body leads to:

A_{1} ⊢ struct b end : sig (#scaled point) φ end

Finally, by rule Class-Fun, we get:

A_{0} ⊢ fun (s_{0}) struct b end :
int → sig (#scaled point) φ end

3. Binary methods

In Objective ML, it is possible to de�ne binary methods, that is, methods that receive as a parameter an object of the same type as self. Furthermore, a class that has binary methods can be freely extended by inheritance. Of course, binary methods remains binary in a subclass.

The virtual class comparable is a template for classes with a binary method leq. The component virtual leq is a type constraint on the type of self. This method must be applied to an object of the same type as self.

class comparable () = struct virtual (α)

  virtual leq : α → bool
end;;
class comparable : unit → sig virtual (α)
  virtual leq : α → bool
end

Class int comparable inherits from class comparable. It implements method leq and adds a method getx.

class int comparable (x : int) = struct
  inherit comparable ()
  field x = ref x
  method getx = !x
  method leq o = !x ≤ o#getx
end;;
class int comparable : int → sig (α)
  field x : int ref
  method leq : α → bool
  method getx : int
end

Method leq still expects to be applied to an object of the same type as self. So, type int comparable = rec α.⟨leq : α → bool; getx : int⟩ is not a subtype of type comparable = rec α.⟨leq : α → bool⟩: inheritance is not subtyping. Indeed, a method leq of an object of the former type expects to be applied to an object that has a method getx; this is not ensured by the latter type. How-

ever, int comparable is an instance of ρ #comparable,

which is by de�nition rec α.⟨leq : α → bool; ρ⟩. Binary methods are correctly handled since the type of self is kept open while typing classes: adding the method getx to class comparable simply amounts to instantiating the row variable in the type of self, to (getx : int; ..). Thus, the type of self in the subclass has a method getx and is still open.

As a test, the function min will return the minimum of any two objects whose type is an instance of type #comparable.

let min (x : #comparable) y =
  if x#leq y then x else y;;
value min : (#comparable as α) → α → α =
  ⟨fun⟩

This function can thus be applied to objects of type

int comparable.
let p = min (new int comparable  7)
            (new int comparable 11)
in (p, p#getx);;
− : int comparable * int = ⟨obj⟩, 7

4. Proofs of type soundness theorems

Subject reduction is a straightforward combination of redex contraction (lemma 13) and context replacement (lemma 8). Since we have multiple syntactic categories for expressions, contexts, and types, it is convenient to introduce the following

meta-notations:

ǎ ::= a | b | c | d  Ě ::= E | F | E_{c} | F_{d}  τ̌ ::= τ | φ | γ

These meta-letters are used consistently. For instance, when writing A ⊢ ǎ : τ̌, (ǎ, τ̌) means (a, τ), (b, φ), etc, but not (b, τ). The following propositions are used several times in the proof.

Proposition 4 (Stability by substitution) If A ⊢ ǎ : τ̌, then for any substitution θ, θ(A) ⊢ ǎ : θ(τ̌).

Proposition 5 (Extension of environment) If type environments A and B are identical on free variables of expression a and A ⊢ ǎ : τ̌, then B ⊢ ǎ : τ̌. If type environment B extends type environment A (that is B |�dom (A) is A) and A ⊢ ǎ : τ̌, then B ⊢ ǎ : τ̌.

We say that σ is an instance of σ′ if any instance of σ is an instance of σ′. We say that type environment A is an instance of type environment A′ if both type environments have the same domain and for any element h of their domain A(h) is an instance of A′(h).

Proposition 6 (Strengthening of context) If type environment A is an instance of type environment B and A ⊢ a : τ, then B ⊢ a : τ.

The following lemma somewhat simpli�es the proofs.

Lemma 7 (Derivation simpli�cation) When proving that for all τ, A_{0} ⊢ a_{0} : τ implies A ⊢ a : τ (for some A_{0}, a_{0}, A and a), one can restrict oneself to the case where a derivation of A_{0} ⊢ a_{0} : τ does not end with rule Sub. The general case follows.

Proof. This is done by induction on the size of derivations. Let us assume that a derivation of A_{0} ⊢ a_{0} : τ ends as

A_{0} ⊢ a_{0} : τ′ τ′ ≤ τ (Sub)

A_{0} ⊢ a_{0} : τ

By induction hypothesis, A ⊢ a : τ′. Hence

A ⊢ a : τ′ τ′ ≤ τ (Sub)

A ⊢ a : τ

We write a_{1} ⊂ a_{2} if for any environment A such that A^{⋆} = A and any type τ such that A ⊢ a_{1} : τ, A ⊢ a_{2} : τ. Likewise, we write b_{1} ⊂ b_{2} (resp. c_{1} ⊂ c_{2}) if for any environments A and any class body type φ such that A ⊢ b_{1} : φ (resp. any class type γ such that A ⊢ c_{1} : γ), then A ⊢ b_{2} : φ (resp. A ⊢ c_{2} : γ). Subject reduction theorem can be restated as follows: if a_{1} ⟶ a_{2}, then a_{1} ⊂ a_{2}.

Lemma 8 (Context replacement) For any context E, if ǎ_{1} ⊂ ǎ_{2} then E[ǎ_{1}] ⊂ E[ǎ_{2}].

Proof. The property can be proved independently for each arbitrary one-node context Ě. Then, the lemma follows by a trivial induction on the size of the context.

Let Ě be a one-node context. Let A be a type environment and τ̌ a type such that A ⊢ Ě[ǎ_{1}] : τ̌ (1). We show that A ⊢ Ě[ǎ_{2}] : τ̌. Using lemma 7, one can assume that a derivation of (1) does not end with rule Sub.

All cases are simple and similar. We show one case for example:

Case E is let x = [] in a: A derivation of (1) ends as:

A ⊢ a_{1} : τ′ A + x : Gen(τ′, A) ⊢ a : τ (Let)

A ⊢ let x = a_{1} in a : τ

By induction hypothesis applied to the �rst premise, A ⊢ a_{2} : τ′. Hence A ⊢ let x = a_{2} in a : τ

The following lemmas (9 thru 12) are used to simplify the proof of redex contraction.

Lemma 9 (Append) Let A be a typing environment containing no super bindings. If A ⊢ b_{1} : φ_{1}, A + (φ_{1} \ method) ⊢ b_{2} : φ_{2}, and φ_{1} and φ_{2} are compatible (that is, φ_{1} ⊕ φ_{2} is correct), then A ⊢ b_{1} @ b_{2} : φ_{1} ⊕ φ_{2}.

Proof. We actually prove a more general property. Let φ_{0} be a sequence of super bindings. If A + φ_{0} ⊢ b_{1} : φ_{1}, A + (φ_{1} \ method) ⊢ b_{2} : φ_{2}, and φ_{1} and φ_{2} are compatible (that is, φ_{1} ⊕ φ_{2} is correct), then A + φ_{0} ⊢ b_{1} @ b_{2} : φ_{1} ⊕ φ_{2}.

This is easily proved by induction on b_{1}.

Lemma 10 (Term replacement (variables)) Let A be a type environment, ǎ and a′ be term expressions, τ̌ and τ′ be type expressions. If A^{⋆} ⊢ a′ : τ′ (2) and A + x : Gen(τ′, A) ⊢ ǎ : τ̌ (3) and bound variables of ǎ are not free in a′, then A ⊢ ǎ[a′/x] : τ̌ is provable (4).

THEORY AND PRACTICE OF OBJECT SYSTEMS—(1998) 19

Proof. The proof is by induction on the structure of ǎ (i.e. a, c, b and d). Using lemma 7, we can assume that a derivation of (3) does not end with rule Sub.

In each case, we consider a derivation of (3). By using a renaming substitution on (2) if necessary (proposition 4), we can assume that free variables of τ′ that are not in A^{⋆} do not appear free in this derivation (5). We write A_{x} for A+x : Gen(τ′, A^{⋆}).

We only show the more complicated cases. Other cases are either similar or simple.

Case a is let x_{1} = a_{1} in a_{2}: A derivation of (3) ends as:

(6) A_{x} ⊢ a_{1} : τ_{1} A_{x} + x_{1} : Gen(τ_{1}, A_{x}) ⊢ a_{2} : τ (7) (Let)

A_{x} ⊢ let x_{1} = a_{1} in a_{2} : τ

By induction hypothesis applied to (6), we get A ⊢ a_{1}[a′/x] : τ_{1} (8).

If x_{1} = x, (7) becomes A + x : Gen(τ_{1}, A_{x}) ⊢ a_{2} : τ. By strengthening of environment (proposition 6), we have A + x : Gen(τ_{1}, A) ⊢ a_{2} : τ since A is a subsequence of A_{x}. We conclude by rule Let.

Otherwise, let A_{1} be A+x_{1} : Gen(τ_{1}, A). Re-ordering hypotheses in (7), we have A+x_{1} : Gen(τ_{1}, A_{x})+x : Gen(τ′, A) ⊢ a_{2} : τ. By strengthening of environment, we can replace A_{x} by A. Since free type variables of A_{1} are the same as free type variables of A, we can replace A by A_{1} in Gen(τ′, A). Thus, we have A_{1} + x : Gen(τ′, A_{1}) ⊢ a_{2} : τ. On the other hand, since x_{1} is not bound in a′, and A_{1}^{⋆} extends A^{⋆}, we deduce A_{1}^{⋆} ⊢ a′ : τ′ from (2) by extension of environment (proposition 5). Thus, we can apply the induction hypothesis with A_{1} for A. We get A_{1} ⊢ a_{2}[a′/x] : τ. Combining with (8) in a Let rule, we �nally have A ⊢ (let x_{1} = a_{1} in a_{2})[a′/x] : τ.

Case a is fun (x_{1}) a_{2}: A derivation of (3) ends as:

A_{x} + x_{1} : τ_{1} ⊢ a_{2} : τ_{2} (Fun)

A_{x} ⊢ fun (x_{1}) a_{2} : τ_{1} → τ_{2}

Let A_{1} be A + x_{1} : τ_{1}. Re-ordering type environment of the premise, we have A + x_{1} : τ_{1} + x : Gen(τ′, A) ⊢ a_{2} : τ_{2}. By (5), the generalization Gen(τ′, A) is equal to Gen(τ′, A+x_{1} : τ_{1}), that is, Gen(τ′, A_{1}). So, we have A_{1}+x : Gen(τ′, A_{1}) ⊢ a_{2} : τ_{2}. Since x_{1} is not bound in a′ and A_{1}^{⋆} extends A^{⋆} , we deduce A_{1}^{⋆} ⊢ a′ : τ′ from (2). Thus, we can apply the induction hypothesis with A_{1} for A. We get A_{1} ⊢ a_{2}[a′/x] : τ_{2}. We conclude with rule Fun

Case a is ⟨b⟩: A derivation of (3) ends as:

A_{x}^{⋆} + self : τ_{y} ⊢ b : φ τ_{y} = ⟨method (φ)⟩

(Object)

A_{x} ⊢ ⟨b⟩ : τ_{y}

Let A_{y} be A^{⋆} + self : τ_{y}. Re-ordering type environment of the premise, we have A^{⋆} + self : τ_{y} + x : Gen(τ′, A) ⊢ b : φ. We can replace Gen(τ′, A) by Gen(τ′, A^{⋆}) by strengthening of environment. By (5), the generalization Gen(τ′, A^{⋆}) is equal to Gen(τ′, A^{⋆} + self : τ_{y}), that is, Gen(τ′, A_{y}). Thus, we have A_{y} + x : Gen(τ′, A_{y}) ⊢ b : φ. Since A_{y}^{⋆} is just A^{⋆}, we have A_{y}^{⋆} ⊢ a′ : τ′ (3). Thus, we can apply the induction hypothesis with A_{y} for A. We get A_{y} ⊢ b[a′/x] : φ. We conclude with rule Object.

Lemma 11 (Term replacement (instance variables and self)) Let A be an environment and ǎ be either an expression a or a class expression c. Let w be an object body and φ be an object body type. We de�nes U as the restriction of dom (w) to �elds. We write τ_{y} for ⟨method (φ)⟩. We assume that A^{⋆} is A, bound variables of ǎ are not be free in ⟨w⟩ and w(u), and the following three judgments hold:

A + self : τ_{y} ⊢ w : φ,  (A ⊢ w(u) : τ_{u})^{u∈U},  A + self : τ_{y} + (φ \ method) ⊢ ǎ : τ̌(9).

Then, A ⊢ ǎ[⟨w⟩/self][w(u)/u]^{u∈U}[⟨w @ (field u = a_{u}^{u∈V})⟩/{⟨u = a_{u}^{u∈V} ⟩}]^{V ⊂U} : τ̌.

Proof. The proof is by induction on the structure of ǎ. For any expression a, we write a^{+} for

a[⟨w⟩/self][w(u)/u]^{u∈U}[⟨w @ (field u = a_{u}^{u∈V})⟩/{⟨u = a_{u}^{u∈V} ⟩}]^{V ⊂U}

Class expression c^{+} is de�ned likewise. We write A_{y} for A + self : τ_{y} + (φ \ method). Using lemma 7, we can assume that a derivation of (9) does not end with rule Sub.

We only show the more complicated cases. Other cases are easy.

Case a is self: Hypothesis (9) is A + self : τ_{y} + (φ \ method) ⊢ self : τ. So, τ and τ_{y} are equal. On the other hand, a^{+} is equal to ⟨w⟩. We conclude by rule Object:

A + self : τ ⊢ w : φ τ = ⟨method (φ)⟩

(Object)

A ⊢ ⟨w⟩ : τ

Case a is {⟨u = a_{u}^{u∈V} ⟩}: A derivation of (9) ends as:

((10) field u : τ_{u} ∈ A_{y} (11) A_{y} ⊢ a_{u} : τ_{u})^{u∈V}

(Override)

A_{y} ⊢ {⟨u : a_{u}^{u∈V} ⟩} : τ_{y}

So, from (10), φ ⊕ field u : τ_{u}^{u∈V} = φ. By induction hypothesis applied to (11), we get A ⊢ a_{u}^{+} : τ_{u} (12). Hence A ⊢ (field u = a_{u}^{+})^{u∈V} : (field u : τ_{u})^{u∈V}. Then, the append lemma 9 applied to the hypothesis A + self : τ_{y} ⊢ w : φ and the last judgment yields A + self : τ_{y} ⊢ w @ (field u = a_{u}^{+})^{u∈V} : φ. Hence the following derivation :

A + self : τ_{y} ⊢ w @ (field u = a_{u}^{+})^{u∈V} : φ τ_{y} = ⟨method (φ)⟩

(Object)

A ⊢ ⟨w @ (field u = a_{u}^{+})^{u∈V} ⟩ : τ_{y}

Lemma 12 (Term replacement (super)) If A ⊢ b_{1} : φ_{1}, A + super: φ ⊢ b_{2} : φ_{2} and bound variables of b_{2} are not free in b_{1}, then A ⊢ b′_{2} : φ_{2} where b′_{2} is [a/s#m]^{methodm=a∈b_{1}}, i.e. b_{2} where all invocations of methods to super s#m have been replaced by the body a of the corresponding method m in b_{1}.

Proof. The proof is similar to the one of lemma 10. It is in fact simpler, as super is not substituted across class and object boundaries, nor across instance variable de�nitions.

Lemma 13 (Redex contraction) We write ⟶_{ϵ} for a one-step reduction in an empty context. If ǎ_{1} ⟶_{ϵ} ǎ_{2} then ǎ_{1} ⊂ ǎ_{2}.

Proof. The proof is done independently for each redex. All cases are easy now that we have proven the right lemmas. Let us assume A ⊢ a_{1} : τ (13) and A equals A^{⋆} (resp. A ⊢ b_{1} : φ (14) for any A). We show that A ⊢ a_{2} : τ (15) (resp.

A ⊢ b_{2} : φ) by cases on the redex a_{1} (resp. b_{1}). Each case is shown independently. Using lemma 7, we can assume that a derivation of (13) does not end with rule Sub.

Case a_{1} is (fun (x) a) v: A derivation of (13) ends either as:

\begin{aligned}A + x : τ′ ⊢ a : τ_{0} \\ & (Fun) \\ A ⊢ fun (x) a : τ′ → τ_{0} \end{aligned}  τ′ → τ_{0} ≤ τ′_{0} → τ (Sub) A ⊢ fun (x) a : τ′_{0} → τ  A ⊢ v : τ′_{0} (App)
A ⊢ (fun (x) a) v : τ

or as:

\begin{aligned}(16) A + x : τ′ ⊢ a : τ \\ & (Fun) \\ A ⊢ fun (x) a : τ′ → τ \end{aligned} (17) A ⊢ v : τ′ (App)

A ⊢ (fun (x) a) v : τ

The end of the �rst derivation can be rewritten as:

A + x : τ′ ⊢ a : τ_{0} τ_{0} ≤ τ \overline{(Sub)}

(16) A + x : τ′ ⊢ a : τ (Fun)

A ⊢ fun (x) a : τ′ → τ

A ⊢ v : τ′_{0} τ′_{0} ≤ τ′ ; \overline{(Sub)} ; (17) A ⊢ v : τ′

(App)

A ⊢ (fun (x) a) v : τ

In both cases, the term replacement lemma 10 applied to (17) and (16) shows the conclusion.

Case c_{1} is (fun (x) c) v: Similar to previous case.

Case a_{1} is let x = v in a: A derivation of (13) ends as

(18) A ⊢ v : τ′ (19) A + x : Gen(τ′, A) ⊢ a : τ (Let)

A ⊢ let x = v in a : τ

The term replacement lemma 10 applied to (18) and (19) shows the conclusion.

Case a_{1} is class z = v in a: Similar to previous case.

Case a_{1} is new (struct w end): A derivation of (13) ends as

A^{⋆} + self : τ_{y} ⊢ w : φ \overline{(Class-Body)} A ⊢ struct w end : sig (τ_{y}) φ end τ_{y} = ⟨method (φ)⟩

(New)

                            (20) A ⊢ new (struct w end) : τ_{y}

Hence,

A^{⋆} + self : τ_{y} ⊢ w : φ τ_{y} = ⟨method (φ)⟩

(Object)

A ⊢ ⟨w⟩ : τ_{y}

Case a_{1} is ⟨w⟩#m: We must remember that A^{⋆} is A. A derivation of (13) ends either as

A + self : τ_{y} ⊢ w : φ  τ_{y} = ⟨method (φ)⟩ (Object) A ⊢ ⟨w⟩ : τ_{y}  τ_{y} ≤ τ_{y}′ (Sub) A ⊢ ⟨w⟩ : τ_{y}′  τ_{y}′ = ⟨m : τ′_{k}; τ′⟩ (Send)
A ⊢ ⟨w⟩#m : τ′_{k}

or as

(21) A + self : τ_{y} ⊢ w : φ  (22) τ_{y} = ⟨method (φ)⟩ (Object) A ⊢ ⟨w⟩ : τ_{y}  (23) τ_{y} = ⟨m : τ_{k}; τ⟩

(Send)

A ⊢ ⟨w⟩#m : τ_{k}

The end of the �rst derivation can be rewritten

A + self : τ_{y} ⊢ w : φ  τ_{y} = ⟨method (φ)⟩ (Object) A ⊢ ⟨w⟩ : τ_{y}  τ_{y} = ⟨m : τ_{k}; τ⟩ (Send) A ⊢ ⟨w⟩#m : τ_{k}  τ_{k} ≤ τ′_{k}

(Sub)

A ⊢ ⟨w⟩#m : τ′_{k}

It has been seen at the beginning of the proof that rule Sub at the end of a derivation could be ignored. Thus, only the second case need to be considered.

The result is then proved using the term replacement lemma 11.

We �rst show that the hypotheses of lemma 11 are satis�ed. As the �elds of an object are typed in the same environment as the object, for field u : τ_{u} ∈ φ, A ⊢ v_{u} : τ_{u} (24) where field u = v_{u} ∈ w. From (22) and (23), method m : τ_{k} ∈ φ. Then, from (21), an easy induction on w using rules Then, Field, and Method yields:

A + self : τ_{y} + φ_{1} ⊢ w(m) : τ_{k} for some φ_{1} ⊂ (φ \ method)

As A contains no field bindings, the environment can be extended to include φ \ method:

(25) A + self : τ_{y} + (φ \ method) ⊢ w(m) : τ_{k}

Finally, the term replacement lemma 11 applied to (21), (24), (25) yields

A ⊢ w(m)[⟨w⟩/self][w(u)/u]^{u∈U}[⟨w @ (field u = a_{u}^{u∈V})⟩/{⟨u = a_{u}^{u∈V} ⟩}]^{V ⊂U} : τ_{k}

Case b_{1} is inherit (struct w end) as s; b: A derivation of (14) ends as

⋮

              A ⊢ inherit (struct w end) as s : φ  (26) A + (φ \ method) ⊢ b : φ_{2}

(Then)

                         A ⊢ inherit (struct w end) as s; b : φ_{1} ⊕ φ_{2}

where φ = φ_{1} + (super s : φ_{1}), continued by

(27) A ⊢ self : τ_{y}  (28) A^{⋆} + self : τ_{y} ⊢ w : φ_{1} \overline{(Class-Body)} A ⊢ struct w end : sig (τ_{y}) φ_{1} end

(Inherit)

                    A ⊢ inherit (struct w end) as s : φ_{1} + (super s : φ_{1})

According to (27), self : τ_{y} ∈ A. Judgment (28) can thus be rewritten A ⊢ w : φ_{1} (29).

Applying the term replacement lemma 12 on A + (φ_{1} \ method) ⊢ w : φ_{1} (the environment has been extended) and (26) yields A + (φ_{1} \ method) ⊢ b[a/s#m]^{methodm=a∈w} : φ_{2}. Then, the append lemma applied on (29) and this last judgment gives the result:

A ⊢ w @ b[a/s#m]^{methodm=a∈w} : φ_{1} ⊕ φ_{2}

Case b_{1} is field u = v ; b: A derivation of (14) ends as

A^{⋆} ⊢ v : τ (Field) A ⊢ field u = v : (field u : τ) (30) A + (field u : τ) ⊢ w : φ

(Then)

A ⊢ field u = v ; w : φ ⊕ (field u : τ)

From (30), since u ∈ dom (w) and �elds appear before methods in w, an easy induction shows that A ⊢ w : φ. Indeed, �elds are typed in environment A^{⋆}, and methods are typed in an environment in which (field u : τ) has been added anyway after the typing of the �eld u appearing in w.

Case b_{1} is method m = a; b: A derivation of (14) ends as

A ⊢ self : ⟨m : τ; τ′⟩  A ⊢ a : τ (Method) A ⊢ method m = a : (method m : τ)  (31) A ⊢ w : φ

(Then)

A ⊢ method m = a; w : (method m : τ) ⊕ φ

Since m ∈ dom (w), m ∈ dom (φ), then φ and (method m : τ) ⊕ φ are equal. Therefore, judgment (31) can be rewritten A ⊢ w : (method m : τ) ⊕ φ.

Case a_{1} is (v : τ <: τ′): A derivation of (13) ends as

A ⊢ v : θ(τ) τ ≤ τ′ (Coerce)

A ⊢ (v : τ <: τ′) : θ(τ′)

Hence,

A ⊢ v : θ(τ) θ(τ) ≤ θ(τ′) (Sub)

A ⊢ v : θ(τ′)

The normal-form theorem is proved by structural induction on values, using the following lemma.

Lemma 14 Let v be a value. We assume ∅ ⊢ v : τ (32).

• If τ is a functional type, then v is a function.

• If τ is an object type, then v is an object.

Let v_{c} be a value. We assume ∅ ⊢ v_{c} : γ.

• If γ is a functional type, then v is a function.

• Otherwise, v is an object.

Proof. We prove that if v is a function, then τ is a functional type and that if v is an object, then τ is an object type. Then, since a value is either a function or an object and functional types and object types are incompatible, this proves the lemma.

We can ignore rule Sub at the end of a derivation, as it does not change the shape of a type.

Case a is fun (x) a_{1}: A derivation of (32) ends as

A + x : τ_{1} ⊢ a_{1} : τ_{2} (Fun)

A ⊢ fun (x) a_{1} : τ_{1} → τ_{2}

So, τ is τ_{1} → τ_{2}.

Case a is ⟨w⟩: A derivation of (32) ends as

A^{⋆} + self : τ_{y} ⊢ w : φ τ_{y} = ⟨method (φ)⟩

(Object)

A ⊢ ⟨w⟩ : τ_{y}

So, τ is ⟨method (φ)⟩.

The proof is similar for class values.

Theorem 2 (Normal forms) Well-typed irreducible normal forms are values (i.e. if ∅ ⊢ a : τ and a cannot be reduced, then a is a value.)

Proof. The proof is by structural induction simultaneously on expressions a and class bodies b. Let us assume ∅ ⊢ a : τ (33) (resp. ∅ ⊢ c : γ (34), A ⊢ b : φ (35) or A ⊢ d : φ, where A contains only field and method bindings), and that a (resp. c, b or d) cannot be reduced. Case a is x: This expression cannot be typed in the empty environment. Case a is a_{1} a_{2}: It is not possible. A derivation of (33) shows that there exists a type τ_{1} such that ∅ ⊢ a_{1} : τ_{1} → τ. The induction hypothesis applied to expression a_{1} shows that it is a value. Since it has a functional type, it must be a function fun (x) a_{0}. But then expression a could be reduced. Case a is let x = a_{1} in a_{2}: It is not possible. The induction hypothesis applied to expression a_{1} shows that it is a value. But then expression a could be reduced. Case a is a_{1}#m or class z = c in a_{1}: Similar to previous cases. Case a is fun (x) a_{1}: By de�nition, expression a is a value. Case a is s#m: It is not possible : expression s#m is not typable in the empty environment. Case a is self or u or {⟨u = a_{u}^{u∈V} ⟩}: Same as previous case. Case a is (a_{1} : τ <: τ′): It is not possible: a can be reduced. Case a is ⟨b⟩: The induction hypothesis shows that object body b is a value. Then, expression a is also a value. Case a is new c: It is not possible. A derivation of (33) shows that ∅ ⊢ c : sig (τ_{y}) φ end. The induction hypothesis applied to c shows that it is a value. According to its type, it is a structure. But then a can be reduced Case c is z: This expression is not typable in the empty environment. Case c is c_{1} a: It is not possible. A derivation of (34) shows that there exists a type τ such that ∅ ⊢ c_{1} : τ → γ. The induction hypothesis applied to expression c_{1} shows that it is a class value. Since it has a functional type, it must be a function fun (x) c_{0}. But then expression c could be reduced. Case c is fun (x) c_{1}: By de�nition, expression c is a value. Case c is struct b end: The induction hypothesis shows that class body b is a value. Then, expression c is also a value. Case b is d; b_{1}: The induction hypothesis shows that object component d and object body b_{1} are in normal forms. d is thus a �eld or method de�nition, and it is not overridden by b_{1} (otherwise, b could be reduced.) Case b is ∅: By de�nition, object body b is a value. Case d is inherit c as s: It is not possible. A derivation of (35) ends as:

A ⊢ self : τ_{y} (36) A ⊢ c : sig (τ_{y}) φ_{1} end

(Inherit)

                          A ⊢ inherit c as s : φ_{1} + (super s : φ_{1})

The induction hypothesis applied to c shows that it is a class value. According to its type, it is of the form struct w end. But then, the inheritance clause could be reduced. Case d is method m = a: By de�nition, expression d is in normal form. Case d is field u = a: If A ⊢ d : field u : τ, then ∅ ⊢ a : τ, as A contains only field and method bindings. By induction hypothesis, expression a is in normal form. Then, so is object component d.