Previous Contents Next
4 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 =
  object
    constraint 'a = #food
    method diet : 'a = f
    method virtual private eat : 'a -> unit
  end ;;
The method 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, which is <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 food animal. We can define a particular race of animals that eat a specific type of food. 
class camel = object 
  inherit [grass] starving_animal (new grass) method eat (f:grass) = f#grass
end;;
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 ill-typed.

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 hide method eat, which is contravariant in the type food, so as to be sound. Indeed, an animal cannot be fed if we do not know its diet. A camel can still be seen as a grass starving_animal since the food a camel eats is grass. A camel is also a food starving_animal: the food a camel eats is food, since grass is (a subtype of) food. Conversely, a camel is not a meat animal, since grass is not (a subtype of) meat.

In [IP99], an animal is given the following type:
animal =def á t = $ a <: food.a; diet : t; eat : t ® unitñ
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 known exactly:
camel : á t = grass; diet : t; eat : t ® unitñ
omnivore : á t = food; 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.

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.

Previous Contents Next