Subtyping and Inclusion Polymorphism
Subtyping makes it possible for an object of some type to be considered and
used as an object of another type. An object type ot2 could be a
subtype of ot1 if:
-
it includes all of the methods of ot1,
- each method of ot2 that is a method of ot1 is a
subtype of the ot1 method.
The subtype relation is only meaningful between objects: it can only be
expressed between objects. Furthermore, the subtype relation must always be
explicit. It is possible to indicate either that a type is a subtype of
another, or that an object has to be considered as an object of a super type.
Syntax
(name : sub_type :> super_type) |
(name :> super_type) |
Example
Thus we can indicate that an instance of colored_point can be used
as an instance of point:
# let
pc
=
new
colored_point
(4
,
5
)
"white"
;;
val pc : colored_point = <obj>
# let
p1
=
(pc
:
colored_point
:>
point);;
val p1 : point = <obj>
# let
p2
=
(pc
:>
point);;
val p2 : point = <obj>
Although known as a point, p1 is nevertheless a colored point, and
sending the method to_string will trigger the method relevant for
colored points:
# p1#to_string();;
- : string = "( 4, 5) with color white"
This way, it is possible to build lists containing both points and colored
points:
# let
l
=
[
new
point
(1
,
2
)
;
p1]
;;
val l : point list = [<obj>; <obj>]
# List.iter
(fun
x
->
x#print();
print_newline())
l;;
( 1, 2)
( 4, 5) with color white
- : unit = ()
Of course, the actions that can be performed on the objects of such a list are
restricted to those allowed for points.
# p1#get_color
()
;;
Characters 1-3:
This expression has type point
It has no method get_color
The combination of delayed binding and subtyping provides a new form of
polymorphism: inclusion polymorphism. This is the ability to handle
values of any type having a subtype relation with the expected type.
Although static typing information guarantees that sending a message will always find
the corresponding method, the behavior of the method depends on the
actual receiving object.
Subtyping is not Inheritance
Unlike mainstream object-oriented languages such as C++, Java,
and SmallTalk, subtyping and inheritance are different concepts in
Objective CAML. There are two main reasons for this.
-
Instances of the class c2 may have a type that is a subtype of
the object type c1 even if the class c2 does not inherit
from the class c1.
Indeed, the class colored_point can be defined independently from
the class point, provided the type of its instances are constrained to
the object type point.
- Class c2 may inherit from the class c1 but have
instances whose type is not a subtype of the object type c1. This is
illustrated in the following example, which uses the ability to define an
abstract method that takes an as yet undetermined instance as an argument of
the class being defined. In our example, this is method eq of class
equal.
# class
virtual
equal
()
=
object(self:
'a)
method
virtual
eq
:
'a
->
bool
end;;
class virtual equal : unit -> object ('a) method virtual eq : 'a -> bool end
# class
c1
(x0:
int)
=
object(self)
inherit
equal
()
val
x
=
x0
method
get_x
=
x
method
eq
o
=
(self#get_x
=
o#get_x)
end;;
class c1 :
int ->
object ('a) val x : int method eq : 'a -> bool method get_x : int end
# class
c2
(x0:
int)
(y0:
int)
=
object(self)
inherit
equal
()
inherit
c1
x0
val
y
=
y0
method
get_y
=
y
method
eq
o
=
(self#get_x
=
o#get_x)
&&
(self#get_y
=
o#get_y)
end;;
class c2 :
int ->
int ->
object ('a)
val x : int
val y : int
method eq : 'a -> bool
method get_x : int
method get_y : int
end
We cannot force the type of an instance of c2 to be the type of
instances of c1:
# let
a
=
((new
c2
0
0
)
:>
c1)
;;
Characters 11-21:
This expression cannot be coerced to type
c1 = < eq : c1 -> bool; get_x : int >;
it has type c2 = < eq : c2 -> bool; get_x : int; get_y : int >
but is here used with type < eq : c1 -> bool; get_x : int; get_y : int >
Type c2 = < eq : c2 -> bool; get_x : int; get_y : int >
is not compatible with type c1 = < eq : c1 -> bool; get_x : int >
Only the first object type has a method get_y
Types c1 and c2 are incompatible because the type of
eq in c2 is not a subtype of the type of eq in
c1.
To see why this is true, let o1 be an instance of
c1. If o21 were an instance of c2 subtyped to
c1, then since o21 and o1 would both be of type
c1 the type of eq in c2 would be a subtype
of the type of eq in c1 and the expression
o21#eq(o1) would be correctly typed. But at run-time, since
o21 is an instance of class c2, the method eq of
c2 would be triggered. But this method would try to send the message
get_y to o1, which does not have such a method; our type
system would have failed!
For our type system to fulfill its role, the subtyping
relation must be defined less naïvely. We do this in the next
paragraph.
Formalization
Subtyping between objects.
Let t=<m1:t1; ... mn: tn>
and t'=<m1:s1 ; ... ; mn:sn; mn+1:sn+1;
etc...> we shall say that t' is a subtype of t, denoted by t' £
t, if and only if si £ ti for i Î {1,...,n}.
Function call.
If f : t ® s, and if a:t' and t' £ t then (f a) is well
typed, and has type s.
Intuitively, a function f expecting an argument of type t may safely receive
`an argument of a subtype t' of t.
Subtyping of functional types.
Type t'® s' is a subtype of t® s, denoted by
t'® s' £ t® s, if and only if
s'£ s and t £ t'
The relation s'£ s is called covariance, and the relation t £ t' is
called contravariance. Although surprising at first, this relation
between functional types can easily be justified in the context of
object-oriented programs with dynamic binding.
Let us assume that two classes c1 and c2 both have a method m.
Method m has type t1® s1 in c1, and type
t2® s2 in c2. For the sake of readability, let us denote by
m(1) the method m of c1 and m(2) that of c2. Finally, let us
assume c2£ c1, i.e. t2® s2 £ t1® s1, and let us
look at a simple example of the covariance and contravariance relations.
Let g : s1 ® a, and
h (o:c1) (x:t1) = g(o#m(x))
-
Covariance:
- function h expects an object of type
c1 as its first argument. Since c2£ c1, it is legal to pass it an object of type c2. Then
the method invoked by o#m(x) is m(2), which returns a value of type
s2. Since this value is passed to g which expects an argument of type
s1, clearly we must have s2£ s1.
- Contravariance:
- for its second argument, h requires a value of
type t1. If, as above, we give h a first argument of type c2, then method
m(2) is invoked. Since it expects an argument of type t2,
t1£ t2.
Inclusion Polymorphism
By ``polymorphism'' we mean the ability to apply a function to
arguments of any ``shape'' (type), or to send a message to objects of various
shapes.
In the context of the functional/imperative kernel of the language, we have
already seen parameterized polymorphism, which enables you to apply a function
to arguments of arbitrary type. The polymorphic parameters of the function have
types containing type variables. A polymorphic function will execute the same
code for various types of parameters. To this end, it will not depend on the
structure of these arguments.
The subtyping relation, used in conjunction with delayed binding, introduces a
new kind of polymorphism for methods: inclusion polymorphism. It lets
the same message be sent to instances of different types, provided they have been
constrained to the same subtype. Let us construct a list of points where some of
them are in fact colored points treated as points. Sending the same
message to all of them triggers the execution of different methods, depending
on the class of the receiving instance. This is called inclusion polymorphism because it
allows messages from class c, to be sent to any instance of
class sc that is a subtype of c (sc
:>
c) that has been
constrained to c. Thus we obtain a polymorphic message passing for all
classes of the tree of subtypes of c. Contrary to parameterized
polymorphism, the code which is executed may be different for these instances.
Thanks to parameterized classes, both forms of polymorphism can be used together.
Equality between Objects
Now we can explain the somewhat surprising behavior of structural equality
between objects which was presented on page ??. Two objects
are structurally equal when they are physically the same.
# let
p1
=
new
point
(1
,
2
);;
val p1 : point = <obj>
# p1
=
new
point
(1
,
2
);;
- : bool = false
# p1
=
p1;;
- : bool = true
This comes from the subtyping relation. Indeed we can try to compare an
instance o2 of a class sc that is a subtype of c, constrained
to c, with an instance of o1 from class c. If the
fields which are common to these two instances are equal, then these objects
might be considered as equal. This is wrong from a structural point of view
because o2 could have additional fields. Therefore Objective CAML considers
that two objects are structurally different when they are physically
different.
# let
pc1
=
new
colored_point
(1
,
2
)
"red"
;;
val pc1 : colored_point = <obj>
# let
q
=
(pc1
:>
point);;
val q : point = <obj>
# p1
=
q;;
- : bool = false
This restrictive view of equality guarantees that an answer true is
not wrong, but an answer false guarantees nothing.