Previous Contents Next
3 The necessary ingredients for decoupling classes


As shown in section 1, classes do not need to be recursive. Object types, however, often need to be mutually recursive. For instance, the type of class subject in section 1 has the following polymorphic class type, which uses recursive object types:
" b, ha, hc.
let rec type a = á m : c ® b ® unit; hañ
and c = á m1 : a ® unit; m2 : b ® unit; hcñ in
class (c)[u : a; m1 : a ® unit; m2 : b ® unit]
We used letrec type .. and .. in .. rather than a standard recursive µ-binder both to emphasize the mutual dependence and to reduce the verbosity (expanding the former into the later would force some duplication).

Using row-variables
The above type class can be written as such in Ocaml. This is made possible by the use of row variables, such as hc and ha (in fact, in Ocaml, ha would be left anonymous, and hc would be left implicit.) The key point here is that the quantified row variables are independent and unconstrained. Row variables (and the corresponding rich structure of record-types) [Rém94, Wan87] allow one to grab exactly the part of the object that is polymorphic: the row variables ha and hc occur at the leaves of the types that are bound to a and c; therefore they are external to the recursion.

Indeed, the language Ocaml is not the only one to allow to write such a type. However, expressing this type in F<: fails. This is not so surprising since virtual types include binary methods and system F<: is not powerful enough to type binary methods. The problem is that standard record or object types used in F<: are less expressive than extensible-record types used for Ocaml object types: there is no way to grab record polymorphism directly as an unconstrained polymorphic type variable. Instead, one is forced to quantify a with a bound of the form á m : c ® b ® unit; hañ and similarly for c; that is, one is lead to write:
"b. " a <: á m : c ® b ® unitñ. " c <: á m1 : a ® unit; m2 : b ® unitñ.
class (c)[u : a; m1 : a ® unit; m2 : b ® unit]
The bound of a depends on c and conversely. Thus, the above type is ill-formed. There is no way to order type variables so as to obtain a well-formed type expression.

Programming in F<:w
The system F<:w [SP94] is sufficiently powerful to abstract over, and thus isolate, the interior of a record type. The recursion can then be broken by parameterizing the bound of one of these types over the other one. Assuming an Ocaml-like class-based object-oriented extension of F<:w:
All (b <: T)
All (Ra<: Fun (c:*) á m : c ® b ® unitñ)
All (Rc<: Fun (a:*) á m1 : a ® unit; m2 : b ® unitñ)
let rec type a = Rac and c = Rca in
class (c)[u : a; m1 : a ® unit; m2 : b ® unit]
The code of class subject would be: 
class subject =
  fun (E <: $\Top$)
  fun (RO <: Fun (S <: $\Top$) <at_notification : S -> E -> unit>)
  fun (RS <: Fun (O <: $\Top$) <add_observer : O -> unit; notify : E -> unit>)
  letrec type O = RO S and S = RS O in
    object (self : S)
      val observers : O  = []
      method add_observers (x : O) =  observers <- x :: observers;
      method notify (e : E) =
        List.iter (fun (obs: O) obs.at_notification self e) observers
    end
This solution is unsurprising, since a similar pattern has been used to type binary methods in F<:w [BCC+96]3. We assumed an extension of F<:w with a class-based language, which includes recursive types. This is to keep closer to the Ocaml object-oriented layer. We should be able to write the subject/observer example in plain F<:w encoding objects into records and existential types, even though the lack of primitive classes will likely make the example more verbose.

F-bounded quantification with recursively defined bounds

F-bounded quantification has been used to type binary methods involving recursion between a quantified type variable and its bound [CCH+89]. However, F-bounded quantification as presented in [CCH+89] only allows this particular case and does not help when the recursion extends to several bounds. Assuming a simple extension of F-bounded quantification with recursively defined bounds would allow one to replace " (a <: ta). " (c <: tc). T by " (a <: taÙ c <: tc). T. Variables a and c can now appear in both of their bounds.

Note that, as opposed to system F<: or even F-bounded quantification, ML with subtyping constraints inherently comes with recursive F-bounded quantification (with multiple bi-directional bounds) [EST95a]. Thus, an object-oriented language based on type constraints such as [EST95b] should also easily handle virtual types.

