Previous Up Next

Chapter 3  The object layer

We first introduce objects and classes, informally. Then, we present the core of the object layer, leaving out some of the details. Last, we show a few advanced uses of objects.

3.1  Discovering objects and classes

In this section, we start with a series of very basic examples, and present the key features common to all object oriented languages; then we introduce polymorphism, which play an important role in OCaml.

Object, classes, and types.

There is a clear distinction to be emphasized between objects, classes, and types. Objects are values which are returned by evaluation and that can be sent as arguments to functions. Objects only differ from other values by the way to interact with them, that is to send them messages, or in other words, to invoke their methods.

Classes are not objects, but definitions for building objects. Classes can themselves be built from scratch or from other classes by inheritance. Objects are usually created from classes by instantiation (with the new construct) but can also be created from other objects by cloning or overriding.

Neither classes nor objects are types. Object have object types, which are regular types, similar to but different from arrow or product types. Classes also have types. However, class types are not regular types, as much as classes are not regular expressions, but expressions of a small class language.

Classes may be in an inheritance (sub-classing) relation, which is the case when a class inherits from another one. Object types may be in a subtyping relation. However, there is no correspondence to be made between sub-classing and subtyping, anyway.

3.1.1  Basic examples

A class is a model for objects. For instance, a class counter can be defined as follows.

class counter = object val mutable n = 0 method incr = n <- n+1 method get = n end;;

That is, objects of the class counter have a mutable field n and two methods incr and get. The field n is used to record the current value of the counter and is initialized to 0. The two methods are used to increment the counter and read its current, respectively.

As for any other declaration, the OCaml system infer a principal type for this declaration:

class counter : object val mutable n : int method get : int method incr : unit end

The class type inferred mimics the declaration of the class: it describes the types of each field and each method of the class.

An object is created from a class by taking an instance using the new construct:

let c = new counter;;
val c : counter = <obj>

Then, methods of the object can be invoked —this is actually the only form of interaction with objects.

c#incr; c#incr; c#get;;
- : int = 2

Note the use of # for method invocation. The expression c.incr would assume that c is a record value with an incr field, and thus fail here.

Fields are encapsulated, and are accessible only via methods. Two instances of the same class produce different objects with different encapsulated state. The field n is not at all a class-variable that would be shared between all instances. On the contrary, it is created when taking an instance of the class, independently of other objects of the same class.

(new counter)#get;;
- : int = 0

Note that the generic equality (the infix operator =) will always distinguish two different objects even when they are of the same class and when their fields have identical values:

(new counter) = (new counter);;
- : bool = false

Objects have their own identity and are never compared by structure.


Classes are often used to encapsulate a piece of state with methods. However, they can also be used, without any field, just as a way of grouping related methods:

class out = object method char x = print_char x method string x = print_string x end;;

A similar class with a richer interface and a different behavior:

class fileout filename = object val chan = open_out filename method char x = output_char chan x method string x = output_string chan x method seek x = seek_out chan x end;;

This favors the so-called “programming by messages” paradigm:

let stdout = new out and log = new fileout "log";; let echo_char c = stdout#char c; log#char c;;

Two objects may answer the same message differently, by running their own methods, ie. depending on their classes.


Classes are used not only to create objects, but also to create richer classes by inheritance. For instance, the fileout class can be enriched with a method to close the output channel:

class fileout' filename = object (self) inherit fileout filename method close = close_out chan end

It is also possible to define a class for the sole purpose of building other classes by inheritance. For instance, we may define a class of writer as follows:

class virtual writer = object (this) method virtual char : char -> unit method string s = for i = 0 to String.length s -1 do this#char s.[i] done method int i = this#string (string_of_int i) end;;

The class writer refers to other methods of the same class by sending messages to the variable this that will be bound dynamically to the object running the method. The class is flagged virtual because it refers to the method char that is not currently defined. As a result, it cannot be instantiated into an object, but only inherited. The method char is virtual, and it will remain virtual in subclasses until it is defined. For instance, the class fileout could have been defined as an extension of the class writer.

class fileout filename = object inherit writer method char x = output_char chan x method seek pos = seek_out pos end
Late binding

During inheritance, some methods of the parent class may be redefined. Late binding refers to the property that the most recent definition of a method will be taken from the class at the time of object creation. For instance, another more efficient definition of the class fileout would ignore the default definition of the method string for writers and use the direct, faster implementation:

class fileout filename = object inherit writer method char x = output_char chan x method string x = output_string chan x method seek pos = seek_out pos end

Here the method int will call the new efficient definition of method string rather than the default one (as an early binding strategy would do). Late binding is an essential aspect of object orientation. However, it is also a source of difficulties.

Type abbreviations

The definition of a class simultaneously defines a type abbreviation for the type of the objects of that class. For instance, when defining the objects out and log above, the system answers were:

val stdout : out = <obj> val log : fileout = <obj>

Remember that the types out and fileout are only abbreviations. Object types are structural, ie. one can always see their exact structure by expanding abbreviations at will:

