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, h_{a}, h_{c}. 
let rec type a = á m : c ® b ® unit; h_{a}ñ 
and c = á m_{1} : a ® unit; m_{2} : b ® unit; h_{c}ñ in 
class (c)[u : a; m_{1} : a ® unit; m_{2} : 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 rowvariables
The above type class can be written as such in Ocaml. This is made possible
by the use of row variables, such as h_{c} and h_{a} (in fact, in
Ocaml, h_{a} would be left anonymous, and h_{c} 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 recordtypes) [Rém94, Wan87] allow one to grab exactly the part of the
object that is polymorphic: the row variables h_{a} and h_{c} 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
extensiblerecord 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; h_{a}ñ and similarly for c; that
is, one is lead to write:

"b.
" a <: á m : c ® b ® unitñ.
" c <: á m_{1} : a ® unit; m_{2} : b ® unitñ. 
class (c)[u : a; m_{1} : a ® unit; m_{2} : b ® unit] 

The bound of a depends on c and conversely. Thus, the above type is
illformed. There is no way to order type variables so as to obtain a
wellformed 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 Ocamllike classbased objectoriented
extension of F_{<:}^{w}:

All (b <: T) 
All (R^{a}<: Fun (c:*) á m : c ® b ® unitñ) 
All (R^{c}<: Fun (a:*) á m_{1} : a ® unit; m_{2} :
b ® unitñ) 
let rec type a = R^{a}c and c = R^{c}a in 
class (c)[u : a; m_{1} : a ® unit; m_{2} : 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 classbased language, which
includes recursive types. This is to keep closer to the Ocaml
objectoriented 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.
Fbounded quantification with recursively defined bounds 

Fbounded quantification has been used to type binary methods involving
recursion between a quantified type variable and its bound [CCH^{+}89]. However, Fbounded 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 Fbounded quantification with
recursively defined bounds would allow one to replace
" (a <: t_{a}). " (c <: t_{c}). T
by " (a <: t_{a}Ù c <: t_{c}). T.
Variables a and c can now appear in both of their bounds.
Note that, as opposed to system F_{<:} or even Fbounded
quantification, ML with subtyping constraints inherently comes with
recursive Fbounded quantification (with multiple bidirectional
bounds) [EST95a]. Thus, an objectoriented
language based on type constraints such as [EST95b] should also easily handle virtual types.
The extension of Fbounded 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 £ á m_{1} : a ® unit; m_{2} : b ® unitñ
) 
[ u : a; m_{1} : a ® unit; m_{2} : 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 illformed. 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.)
Matchbounded quantification with recursively
defined bounds 

Matchbounded quantification [Bru95] can
solve binary methods as easily as row variables do.
However, it suffers from the same
problem as boundedquantification 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 matchbounded quantification with multiple recursive
bounds does not have to enforce grouping. More recently,
Bruce and Vanderwaart also proposed a notion of typegroup and classgroup 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; m_{1} : a ® unit; m_{2} : 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 metatheory of type destructors remains quite
complicated as a result of their generality, and recordtype destructors are
not considered in [HP98].