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:
Object types are structural (ie. they structure is
transparent) and use row variables to allow polymorphism;
Class types are polymorphic in the type of self to allow further
refinements.
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 u Î F of field names,
m Î M of method names, and z Î Z of class names.
Figure 3.1: Syntax for objects and classes
Expressions
a ::= ... | new a | a#m | classz = dina
Class expressions
d ::=
objectBend
creation
|
z | l x. d | da
abstraction and instantiation
Class bodies
B ::= Ø |
Binheritd |
B
u = a
field
|
B
m = V(x) a
method
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 Bend, 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 V(x) m where x is a binder for self.
Of course, we can always see the OCaml expression object (x) u = a; m1 =
a1; m2 = a1end as syntactic sugar for objectu = a; m1 = V(x) a1;
m2 = V(x) a1end. 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.
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 h Î R,
raw types and rows are described by the following grammars:
t ::= ... | árñ
r ::= 0 | h | m : t; r
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 : t; m : t'; r)
should be rejected as ill-formed.
Other types such as ám : t; rñ ® árñ should also be ruled
out since replacing r by m : t'; r 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 r
(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 : t; (m' : t'; r) is equal to m' : t'; (m : t; r). For
notational convenience, we assume that (m : _; _) binds tighter to
the right, so we simply write (m : t; m' : t'; r).
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:
Message
A |- a : ám : t; rñ
A |- a#m : t
That is, if an expression a is an object with a method m of type t
and maybe other methods (captured by the row r), then the expression
a#m is well-typed and has type t.
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) : " a, h. ám : a; hñ
® a)m Î M. 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:
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
(
$ hi. ámi : ti; hiñ = ei
)
where U, all ti's and ei's do not contain any row
variable.
In such a case, we may abbreviate $ hi. ámi : ti; hiñ
= ei as ámi : ti; 1ñ = e, using an anonymous row
variable 1 instead of h.
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 a = ám : t; 1ñ
can be replaced by a kind constraint
a :: ám : t; 1ñ (then
a = ám : t; 0ñ is also replaced by
a :: ám : t; 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
l-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 µ q. t can be used to represent the
infinitely unfolded tree t [q ¬ t [q ¬
...]]. Alternatively, a regular tree can also be represented as a pair
t | 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 a ® a | a = t is different from the
type t ® t 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; hñ ® ám : int; hñ,
is represented as a ® a where a = á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 a) ®
a. The previous example is simply (t as a) ® a.
The recursive type µ a. ám : int ® añ, which is represented
by a where a = ám : int ® añ, is displayed as (ám : int ® añ as a).
Remark that the as construct binds globally (while in (µ a. t)
® a, the variable a 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 inlet p = new c in f p;;
The function f expects an argument of type ám : a; 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 a
|® int.
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 z(t)(F;M) where
t 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 j for class types):
j ::= z(t)(F; M) | t ® j
Class bodies
Typing class bodies can first be explored on a small example.
Let us consider the typing of class objectu
= au; m = V(x) amend 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 z(t)(u : tu; m : tm).
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 A |- au : tu.
On the contrary, the body of the method m can see self and the field u,
of types t
and tu, respectively. Hence, we must have A, x :
t, u : tu |- am : tm. 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 t = ám : tm; rñ.
Figure 3.3: Typing rules for class bodies
Empty
A |- Ø : z(t)(Ø; Ø)
Field
A |- B : z(t)(F; M) A |- a : t'
A |- (B, u = a) : z(t)(F Å u : t'; M)
Method
A |- B : z(t)(F; M) A, x : t, F |- a : t'
A |- (B, m = V(x) a) : z(t)(F; M Å m : t')
Inherit
A |- B : z(t)(F; M) A |- d : z(t)(F'; M')
A |- Binheritd : z(t)(F Å F'; M Å M')
The treatment of the general case uses an auxiliary judgment A |- B : z(t)(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
Object
A |- B : z(t)(F; M) t= áM; rñ
A |- objectBend : z(t)(F; M)
Class-Var
d : " a. j
A |- d : j [a¬ t]
Class-Fun
A, x : t |- d : j
A |- l x. d : t ® j
Class-App
A |- d : t ® j A |- a : t
A |- da : j
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
Class
A |- d : j
A, z : " (ftv(j) \ ftv(A)). j |- a : t
A |- classz = dina : t
New
A |- d : z(t)(F; M) t= áM; 0ñ
A |- new d : t
Finally, we must also add the rules of Figure 3.5,
for the two new forms of expressions. A class binding classz = dina
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
Method
A |- B : z(t)(F; M) A, x : t, F, F¬|- a : t'
A |- (B, m = V(x) a) : z(t)(F; M Å m : t')
where F¬ stands for {(u ¬ _ : F(u) ® unit)
| u Î dom (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.
Overriding
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 n Î IN 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 : t1; ... un : tnñ}t for the
typing assumption
({áu1 = _; ... un = _ñ} :
t1 ® ... tn ® t)
and F * t the typing environment ÈF' Ì F
{áF'ñ}t.
Then, the new version of the Method rule is:
Method
A |- B : z(t)(F; M) A, x : t, F, F * t |- a : t'
A |- (B, m = V(x) a) : z(t)(F; M Å m : t')
Subtyping
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 (_ : t1 :> t2) of
respective type scheme " a. t1 ® t2 for all pairs of types
such that t1 £ t2. Note that the types t1 and t2 used here
are given and not inferred.
Figure 3.6: Closure and consistency rules for subtyping
Closure rules
t1 ® t2 £ t1' ® t2'
Þ
t1' £ t1 Ù t2 £ t2'
átñ £ át'ñ
Þ
t £ t'
(m : t1; t2) £ (m : t'1; t2')
Þ
t1 £ t1' Ù t2 £ t2'
Consistency rules
t £ t1 ® t2
Þ
t is of the shape t1' ® t2'
t £ át0ñ
Þ
t is of the shape át0'ñ
t £ (m : t1; t2)
Þ
t is of the shape (m : t1'; t2')
t £ Abs
Þ
t = Abs
t £ a
Þ
t = a
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 c1 £ c2 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.