The extension of F-bounded quantification to recursively defined bounds has actually been used in the language Pizza [OW97b]. Thus, in principle, Pizza could allow the same style of programming as ours. Indeed, it was already shown in [BOW98] that examples involving virtual types can be implemented with and only with parametric polymorphism. However, the solution proposed in [BOW98] still enforces grouping: Two related classes A and B are replaced by two groups of recursive definitions. The first group defines two generators A' and B' abstracted over classes X and Y that should be instances of the generators, respectively: 
public class A'<X extends A'<X,Y>, Y extends B'<X,Y>> { ... }
public class B'<X extends A'<X,Y>, Y extends B'<X,Y>> { ... }
Classes A and B are then defined as fix points of the generators: 
public class A extends A'<A,B> { public A (args) { super (args); } }
public class B extends B'<A,B> { public B (args) { super (args); } }
Inheritance must be applied to generators and must preserve the group structure. The authors find this solution unsatisfactory. Consequently, they present an extension to Java/Pizza to cope with virtual types more directly. Hence, the authors chose to augment the coupling of related classes, while we prefer to loose such coupling as much as possible.

One may still wonder whether decoupling related classes is possible in Pizza, since its type system seems to have sufficient expressiveness. Below is an (unsuccessful) attempt to write the above class type in Pizza:
class (b £ á ñ, a £ á m : c ® b ® unitñ, c £ á m1 : a ® unit; m2 : b ® unitñ )
[ u : a; m1 : a ® unit; m2 : b ® unit]
Alas, Pizza object types cannot be built from scratch, but only as the types of elements of classes. Hence, the above expression is ill-formed. An expression with equivalent meaning can only be built using recursively defined classes.

Adding structural types to Pizza would allow one to define a class with the above type. For convenience, one could also add an anonymous fix point construct so as to avoid the systematic need for the second group definition. (Once grouping has been eliminated, this second step becomes easier and should usually be a simple type application.)

Match-bounded quantification with recursively defined bounds

Match-bounded quantification [Bru95] can solve binary methods as easily as row variables do. However, it suffers from the same problem as bounded-quantification in its inability to grab the interior of a record type. In the subject/observer example, bounds would also need to be recursively defined. This difficulty has motivated an extension of LOOM [BFP97, Bru97] with recursively defined bounds, which actually lead to the proposal presented in [BOW98]. Again, we claim that match-bounded quantification with multiple recursive bounds does not have to enforce grouping. More recently, Bruce and Vanderwaart also proposed a notion of type-group and class-group that apparently releases some of the coupling of classes involving virtual types [Bru98, BV99]. In particular, an inherited group may have more components than the parent group.

In fact, since LOOM already has structural types, it would suffice to allow the definition of multiple match bounds, where all bounded type variables, as well as MyType, may occur in the bounds. For instance, one should be able to write the following class type in LOOM:
class (b <# á ñ, a <# á m : MyType ® b ® unitñ )
[ u : a; m1 : a ® unit; m2 : b ® unit]
Moreover, using recursive classes would allow one to use the type name of one class to bound the type parameter of the other. Here is a possible implementation of the classes subject and observer in LOOM extended with recursively defined bounds and recursive classes: 
class subject (E, O <# observer (E, MyType)) 
  var observers : list(O) = []
  methods
    procedure add_observer (obs : O) { observers := obs :: observers }
    procedure notify (e : E)
       { List.iter (function (obs:O) { obs.at_notification (self, e) }, observers) }
and observer (E, S <# subject (E, MyType)) 
  methods procedure at_notification (s : S, e : E) { }
end class
A significant difference with [BOW98] is that grouping is not enforced here; on the opposite, it remains optional, and may be used only when convenient. Moreover, grouping here is just a standard recursive definition and each definition can still be understood (and used) independently from the other.

In fact, the proposal for virtual types that is presented in [BOW98] is based on matching, as done in LOOM, and is thus very close to the above schema, with the exception that it lacks structural types. This exemplifies that the choice between structural and declared object types is a rather significant design choice.

Extending type destructors to object types

Yet another possibility is to use type destructors, which have recently been proposed by Hofmann and Pierce [HP98]. Type destructors retain some of the expressiveness of type operators provided by F<:w while keeping within second order types. In fact, row variables can be seen as a special form of type destructors for records where only the expansion is retained (the contraction for record types has been formally studied in [Rém90, Sag95], but it revealed to be useless in practice, and therefore it has not been included in the language Ocaml). Hence, type destructors might solve virtual types as well as row variables do in Ocaml. However, the meta-theory of type destructors remains quite complicated as a result of their generality, and record-type destructors are not considered in [HP98].

Previous Contents Next