(stdout : < char : char -> unit; string : string -> unit >);;
- : out = <obj>

(Abbreviations have stronger priority than other type expressions and are kept even after they have been expanded if possible.) On the other hand, the following type constraint fails because the type fileout of log contains an additional method seek.

(log : < char : char -> unit; string : string -> unit >);;

3.1.2  Polymorphism, subtyping, and parametric classes


play an important role in the object layer. Types of objects such as out, fileout or

<char : char -> unitstringstring -> unit >

are said to be closed. A closed type exhaustively enumerates the set of accessible methods of an object of this types. On the opposite, an open object type only specify a subset of accessible methods. For instance, consider the following function:

let send_char x = x#char;;
val send_char : < char : 'a; .. > -> 'a = <fun>

The domain of send_char is an object having at least a method char of type 'a. The ellipsis .. means that the object received as argument may also have additional methods. In fact, the ellipsis stands for an anonymous row variable, that is, the corresponding type is polymorphic (not only in 'a but also in ..). It is actually a key point that the function send_char is polymorphic, so that it can be applied to any object having a char method. For instance, it can be applied to both stdout or log, which are of different types:

let echo c = send_char stdout c; send_char log c;;

Of course, this would fail without polymorphism, as illustrated below:

(fun m -> m stdout c; m log c) send_char;;

In most object-oriented languages, an object with a larger interface may be used in place of an object with a smaller one. This property, called subtyping, would then allow log to be used with type out, eg. in place of stdout. This is also possible in OCaml, but the use of subtyping must be indicated explicitly. For instance, to put together stdout and log in a same homogeneous data-structure such as a list, log can be coerced to the typed stdout:

