|| Expressiveness and abstraction
Examples of virtual types were first motivated by the need for
expressiveness so that safe practical examples would not be rejected. The
first solutions to virtual types were unsafe. Safe solutions have been
proposed in [BOW98, Tor98].
In both works, the priority is given to expressiveness, i.e.
to the ability to write known useful examples in a sound typed language.
Recently, virtual types have also been studied for their
abstraction capabilities [IP99].
The cow/animal example, introduced by David
Shang [Sha96], actually mixes both issues; it also
demonstrates the use
of virtual types for specializing the type of a class by inheritance.
First, we present our solution in Ocaml; then, we discuss the
issue of type abstraction.
In its simplest and naive form, this example does not require mutual
recursion between open object types; it could a priori be typed in
languages based on F<: with parametric classes.
The example straightforwardly translates into Ocaml, as virtual types are
here only used to provide bounded type parameterization of classes.
We first define a hierarchy of food classes.
class food = object method food = () end ;;
class grass = object inherit food method grass = () end;;
class meat = object inherit food method meat = () end;;
We then introduce a generic class for starving animals.
class virtual ['a] starving_animal f =
constraint 'a = #food
method diet : 'a = f
method virtual private eat : 'a -> unit
eat is flagged
virtual because it is not yet
implemented. The class must also be flagged
virtual, so that no
instance of the class can be taken. The method
eat is flagged
private so that it does not appear in the type of starving animals,
<diet : 'a> where
'a is the type of the food it eats.
One can also define the class type of real animals (with a method eat):
class type ['a] animal =
object constraint 'a = #food method diet : 'a method eat : 'a -> unit end;;
Of course, an animal is not an omnivore. The former eats some not yet
specified food, while the latter eats any kind of food.
class omnivore =
object inherit [food] starving_animal (new food) method eat f = f#food end;;
Note that the type
omnivore is equal to
We can define a particular race of animals that eat a specific type of
class camel = object
inherit [grass] starving_animal (new grass) method eat (f:grass) = f#grass
The important property is to statically ensure that a camel can eat grass,
but not meat (the phrase in italic is ill-typed).
new camel#eat (new grass);;
new camel#eat (new meat);;
Using an explicit coercion would not help, since
meat is not a subtype of
grass. A camel cannot either eat some unspecified kind of food, that is
new camel#eat (new food) is also
It is important to be able to forget the exact diet of camels. Of
course, a camel is not an omnivore since it cannot eat any type of food.
To hide information about the type of food by subtyping, one must also
eat, which is contravariant in the type food, so as to be
Indeed, an animal cannot be fed if we do not know its diet.
A camel can still be seen as a
since the food a camel eats is
A camel is also a
the food a camel eats is
grass is (a subtype of)
Conversely, a camel is not a
meat animal, since
grass is not (a subtype
an animal is given the following type:
This says that an animal is an object with two methods diet and eat of
respective types t and t ® unit for some type t that is a subtype
of food. A camel and an omnivore have similar types, but with t
á t = $ a <: food.a; diet : t; eat : t ® unitñ
By subtyping, a camel and an omnivore can both be given the type animal,
forgetting their exact type, but retaining the fact that they eat some kind
of food. Both of them can also be given the type of starving animals
á t = $ a <: food.a; diet : tñ, now ignoring that
they can eat.
camel : á t = grass; diet : t; eat : t ® unitñ
omnivore : á t = food; diet : t; eat : t ® unitñ
Partially abstract object types are obviously more precise than our object
types. In particular, we are not able to express the type animal and we
can only give camels the weaker type of starving animals. Practically,
however, the difference is not very significant: an object of type animal
cannot eat: since its diet is unknown, whatever food it is offered will be
rejected. Thus, we have not really lost expressiveness here, but solely
some form of abstraction. Conversely, common examples of the form of
subject/observer pattern that involve mutual recursion of object types
cannot be typed in [IP99].
In [BV99] Bruce and Vanderwaart add
hash-types to provide a form of partially abstract type that is quite
similar to [IP99] in terms of expressiveness.
Partially abstract types are an orthogonal feature that can also be added to
mostly any language (even if this may not always be immediate and may
sometimes raise other design issues). This confirms our early claim
that virtual types are not an atomic construction, since it simultaneously
contains a form of universal and existential (bounded) quantification.