The programming patterns that lead to the introduction of virtual types are
not new in the object-oriented community. However, they recently became
famous for the typechecking challenges that they posed to some recent,
modern, and statically typed object-oriented languages, including several
extensions to Java [OW97a, Bru97]. The notion
of virtual types, first introduced in
Beta [KMMPN87], was not type-safe.
It is difficult to precisely define virtual types, since they have been
presented through programming patterns and (often incomplete) examples.
Some of them were written in informal extensions of existing languages.
Virtual types have never been given a semantic or syntactic
characterization.
Intuitively however, virtual types always involve the definition of several
related classes that interact with one another, such that at least the type
of objects of one of these classes depends on the type of objects of
another one;
moreover, the types of objects of these classes are often, but not
always, mutually recursive.
A few statically type-safe versions of virtual types have been
proposed [BOW98, Tor98].
In [BOW98] the authors show that
examples involving virtual types can be rewritten using only parametric
polymorphism. The language they used for this demonstration is Pizza ---an
extension of Java with parametric polymorphism [OW97a].
However, as the examples of virtual types written in Pizza are sometimes long
and tedious, the authors propose a new primitive construct to
allow a better treatment of virtual types. This includes a mechanism for
grouping together several class definitions. Classes of a group can be
inherited, but only simultaneously. The other work [Tor98] also introduces a primitive but different
construct.
In this paper, we argue as in [BOW98]
that virtual types can be encoded with parametric polymorphism. However, we
disagree with the introduction of a primitive notion of virtual types to
palliate the heaviness of their encoding in Pizza. Conversely, we claim
that no specific construct is necessary. We argue by giving a more direct
coding of examples involving virtual types. The approach is simpler, more
flexible, and more powerful than theirs.
In fact, using Ocaml [Ler96, RV98] as
the implementation language, all examples that we know as involving virtual
types can actually be typed in with no effort at all. Actually, the untyped
code that one naturally writes needs only to be documented with class type
parameters and, sometimes, with type constraints. No other change in the
code is necessary.
Had we not known about this challenge, we would not have
noticed any particular difficulty.
Through detailed examples and comparisons with other solutions, we are still
able to identify the potential difficulty of virtual types. An obvious
requirement is to have self-types in the language, i.e. the ability to type
self with an open object type (partially known object types). However,
mutual recursion between open object types is also needed in many examples
of virtual types. Then, the key is to be able to leave the recursion at the
level of types such that classes do not have to be defined recursively.
In Ocaml, this is permitted by the use of structural object types,
and of row variables [Rém94, Wan87] to keep
the monomorphic, recursive structure isolated from the unconstrained,
polymorphic row variables.
In fact, we are also able to transpose our solution to a few other languages
languages that posses structural types and that can already handle binary
methods.
In the language F<:w [Car90, SP94], we
only need to assume some standard class-based object-oriented extension, but
nothing else. Languages based on match-bounded quantification [BSvG95, BFP97] or F-bounded
quantification [CCH+89] need to be extended with
recursively defined bounds. For instance, this has been recently been done
for the language LOOM in [BV99]. On the
other hand, languages such as Pizza or GJ that already have recursive
F-bounded quantification need to be extended with structural object types,
only.
The rest of the paper is organized as follows. In section 1, we describe in detail the subject/observer
pattern [GHJV95] in Ocaml; we explain the typing constraints
and show the most general class types that are automatically inferred in
Ocaml. In section 2, we compare our solution to other
solutions in strongly-typed languages. We discuss the drawbacks of tightly
grouping definitions of related classes as do virtual types; we show that
enforcing a fixed recursive schema is too rigid (it imposes some
redundancies) and are too restrictive (some inheritance patterns cannot be
expressed). In section 4, we consider another example of
virtual types known as the ``cow/animal'', and discuss the issues of
expressiveness and abstraction. We also show that the lack of abstraction
does not clearly reduce expressiveness. In section 5, we use
the example of alternating lists to argue that while parametric types are
preferable to virtual types: parametric types allow a continuous refinement
of a hierarchy of classes while virtual types show up abruptly at a
particular point in the hierarchy.