let channels = [stdout; (log : fileout :> out)];;
val channels : out list = [<obj>; <obj>]
let braodcast m = List.iter (fun x -> x#string m) channels;;

The domain of subtyping coercions may often (but not always) be omitted; this is the case here and we can simply write:

let channels = [stdout; (log :> out)];;

In fact, the need for subtyping is not too frequent in OCaml, because polymorphism can often advantageously be used instead, in particular, for polymorphic method invocation. Note that reverse coercions from a supertype to a supertype are never possible in OCaml.

Parametric classes

Polymorphism also plays an important role in parametric classes. Parametric classes are the counterpart of polymorphic data structures such as lists, sets, etc. in object-oriented style. For instance, a class of stacks can be parametric in the type of its elements:

class ['a] stack = object val mutable p : 'a list = [] method push v = p <- v :: p method pop = match p with h :: t -> p <- t; h | [] -> failwith "Empty" end;;

The system infers the following polymorphic type.

class ['a] stack : object val mutable p : 'a list method pop : 'a method push : 'a -> unit end

The parameter must always be introduced explicitly (and used inside the class) when defining parametric classes. Indeed, a parametric class does not only define the code of the class, but also defines a type abbreviation for objects of this class. So this constraint is analogous to the fact that type variables free in the definition of a type abbreviation should be bound in the parameters of this abbreviation.

Parametric classes are quite useful when defining general purpose classes. For instance, the following class can be used to maintain a list of subscribers and relay messages to be sent all subscribers via the message send.

class ['a] relay = object val mutable l : 'a list = [] method add x = if not (List.mem x l) then l <- x::l method remove x = l <- List.filter (fun y -> x <> y) l method send m = List.iter m l end;;

While parametric classes are polymorphic, objects of parametric classes are not. The creation of an instance of a class new c must be compared with the creation of a reference ref a. Indeed, the creation of an object may also create mutable fields, and therefore it cannot safely be polymorphic. (Even if the class types does not show any mutable fields, they might have just been hidden from a parent class.)

The type of self

Another important feature of OCaml is its ability to precisely relate the types of two objects without knowing their exact shape. For instance, consider the library function that returns a shallow copy (a clone) of any object given as argument:

Oo.copy : (< .. > as 'a) -> 'a

Firstly, this type indicates that the argument must be an object; we can recognize the anonymous row variable “..”, which stands for “any other methods”; secondly, it indicates that whatever the particular shape of the argument is, the result type remains exactly the same as the argument type. This type of Oo.copy is polymorphic, the types fileout -> fileout, <gnu : int> -> <gnu : int>, or < > -> < > being some example of instances. On the opposite, int -> int is not a correct type for Oo.copy.

Copying may also be internalized as a particular method of a class:

class copy = object (self) method copy = Oo.copy self end;;
class copy : object ('a) method copy : 'a end

The type 'a of self, which is put in parentheses, is called self-type. The class type of the class copy indicates that the class copy has a method copy and that this method returns an object with of self-type. Moreover, this property will remain true in any subclass of copy, where self-type will usually become a specialized version of the the self-type of the parent class.

This is made possible by keeping self-type an open type and the class polymorphic in self-type. On the contrary, the type of the objects of a class is always closed. It is actually an instance of the self-type of its class. More generally, for any class C, the type of objects of a subclass of C is an instance of the self-type of class C.

Exercise 23 ((*) Self types)   Explain the differences between the following two classes:
class c1 = object (self) method c = Oo.copy self end class c2 = object (self) method c = new c2 end;;
Exercise 24 ((**) Backups)   Define a class backup with two methods save and restore, so that when inherited in an (almost) arbitrary class the method save will backup the internal state, and the method restore will return the object in its state at the last backup.

There is a functional counterpart to the primitive Oo.copy that avoids the use of mutable fields. The construct {<  >} returns a copy of self; thus, it can only be used internally, in the definition of classes. However, it has the advantage of permitting to change the values of fields while doing the copy. Below is a functional version of backups introduced in the exercise 24 (with a different interface).

class original = object (self) val original = None method copy = {< original = Some self >} method restore = match original with None -> self | Some x -> x end;;

Here, the method copy, which replaces the method save of the imperative version, returns a copy of self in which the original version has been stored unchanged. Remark that the field original does not have to be mutable.

Exercise 25 ((***) Logarithmic Backups)   Write a variant of either the class backup or original that keeps all intermediate backups.

Add a method clean that selectively remove some of the intermediate backups. For instance, keeping only versions of age 20, 21, ... 2n.

Binary methods

We end this series of examples with the well-known problem of binary methods. These are methods that take as argument an object (or a value containing an object) of the same type as the type of self. Inheriting from such classes in often a problem. However, this difficulty is unnoticeable in OCaml as a result of the expressive treatment of self types and the use of polymorphism.

As an example, let us consider two players: an amateur and a professional. Let us first introduce the amateur player.

class amateur = object (self) method play x risk = if risk > 0 then x else self end;;

The professional player inherits from the amateur, as one could expect. In addition, the professional player is assigned a certain level depending on his past scores. When a professional player plays against another player, he imposes himself a penalty so as to compensate for the difference of levels with his partner.

class professional k = object (self) inherit amateur as super method level = k method play x risk = super#play x (risk + self#level - x#level) end;;

The class professional is well-typed and behaves as expected.

However, a professional player cannot be considered as an amateur player, even though he has more methods. Otherwise, a professional could play with an amateur and ask for the amateur's level, which an amateur would not like, since he does not have any level information.

This is a common pattern with binary methods: as the binary method of a class C expects an argument of self-type, ie. of type the type of objects of class C, an object of a super-class C' of C does not usually have is an interface rich enough to be accepted by the method of C.

An object of a class with a binary method has a recursive type where recursion appears at least once in a contravariant position (this actually is a more accurate, albeit technical definition of binary methods).

class amateur : object ('a) method play : 'a -> int -> 'a end class professional : object ('a) method level : int method play : 'a -> int -> 'a end

As a result of this contravariant occurrence of recursion, the type of an object that exposes a binary method does not possess any subtype but itself. For example, professional is not a subtype of amateur, even though it has more methods. Conversely, level : int > is a correct subtype for an object of the class professional that does not expose its binary method; thus, this type has non-trivial subtypes, such as amateur or professional.

Exercise 26 ((**) Object-oriented strings)   Define a class string that embeds most important operations on strings in a class.

Extend the previous definition with a method concat.


3.2  Understanding objects and classes

In this section, we formalize the core of the object layer of OCaml. In this presentation, we make a few simplifications that slightly decrease the expressiveness of objects and classes, but retain all of their interesting facets.

One of the main restrictions is to consider fields immutable. Indeed, mutable fields are important in practice, but imperative features are rather orthogonal to object-oriented mechanisms. Imperative objects are well explained as the combination of functional objects with references: mutable fields can usually be replaced by immutable fields whose content is a reference. There is a lost though, which we will discuss below. Thus we shall still describe mutable fields, including their typechecking, but we will only describe their semantics informally.

As was already shown in the informal presentation of objects and classes, polymorphism is really a key to the expressiveness of OCaml's objects and classes. In particular, it is essential that:

Besides increasing expressiveness, polymorphism also plays an important role for type inference: it allows to send messages to objects of unknown classes, and in particular, without having to determine the class they belong to. This is permitted by the use of structural object types and row variables. Structural types mean that the structure of types is always transparent and cannot be hidden by opaque names. (We also say that object-types have structural equality, as opposed to by-name equality of data-types.) Of course, objects are “first class” entities: they can be parameters of functions, passed as arguments or return as results.

On the contrary, classes are “second class” entities: they cannot be parameters of other expressions. Hence, only existing classes, ie. of known class types can be inherited or instantiated into objects. As a result, type reconstruction for classes does not require much more machinery than type inference for components of classes, that is, roughly, than type inference for expressions of the core language.

Syntax for objects and classes

We assume three sets uF of field names, mM of method names, and zZ of class names.

Figure 3.1: Syntax for objects and classes
a ::= … ∣ new  a ∣ a#m ∣  class z = d  in  a
Class expressions
d ::= 
 object B end

 z ∣ λ xd ∣ d  a

abstraction and instantiation
Class bodies
B ::= ∅ ∣  B  inherit  d ∣  B  
 u = a

 ∣  B  
 m = ς(x)  a


To take objects and classes into account, the syntax of the core language is extended as described in fig 3.1. Class bodies are either new classes, written object B end, or expressions of a small calculus of classes that including class variables, abstraction (over regular values —not classes), and application of classes to values.

A minor difference with OCaml is we chose to bind self in each method rather than once for all at the beginning of each class body. Methods are thus of the form ς(xm where x is a binder for self. Of course, we can always see the OCaml expression object (xu = a; m1 = a1; m2 = a1 end as syntactic sugar for object u = a; m1 = ς(xa1; m2 = ς(xa1 end. Indeed, the latter is easier to manipulate formally, while the former is shorter and more readable in programs.

As suggested above, type-checking objects and classes are orthogonal, and rely on different aspects of the design. We consider them separately in two different sections.

3.2.1  Type-checking objects

The successful type-checking of objects results from a careful combination of the following features: structural object types, row variables, recursive types, and type abbreviations. Structural types and row polymorphism allow polymorphic invocation of messages. The need for recursive types arise from the structural treatment of types, since object types are recursive in essence (objects often refer to themselves). Another consequence of structural types is that the types of objects tend to be very large. Indeed, they describe the types of all accessible methods, which themselves are often functions between objects with large types. Hence, a smart type abbreviation mechanism is used to keep types relatively small and their representation compact. Type abbreviations are not required in theory, but they are crucial in practice, both for smooth interaction with the user and for reasonable efficiency of type inference. Furthermore, observing that some forms of object types are never inferred allows to keep all row variables anonymous, which significantly simplifies the presentation of object types to the user.

Object types

Intuitively, an object type is composed of the row of all visible methods with their types (for closed object types), and optionally ends with a row variable (for open object types). However, this presentation is not very modular. In particular, replacing row variables by a row would not yield a well-formed type. Instead, we define types in two steps. Assuming a countable collection of row variables η ∈ R, raw types and rows are described by the following grammars:

τ ::= … ∣ ⟨ρ⟩     ρ ::= 0 ∣ η ∣ m : τ; ρ

This prohibits row variables to be used anywhere else but at the end of an object type. Still, some raw types do not make sense, and should be rejected. For instance, a row with a repeated label such as (m : τ; m : τ'; ρ) should be rejected as ill-formed. Other types such as ⟨m : τ; ρ⟩ → ⟨ρ⟩ should also be ruled out since replacing ρ by m : τ'; ρ would produce an ill-formed type. Indeed, well-formedness should be preserved by well-formed substitutions. A modular criteria is to sort raw types by assigning to each row a set of labels that it should not define, and by assigning to a toplevel row ρ (one appearing immediately under the type constructor ⟨ · ⟩) the sort ∅.

Then, types are the set of well-sorted raw types. Furthermore, rows are considered modulo left commutation of fields. That is, m : τ; (m' : τ'; ρ) is equal to m' : τ'; (m : τ; ρ). For notational convenience, we assume that (m : _; _) binds tighter to the right, so we simply write (m : τ; m' : τ'; ρ).

Remark 6   Object types are actually similar to types for (non-extensible) polymorphic records: polymorphic record access corresponds to message invocation; polymorphic record extension is not needed here, since OCaml class-based objects are not extensible. Hence, some simpler kinded approach to record types can also be used [57]. (See end of Chapter 2, page ?? for more references on polymorphic records.)
Message invocation

Typing message invocation can be described by the following typing rule:

A ⊢ a : ⟨m : τ; ρ⟩
A ⊢ a#m : τ

That is, if an expression a is an object with a method m of type τ and maybe other methods (captured by the row ρ), then the expression a#m is well-typed and has type τ.

However, instead of rule Message, we prefer to treat message invocation (a#m) as the application of a primitive (_#m) to the expression a. Thus, we assume that the initial environment contains the collection of assumptions ((_.m) : ∀ α, η.  ⟨m : α; η⟩ → α)mM. We so take advantage of the parameterization of the language by primitives and avoid the introduction of new typing rules.

Type inference for object types

Since we have not changed the set of expressions, the problem of type inference (for message invocation) reduces to solving unification problems, as before. However, types are now richer and include object types and rows. So type inference reduces to unification with those richer types.

The constraint that object types must be well-sorted significantly limits the application of left-commutativity equations and, as a result, solvable unification problems possess principal solutions. Furthermore, the unification algorithm for types with object-types can be obtained by a simple modification of the algorithm for simple types.

Figure 3.2: Unification for object types

Use rules of table 1.5 where Fail excludes pairs composed of two symbols of the form (m : _; _). and add the following rule:
Mute   if m1m2 and α ∉ {α1, α2} ∪ ftv(e)
(m1 : α1; η1) =  (m2 : α2; η2) = e
∃ η.   (m1 : α1m2 : α2; η) = e ∧ η1 = (m2 : α2; η) ∧ η2 = (m1 : α1; η) 
Exercise 27 ((**) Object types)   Check that the rewriting rules preserves the sorts.
Anonymous row variables

In fact, OCaml uses yet another restriction on types, which is not mandatory but quite convenient in practice, since it avoids showing row variables to the user. This restriction is global: in any unificand we forces any two rows ending with the same row variable to be equal. Such unificands can always may be written as

U  ∧  i∈ I  
∃ ηi.  ⟨mi : τi; ηi⟩ = ei

where U, all τi's and ei's do not contain any row variable. In such a case, we may abbreviate ∃ ηi.  ⟨mi : τi; ηi⟩ = ei as ⟨mi : τi; 1⟩ = e, using an anonymous row variable 1 instead of η.

It is important to note that the property can always be preserved during simplification of unification problems.

Exercise 28 ((**) Unification for object types)   Give simplification rules for restricted unification problems that maintain the problem in a restricted form (using anonymous row variables).

An alternative presentation of anonymous row variables is to use kinded types instead: The equation α = ⟨m : τ; 1⟩ can be replaced by a kind constraint α :: ⟨m : τ; 1⟩ (then α = ⟨m : τ; 0⟩ is also replaced by α :: ⟨m : τ; 0⟩).

Recursive types

Object types may be recursive. Recursive types appear with classes that return self or that possess binary methods; they also often arise with the combination of objects that can call one another. Unquestionably, recursive types are important.

In fact, recursive types do not raise any problem at all. Without object types, ie. in ML, types are terms of a free algebra, and unification with infinite terms for free algebras is well-known: deleting rule Cycle from the rewriting rules of figure 1.5 provides a unification algorithm for recursive simple types.

However, in the presence of object types, types are no longer the terms of a free algebra, since row are considered modulo left-commutativity axioms. Usually, axioms do not mix well with recursive types (in general, pathological solutions appear, and principal unifiers may be lost.) Unrestricted left-commutativity axiom is itself problematic. Fortunately, the restriction of object types by sort constraints, which limits the use of left-commutativity, makes objects-types behave well with recursive types.

More precisely, object-types can be extended with infinite terms exactly as simple types. Furthermore, a unification algorithm for recursive object types can be obtained by removing the Cycle rule from the rewriting rules of both figures 1.5 and 3.2.

Remark 7   Allowing recursive types preserves type-soundness. However, it often turns programmers' simple mistakes, such as the omission of an argument, into well-typed programs with unexpected recursive types. (All terms of the λ-calculus —without constants— are well-typed with recursive types.) Such errors may be left undetected, or only detected at a very late stage, unless the programmer carefully check the inferred types.

Recursive types may be restricted, eg. such that any recursive path crosses at least an object type constructor. Such a restriction may seem arbitrary, but it is usually preferable in practice to no restriction at all.

Type sharing

Finite types are commonly represented as trees. Recursive types, ie. infinite regular trees, can be represented in several ways. The standard notation µ θ. τ can be used to represent the infinitely unfolded tree τ [θ ← τ [θ ← …]]. Alternatively, a regular tree can also be represented as a pair τ ∣ U of a term and a set of equations in canonical form. The advantage of this solution is to also represent shared sub-terms. For instance, the type α → α ∣ α = τ is different from the type τ → τ when sharing is taken into account. Sharing may be present in the source program (for instance if the user specifies type constraints;) it may also be introduced during unification. Keeping sharing increases efficiency; when displaying types, it also keeps them concise, and usually, more readable.

Moreover, type sharing is also used to keep row variables anonymous. For instance, ⟨m : int; η⟩ → ⟨m : int; η⟩, is represented as α → α where α = ⟨m : int; 1⟩. The elimination of sharing would either be incorrect or require the re-introduction of row variables.

In OCaml, type sharing is displayed using the as construct. A shared sub-term is printed as a variable, and its equation is displayed in the tree at the left-most outer-most occurrence of the sub-term. The last example is thus displayed as (⟨m : int; 1⟩ as α) → α. The previous example is simply (τ as α) → α. The recursive type µ α. ⟨m : int → α⟩, which is represented by α where α = ⟨m : int → α⟩, is displayed as (⟨m : int → α⟩ as α).

Remark that the as construct binds globally (while in (µ α. τ) → α, the variable α used to name the recursive sub-term of the left branch is a free variable of the right branch).

Type abbreviations

Although object types are structural, there are also named, so as to be short and readable. This is done using type abbreviations, generated by classes, and introduced when taking object instances.

Type abbreviations are transparent, ie. they can be replaced at any time by their definitions. For instance, consider the following example

class c = object method m = 1 end;;
class c : object method m : int end
let f x = x#m in let p = new c in f p;;

The function f expects an argument of type ⟨m : α; 1⟩ while p has type c. If c were a regular type symbol, the unification of those two types would fail. However, since it is an abbreviation, the unification can proceed, replacing c by its definition ⟨m : int⟩, and finally returning the substitution α ↦ int.

3.2.2  Typing classes

Typechecking classes is eased by a few design choices. First, we never need to guess types of classes, because the only form of abstraction over classes is via functors, where types must be declared. Second, the distinction between fields and methods is used to make fields never visible in objects types; they can be accessed only indirectly via method calls. Last, a key point for both simplicity and expressiveness is to type classes as if they were taking self as a parameter; thus, the type of self is an open object type that collects the minimum set of constraints required to type the body of the class. In a subclass a refined version of self-type with more constraints can then be used.

In summary, the type of a basic class is a triple ζ(τ)(F;M) where τ is the type of self, F the list of fields with their types, and M the list of methods with their types. However, classes can also be parameterized by values, ie. functions from values to classes. Hence, class types also contain functional class types. More precisely, they are defined by the following grammar (we use letter ϕ for class types):

ϕ ::= ζ(τ)(FM) ∣ τ → ϕ
Class bodies

Typing class bodies can first be explored on a small example. Let us consider the typing of class object u = au; m = ς(xam end in a typing context A. This class defines a field u and a method m, so it should have a class type of the form ζ(τ)(u : τu; m : τm). The computation of fields of an object takes place before to the creation of the object itself. So as to prevent from accessing yet undefined fields, neither methods nor self are visible in field expressions. Hence, the expression au is typed in context A. That is, we must have Aau : τu. On the contrary, the body of the method m can see self and the field u, of types τ and τu, respectively. Hence, we must have A, x : τ, u : τuam : τm. Finally, we check that the type assumed for the m method in the type of self is the type inferred for method m in the class body. That is, ie. we must have τ = ⟨m : τm; ρ⟩.

Figure 3.3: Typing rules for class bodies
A ⊢ ∅ : ζ(τ)(∅; ∅)
A ⊢ B : ζ(τ)(FM)           A ⊢ a : τ'
A ⊢ (Bu = a) : ζ(τ)(F ⊕ u : τ'; M)
A ⊢ B : ζ(τ)(FM)           Ax : τ, F ⊢ a : τ'
A ⊢ (Bm = ς(x)  a) : ζ(τ)(FM ⊕ m : τ') 
A ⊢ B : ζ(τ)(FM)           A ⊢ d : ζ(τ)(F'; M')
A ⊢ B  inherit  d : ζ(τ)(F ⊕ F'; M ⊕ M')

The treatment of the general case uses an auxiliary judgment AB : ζ(τ)(F; M) to type the class bodies, incrementally, considering declarations from left to right. The typing rules for class bodies are given in figure 3.3. To start with, an empty body defines no field and no method and leaves the type of self unconstrained (rule Empty). A field declaration is typed in the current environment and the type of body is enriched with the new field type assumption (rule Field). A method declaration is typed in the current environment extended with the type assumption for self, and all type assumptions for fields; then the type of the body is enriched with the new method type assumption (rule Method). Last, an inheritance clause simply combines the type of fields and methods from the parent class with those of current class; it also ensures that the type of self in the parent class and in the current class are compatible. Fields or methods defined on both sides should have compatible types, which is indicated by the ⊕ operator, standing for compatible union.

Class expressions
Figure 3.4: Typing rules for class expressions
A ⊢ B : ζ(τ)(FM)           τ = ⟨M; ρ⟩
A ⊢ object B end : ζ(τ)(FM)
d : ∀ α.  ϕ
A ⊢ d : ϕ [α← τ]
Ax : τ ⊢ d : ϕ
A ⊢ λ xd : τ → ϕ
A ⊢ d : τ → ϕ           A ⊢ a : τ
A ⊢ d  a : ϕ

The rules for typing class expressions, described in Figure 3.4, are quite simple. The most important of them is the Object rule for the creation of a new class: once the body is typed, it suffices to check that the type of self is compatible with the types of the methods of the class. The other rules are obvious and similar to those for variables, abstraction and application in Core ML.

Figure 3.5: Extra typing rules for expressions
A ⊢ d : ϕ 
         Az : ∀ (ftv(ϕ) ∖ ftv(A)).  ϕ ⊢ a : τ
A ⊢ class z = d  in  a : τ
A ⊢ d : ζ(τ)(FM)           τ = ⟨M; 0⟩
A ⊢ new  d : τ

Finally, we must also add the rules of Figure 3.5, for the two new forms of expressions. A class binding class z = d in a is similar to a let-binding (rule Class): the type of the class d is generalized and assigned to the class name z before typing the expression a. Thus, when the class z is inherited in a, its class type is an instance of the class type of d. Last, the creation of objects is typed by constraining the type of self to be exactly the type of the methods of the class (rule  New). Note the difference with Object rule where the type of self may contain methods that are not yet defined in the class body. These methods would be flagged virtual in OCaml. Then the class itself would be virtual, which would prohibit taking any instance. Indeed, the right premise of the New rule would fail in this case. Of course, the New rule enforces that all methods that are used recursively, ie. bound in present type of self, are also defined.

Mutable fields

The extension with mutable fields is mostly orthogonal to the object-oriented aspect. This could use an operation semantics with store as in Section 2.2.

Then, methods types should also see for each a field assignment primitive (u ← _) for every field u of the class. Thus the Method typing rule could be changed to

A ⊢ B : ζ(τ)(FM)           Ax : τ, FF⊢ a : τ'
A ⊢ (Bm = ς(x)  a) : ζ(τ)(FM ⊕ m : τ')

where F stands for {(u ← _ : F(u) → unit) ∣ udom (F)}.

Since now the creation of objects can extend the store, the New rule should be treated as an application, ie. preventing type generalization, while with applicative objects it could be treated as a non-expansive expression and allow generalization.


As opposed to assignment, overriding creates a new fresh copy of the object where the value of some fields have been changed. This is an atomic operation, hence the overriding operation should take a list of pairs, each of which being a field to be updated and the new value for this field.

Hence, to formalize overriding, we assume given a collection of primitives {⟨u1 = _; …; un = _⟩} for all nIN and all sets of fields {u1, … un} of size n. As for assignment, rule methods should make some of these primitives visible in the body of the method, by extending the typing environment of the Method rule of Figure 3.3. We use the auxiliary notation {⟨u1 : τ1; … un : τn⟩}τ for the typing assumption

({⟨u1 = _; … un = _⟩} :  τ1 → … τn → τ)

and F * τ the typing environment ∪F' ⊂ F {⟨F'⟩}τ. Then, the new version of the Method rule is:

A ⊢ B : ζ(τ)(FM)           Ax : τ, FF * τ ⊢ a : τ'
A ⊢ (Bm = ς(x)  a) : ζ(τ)(FM ⊕ m : τ')

Since uses of subtyping are explicit, they do not raise any problem for type inference. In fact, subtyping coercions can be typed as applications of primitives. We assume a set of primitives (_ : τ1 :> τ2) of respective type scheme ∀ α.  τ1 → τ2 for all pairs of types such that τ1 ≤ τ2. Note that the types τ1 and τ2 used here are given and not inferred.

Figure 3.6: Closure and consistency rules for subtyping
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')
 τ ≤ Absτ = Abs
 τ ≤ ατ = α

The subtyping relation ≤ is standard. It is structural, covariant for object types and on the right hand side of the arrow, contravariant on the left hand side of the arrow, and non-variant on other type constructors. Formally, the relation ≤ can be defined as the largest transitive relation on regular trees that satisfies the closure and consistency rules of figure 3.6:

Subtyping should not be confused with inheritance. First, the two relations are defined between elements of different sets: inheritance relates classes, while subtyping relates object types (not even class types). Second, there is no obvious correspondence between the two relations. On the one hand, as shown by examples with binary methods, if two classes are in an inheritance relation, then the types of objects of the respective classes are not necessarily in a subtyping relation. On the other hand, two classes that are implemented independently are not in an inheritance relation; however, if they implement the same interface (eg. in particular if they are identical), the types of objects of these classes will be equal, hence in a subtyping relation. (The two classes will define two different abbreviations for the same type.) This can be checked on the following program:

class c1 = object end class c2 = object end;; fun x -> (x : c1 :> c2);;

We have c1c2 but c1 does not inherit from c2.

Exercise 29 (Project —type inference for objects)   Extend the small type checker given for the core calculus to include objects and classes.

3.3  Advanced uses of objects

We present here a large, realistic example that illustrates many facets of objects and classes and shows the expressiveness of Objective Caml.

The topic of this example is the modular implementation of window managers. Selecting the actions to be performed (such as moving or redisplaying windows) is the managers' task. Executing those actions is the windows' task. However, it is interesting to generalize this example into a design pattern known as the subject-observer. This design pattern has been a challenge [10]. The observers receive information from the subjects and, in return, request actions from them. Symmetrically, the subjects execute the requested actions and communicate any useful information to their observers. Here, we chose a protocol relying on trust, in which the subject asks to be observed: thus, it can manage the list of its observers himself. However, this choice could really be inverted and a more authoritative protocol in which the master (the observer) would manage the list of its subjects could be treated in a similar way.

Unsurprisingly, we reproduce this pattern by implementing two classes modeling subjects and observers. The class subject that manages the list of observers must be parameterized by the type 'observer of the objects of the class observer. The class subject implements a method notify to relay messages to all observers, transparently. A piece of information is represented by a procedure that takes an observer as parameter; the usage is that this procedure calls an appropriate message of the observer; the name of the message and its arguments are hidden in the procedure closure. A message is also parameterized by the sender (a subject); the method notify applies messages to their sender before broadcasting them, so that the receiver may call back the sender to request a new action, in return.

class ['observer] subject = object (self : 'mytype) val mutable observers : 'observer list = [] method add obs = observers <- obs :: observers method notify (message : 'observer -> 'mytype -> unit) = List.iter (fun obs -> message obs self) observers end;;

The template of the observer does not provide any particular service and is reduced to an empty class:

class ['subject] observer = object end;;

To adapt the general pattern to a concrete case, one must extend, in parallel, both the subject class with methods implementing the actions that the observer may invoke and the observer class with informations that the subjects may send. For instance, the class window is an instance of the class subject that implements a method move and notifies all observers of its movements by calling the moved method of observers. Consistently, the manager inherits from the class observer and implements a method moved so as to receive and treat the corresponding notification messages sent by windows. For example, the method moved could simply call back the draw method of the window itself.

class ['observer] window = object (self : 'mytype) inherit ['observer] subject val mutable position = 0 method move d = position <- position + d; self#notify (fun x -> x#moved) method draw = Printf.printf "[Position = %d]" position; end;; class ['subject] manager = object inherit ['subject] observer method moved (s : 'subject) : unit = s#draw end;;

An instance of this pattern is well-typed since the manager correctly treats all messages that are send to objects of the window class.

let w = new window in w#add (new manager); w#move 1;;

This would not be the case if, for instance, we had forgotten to implement the moved method in the manager class.

The subject-observer pattern remains modular, even when specialized to the window-manager pattern. For example, the window-manager pattern can further be refined to notify observers when windows are resized. It suffices to add a notification method resize to windows and, accordingly, an decision method resized to managers:

class ['observer] large_window = object (self) inherit ['observer] window as super val mutable size = 1 method resize x = size <- size + x; self#notify (fun x -> x#resized) method draw = super#draw; Printf.printf "[Size = %d]" size; end;; class ['subject] big_manager = object inherit ['subject] manager as super method resized (s:'subject) = s#draw end;;

Actually, the pattern is quite flexible. As an illustration, we now add another kind of observer used to spy the subjects:

class ['subject] spy = object inherit ['subject] observer method resized (s:'subject) = print_string "<R>" method moved (s:'subject) = print_string "<M>" end;;

To be complete, we test this example with a short sequence of events:

let w = new large_window in w#add (new big_manager); w#add (new spy); w#resize 2; w#move 1;;
<R>[Position = 0][Size = 3]<M>[Position = 1][Size = 3]- : unit = ()
Exercise 30 (Project —A widget toolkit)   Implement a widget toolkit from scratch, ie. using the Graphics library. For instance, starting with rectangular areas as basic widgets, containers, text area, buttons, menus, etc. can be derived objects. To continue, scroll bars, scrolling rectangles, etc. can be added.

The library should be design with multi-directional modularity in mind. For instance, widgets should be derived from one another as much as possible so as to ensure code sharing. Of course, the user should be able to customize library widgets. Last, the library should also be extensible by an expert.

In additional to the implementation of the toolkit, the project could also illustrate the use of the toolkit itself on an example. Here is for instance a screen shot during a session of an application running a small window manager implemented on top of the toolkit.

The subject/observer pattern is an example of component inheritance. With simple object-oriented programming, inheritance is related to a single class. For example, figure 3.7 sketches a common, yet advanced situation where several objects of the same worker class interact intimately, for instance through binary methods. In an inherited slave class, the communication pattern can then be enriched with more connections between objects of the same class. This pattern can easily be implemented in OCaml, since binary methods are correctly typed in inherited classes, as shown on examples in Section 3.1.2.

Figure 3.7: Traditional inheritance

A generalization of this pattern is often used in object-oriented components. Here, the intimate connection implies several objects of related but different classes. This is sketched in figure 3.8 where objects of the worker class interact with objects of the manager class. What is then often difficult is to allow inheritance of the components, such that objects of the subclasses can have an enriched communication pattern and still interact safely. In the sketched example, objects of the slave class on the one hand and object of boss or spy classes on the other hand do interact with a richer interface.

Figure 3.8: Component inheritance

The subject/observer is indeed an instance of this general pattern. As shown above, it can be typed successfully. Moreover, all the expected flexibility is retained, including in particular, the refinement of the communication protocol in the sub-components.

The key ingredient in this general pattern is, as for binary methods, the use of structural open object types and their parametric treatment in subclasses. Here, not only the selftype of the current class, but also the selftype the other classes recursively involved in the pattern are abstracted in each class.

Further reading

The addition of objects and classes to OCaml was first experimented in the language ML-ART [64] —an extension of ML with abstract types and record types— in which objects were not primitive but programmed. Despite some limitations imposed in OCaml, for sake of simplification, and on the opposite some other extensions, ML-ART can be still be seen as an introspection of OCaml object oriented features. Conversely, the reader is referred to [66, 72] for a more detailed (and more technical) presentation.

Moby [20] is another experiment with objects to be mentioned because it has some ML flavor despite the fact that types are no longer inferred. However, classes are more closely integrated with the module system, including a view mechanism [68].

A short survey on the problem of binary methods is [9]. The “Subject/Observer pattern” and other solutions to it are also described in [10]. Of course, they are also many works that do not consider type inference. A good but technical reference book is [1].

Previous Up Next