Mads Torgersen
Computer Science Department, Arhus University Ny Munkegade, DK-8000 Arhus C, Denmark
(+45) 89 42 32 57 [email protected]
Abstract
Virtual types are a combined genericity and covariance mech- anism rst introduced in BETA. Like most other covari- ant language constructs, virtual types in their original form depend on dynamic checking for type safety. This paper presents full statical type checking for virtual types, while not relying on any other special language mechanisms for safety. Good expressiveness is retained, as demonstrated by a simple but eective solution to the infamous ColourPoint problem.
1 Introduction
Madsen 11] states that \it is well known that at most two of the following three properties can be obtained at the same time:
1. Static typing.
2. Subtype substitutability.
3. Covariance."
It is the intention of this paper to demonstrate that this need not be so.
Virtual types, originally introduced in Beta14], are a very powerful and expressive mechanism, which gives rise to covariance. In their original form, virtual types gave rise to a certain amount of dynamic typechecking, and this was adopted by a recent proposal for introducing virtual types in Java 9] by Thorup 18].
In this paper we introduce fully statical type checking of virtual types, while not compromising subtype substitutabil- ity in any way. The key to retaining expressiveness under these conditions is the ability { also present in Beta { of virtual types to be nal bound.
2 What are virtual types
Virtual types are best thought of as symbolic names for classes. These names (or aliases) are themselves attributes
of classes, and their binding { the class they are a name for { may be overwritten in subclasses. This overwriting { called further binding { must be covariant, i.e. to a subclass of the previous binding.
A special kind of further binding called a nal binding has the additional property of xing the binding of the vir- tual type: It may not be further bound in subclasses. Thus, in this way the potential further covariance of a virtual type may be explicitly prohibited.
2.1 An example
The \Cow Example", originating from a brilliant treatment of covariance by David Shang 17], illustrates the mechanism of virtual types and nal bindings as well as serving as a basis for demonstrating their typing implications.
Animal =f
FoodType<=Food
eat(f: FoodType)f... g
g
Herbivore = Animalf FoodType<=Plants
g
Cow = Herbivoref FoodType = Grass
g
Figure 1: The cow example
FoodType is a virtual type. In the declaration ofAnimal it is declared, and bound to Food. This means that \an Animal has a FoodType, which is some subclass of Food".
The consequence for theeatmethod also declared inAnimal is that \anAnimalcaneatsome kind ofFood".
In the declaration of Herbivore as a subclass ofAnimal, FoodTypeis further bound to Plants. This means that \the FoodType of anHerbivoreissome subclass ofPlants". As a consequence \anHerbivorecaneatsome kind ofPlants".
In the declaration ofCowas a subclass ofHerbivore,Food- Typeis nal bound toGrass. This means that \theFoodType of aCowisprecisely Grass". As a consequence \aCowcan eatany kind ofGrass".
Leaving out an implementation of theeatmethod should emphasize the fact (already suggested by their name) that
virtual types are primarily a matter of typingrather than functionality. The only functionality directly associated with virtual types is the possibility of instantiating them with the newoperation.
In order to see the typing implications of virtual types, let us investigate some uses of theAnimalhierarchy of Fig- ure 1.
Farmer =f
FeedCow(c: Cow, g: Grass)f c.eat(g)
g
g
Figure 2: Cow feeding: A sure success
AFarmer, as dened if Figure 2, is able to take a cow and some grass, and give the grass to the cow. This, according to the interpretation of theCow class given above, is quite alright, since anyCowwill eat any kind ofGrass.
BadFarmer =f
FeedCow(c: Cow, m: Meat)f c.eat(m)
g
g
Figure 3: Cow choking: A sure failure
At the other end, sinceMeatis denately notGrass, try- ing as the BadFarmer of Figure 3 to give it to a cow can never succeed, and is therefore a certain static type error.
Trying to generalize this mixed experience we move on to dene aKeeper(Figure 4) who is able to take an animal and some food, and give the food to the animal.
Keeper =f
FeedAnimal(a: Animal, f:Food)f a.eat(f)
g
g
Figure 4: A keeper having a problem
Trying this out with a cow and some grass should work just as ne as for theFarmer above. Unfortunately, giving the cow meat or giving the grass to a lion seems to be equally possible. Thus, theFeedAnimalmethod of theKeeperclass is type safe on some inputs but not on others. The problem is that the method assumes that any Animal can eat any kind ofFood, while according to the declaration of Animal it is only guaranteed toeatsomekind ofFood.
Betahandles this optimistically by allowing the method to be statically type checked, but inserting code for perform- ing adynamictype check every time the method is invoked to ensure that only sensible (i.e. typesound) executions of a.eat(f)are allowed.
Essentially the only dierence between the Beta ap- proach and the one suggested in this paper is, that we do
not allow such optimism. In order to buy the full static type safety thatBetadoesn't have, the possibilty of writing code such as theKeeperis sacriced. WhereBetainserts runtime type checks, we ag a static type error instead.
3 Other covariance mechanisms
This section investigates the relationship of virtual types with other language constructs giving rise to covariance.
We look at the ability of virtual types to express these con- structs, as well as the possibility of adding equivalents of
nal bindings to them, in order to try to gain the same static safety for these mechanisms as we just achieved with virtual types.
3.1 Signature covariance
In Eiel 15], overwriting a method in a subclass allows for specialization of the method parameters, a facility one could call signature covariance. Since any parameter types may be specialized, only a global analysis of the program can determine whether unsafe situations arise.
It should be clear that this mechanism can be simulated with method parameters of virtual type, likef:FoodTypein the eat method from Figure 1. Furthermore, more static typechecking is possible, exploiting that parameters with non-virtual or closed virtual type are guaranteednot to be covariant.
It is quite straightforward to imagine making languages like Eiel safer by adding an anonymous parallel of nal bindings some kind of marker explicitly agging a given parameter type as \not covariant" in subclasses.
3.2 Self recursive classes
3] gives a good overview of various approaches to the prob- lem of so-calledbinary methods methods that are supposed to take arguments of the type of their enclosing object. One way to express this is to introduce a special keyword My- Type2] orSAME16] which is covariant in the sense that it always denotes the class of theactualenclosing object - not the one where theMyTypeappears.
One might view (and implement) MyType as a virtual type which is automatically bound in all classes 18]. Such a solution makes static typing problematic, however, because MyTypeobviously cannot be nal bound (except of course in a language that has nal classes, such as Java). Beta
lets the programmer manually specify such virtuals when- ever needed 13], and nal bind them at suitable places. An example of this approach is theCompareTypeof theColour- Pointexample in Figure 12 and 13.
4 A pseudo-language
Until now virtual types have most often been described in the context of full-edged commercial programming lan- guages, specically Beta and Java 14, 18]. This has the disadvantage that the typing aspects of virtual types are mangled with those of other constructs of these languages
e.g. part objects and block structure inBeta, or abstract and nal classes, interfaces and constructors in Java.
For this reason we have chosen here to use an absolutely minimal pseudo-language, which contains no such features and is designed so as to let the properties of virtual types stand out for themselves.
Program ::= ClassDecl*
ClassDecl ::= ClassId =ClassId fVirtualDecl*VarDecl*MethodDecl*g
VirtualDecl ::= VirtualId <=ClassId
j VirtualId =PreType
VarDecl ::= VarId : PreType
MethodDecl ::= MethodId (ParDecl* ) : PreTypefStatement*g
ParDecl ::= ParId: PreType PreType ::= ClassId
j VirtualId Statement ::= Expression
j Expression.VarId :=Expression
j returnExpression
Expression ::= this
j ParId
j Expression.VarId
j Expression.MethodId (Expression* )
j newType Type ::= ClassId
j Expression.VirtualId
Figure 5: The pseudo-language This approach carries with it the danger that its results
cannot survive subsequent exposure to a more complex en- vironment (indeed this is acknowledged as one of the mo- tivating factors for applying formal type theory to Java in
6]). In order to try out the type checking scheme and pro- gramming techniques suggested in this paper in a somewhat more realistic setting, statically safe virtual types are cur- rently being added to a compiler for a subset of Java see Section 9.
The language, sketched in gure 5, is intended to be the essential core of a statically typed, statically scoped, class- based, single-inheritance object-oriented language. The only thing special is the presence of virtual types.
For clarity, and to ease the formulation of type rules, the syntax is somewhat restrictive. Several kinds of pro- gramming constructs and syntactic sugar with little impact on type checking might easily be added, and indeed many of the program examples throughout this paper belong to a more permissive superset. In the course of the following description some obvious relaxations and additions will be noted.
4.1 Declarations
A program is a number of class declarations. Each class has one superclass, which could have been optional. (Multi- ple inheritance would seriously complicate things and is not considered.) It furthermore has a body of attribute declara- tions, of which there are three kinds: Virtual types, instance variables and methods.
Virtual types are declared and further bound with \<="
and nal bound with \=". A nal binding prohibits further binding in subclasses. Virtual types are covariant, which means that a binding must always specialize the previous one. A virtual typeVcan be nal bound to another oneV0, meaning that V will automatically have the same binding
as V0 in all subclasses. A virtual type is closed in a class if it is nal bound to a class or another closed virtual type.
Otherwise it is open.
Instance variables are mutable object references. Their declaration may not be overridden in subclasses. Immutable references could be added, but would complicate things due to the need for an initialization mechanism. As will be evi- dent below, immutable references play a special role in the type checking of expressions, but method parameters, which areimmutable, will su ce to demonstrate this point.
Methods are declared with a number of formal parame- ters, a return type (which in a \real" language would have been optional) and a body of statements. The body may be overridden in subclasses, but the signature (formal parame- ters and return type) cannot be changed. As already men- tioned, formal parameters are immutable object references.
Because covariance on signatures is not allowed, statically resolved method overloading as inC++ 7] could be added without problems. For the same reason asuperconstruct for calling overwritten methods as in Smalltalk and Java 8, 9]
would have identical type properties tothis. 4.2 Statements and expressions
The syntax in gure 5 contains only statements and expres- sions that are important from a typing point of view. This means that there are no control structures, literal expres- sions or binary operators. Likewise, local variables within statements are omitted.
Only method parameters and the special constant this, denoting the current instance of the enclosing class, may be accessed directly, while all kinds of object attributes { variables, methods and virtual types { must be accessed via a dot expression (as ine:a,e:m() andnewe:V respectively).
Of course a freeVarId acould easily be treated as syntactic sugar forthis.a, as is normal practice.
4.3 Runtime behaviour
At runtime, the evaluation of an expression results in an object. Every object has a class, and is created with the primitivenew. If the argument tonewis a simple class, the new object gets that class. If is is of the forme.V, whereV is a virtual type, thene evaluates to some runtime object, o. The binding ofVin the class of o will then be the class of the new object.
The implementation of object creation requires the bind- ing of virtual types to be represented at runtime. If the language included casting or typecase constructs, they too would need such runtime information, as would of course implicit runtime type checks as used inBeta.
5 Static type checking with virtual types
The purpose of this section is to give a detailed constructive description of how the type checking mechanism is designed to achieve static safety.
To motivate the design we rst review what it takes to be type safe in terms of programexecution and then move on to discuss in an abstract way how this can be checked statically in terms of programinspection.
On the basis of this, a detailed account of the proposed type checking mechanism is given. Type rules are presented only for statements and expressions, while the typing con- straints on declarations are described more informally. Apart from a complete set of type rules, an actual proof of type safety would also require the specication of a formal se- mantics of the language.
5.1 Type safety
We assume the following denitions of type safety:
A program execution is type safe if it no attempt is made to access an attribute of an object that the object doesn't have.
A program is type safe if all executions of it are type safe.
A language is type safe if any program in the language is type safe.
Additionally, type safety is static, if it does not depend on checks performed during program execution.
As for the runtime behaviour of a language implementa- tion it seems fair to assume that
The class of an object does not change.
An object actually has the attributes declared in its class.
Thus it su ces to verify that objects are used according to their class. This in turn follows if each reference (instance variable or method parameter) has an associatedqualica- tionso that
The qualication of a reference is a superclass of the class of the object it refers to.
Only attributes declared in the qualication of a given reference are accessed on the object it refers to.
This rendering is operational in the sense that it tells us what to check for:
When assigning an object to a reference (by variable assignment or method parameter passing), check for the appropriate qualication.
When accessing an attribute of a reference, check the class for an appropriate declaration.
We are now ready to move to static typing. Inspecting a given statement in the program, we can establish its static safeness (the fact that it preserves static type safety) if we can conservatively assert that the above will holdwhenever it is executed.
A natural way to do this is to let expressions and refer- ences have static types which summarize the possible classes they may have at runtime. This will allow us to statically check type safety in a way that nicely parallels the above:
Assignment is checked with the use of a subtype rela- tion betweenstatictypes, which asserts that the needed subclass relation will always hold at runtime.
Attribute access is checked using the most specic stat- ically known common superclass of all classes denoted by the type.
If a static type is covariant, it generally doesn't have any guaranteed subtypes at compile time (the only exceptions being quite specic special cases, as exemplied in Section 5.3 and Figure 6). This is the situation where Betawould in- troduce runtime checks.
The pivotal point of the following is the eshing out of the static type concept and subtype relation for the pseudo- language.
5.2 Basic assumptions
In the following, dierent names denote dierent kinds of entities, according to this table:
name is used for C0CC0 classes
A attributes
V virtual types TTi pretypes M0M methods
S statements
a instance variables
p parameters
eei expressions
0i types
in numbers
Attributes is a common designation for virtual types, instance variables and methods. Types and pretypes will be further explained below.
5.3 Pretypes and types
With all that in place, we can now attack the central prob- lem: What should a static type be, in order to facilitate full static type checking, yet be as permissive as possible, so as not to inhibit expressiveness.
A good starting point is to see what types we might assign to anewexpression, since this is where objects begin their existence. To go with \new C" it seems obvious to introduce a plain class type, denoted byhCi.
What should be the type of \newe:V"? Since the binding ofV depends recursively on the type ofe (say), the only
way not to throw away potentially useful type information is to keep along withV in the type of the expression. Such a type is writtenhVi.
This scheme matches well with the fact that the so-called pretype of e.g. variable declarations (see Figure 5) can be either a class or a virtual type. When a variable with class pretype (say a:C) is used within a method body (as in
\this:a"), its type should of course behCi.
But what should be the type of a variable with virtual pretype (saya:V) within a method body? The type is not completely determined by the pretype, but depends on the type of the object thataresides in { its location. This in- completeness is why the type part of a reference declaration is called apre-type.
The type schemefhCihViggenerally works well, but there is one nuisance still left to cope with. In general, we have no option but to forbid assignment to references of open virtual type. Reverting to the animal example for a moment, however, take a look at the class declaration in Figure 6: Given an animal, the keeper feeds it its own kind of food! There would be nothing wrong with accepting this, since the parameter type ofeat{ although denately virtual { is obviously the same as the one produced bynew a.FoodType.
Keeper =f
Feed(a: Animal)f a.eat(new a.FoodType)
g
g
Figure 6: A keeper at a zoo
The reason is that we are refering to the same virtual type in the same object { the latter \same" guaranteed by the immutability of method parameters. To allow for this special case, we introduce an extra kind of typehcifor con- stant referencesc in our case parameters orthis. Their type is simply themselves.
5.4 Environments
The program environmentPcontains the class declarations of the program, and the subclass relation between them. It denes the following relations:
relation means
C2P Cis declared inP
P`CC0 Cis a subclass ofC0
A class environment contains the attributes of the class. It denes the following relations:
relation means
PC0`V<=C V is open, bound toC
PC0`V=T V is nal bound toT
PC0`a:T ais declared toT
PC0`M:T1:::Tn!T signature ofM
A method environment contains the parameters and body of the method. It denes the following relations:
relation means
PC0M0`e: ehas type
PC0M0` <:0 is a subtype of0
C M S S typechecks
5.5 Checking declarations
Type rules for the declaration of classes and attributes have been left out. Thus a description lacks of how the vari- ous environments are constructed and their well-formedness maintained (e.g. according to Section 4.1). While this is certainly nontrivial, it is generally not profoundly inuenced by the presence of virtual types. One exception to this is
nal binding of one virtual type to another. This must be non-circular in order for the Type function of Figure 7 to terminate.
5.6 Type inference rules
Finally we can give precise meaning to the type checking requirements treated throughout this section.
As explained above (Section 5.3), the type of a reference in the context of a given method body must be computed from its pretype and the type of its location. This com- putation is handled by the Typefunction, which is dened by means of inference rules in Figure 7. Notice that the computation for a nally bound virtual pretype is simply propagated to its binding - regardless of whether this bind- ing is itself virtual.
Typeclass `C2P
PC0M0`Type(C) =hCi Typevirtual PC0M0`C0=Class()
PC0`V<=C
PC0M0`Type(V) =hVi Typenal PC0M0`C0=Class()
PC0`V=T
PC0M0`Type(V) =Type(T) Figure 7: TheTypefunction
As concluded in Section 5.1, in order to type check at- tribute access of an expressione, we need to nd the most specic superclass of the type ofe. This is done by theClass function, which is dened in Figure 8.
Classclass `C2P
PC0M0 `ClasshCi=C Classvirtual PC0M0 `C0=Class()
PC0`V<=C
PC0M0 `ClasshVi=C Classnal PC0M0 `C0=Class()
PC0`V=T
PC0M0 `C=Class(Type(T))
PC0M0 `ClasshVi=C Classthis PC0M0 `Classhthisi=C0 Classpar PC0`(p:T)2M0
PC0M0 `C=Class(Type(ThC0i))
PC0M0 `Classhpi=C Figure 8: TheClassfunction
The subtyping relation<: is dened in Figure 9. It gen- erally allows only assignments to references with class type, and even that of course only if the type of the assigned value ts. Notice however, the special treatment of virtual
types within constant references, which was motivated by theKeeperexample above (Figure 6).
Subtypeclass PC0M0`C0=Class()
P`C0C
PC0M0` <:hCi
Subtypethis:V PC0M0`hthisVi<:hthisVi Subtypepar:V PC0`p2M0
PC0M0`hpVi<:hpVi Figure 9: The subtype relation<:
The type rules proper (Figures 10 and 11) are pretty much standard, since most of the virtual type specic \magic"
appears in the above helper functions and the subtype rela- tion.
Expthis PC0M0`this:hthisi Exppar PC0`p2M0
PC0M0`p:hpi Expvar PC0M0`e:0
PC0M0`C=Class(0)
PC`a:T
PC0M0` =Type(T0)
PC0M0`e:a: Expapp PC0M0`e:0
PC0M0`C=Class(0)
PC`M :T1:::Tn!T
PC0M0` =Type(T0)
PC0M0`ei:i 1in
PC0M0`i<:Type(Ti0) 1in
PC0M0`e:M(e1:::en) : ExpnewC `C2P
PC0M0`newC:hCi ExpnewV PC0M0`e:0
PC0M0` =Type(V0)
PC0M0`newe:V : Figure 10: Expression types 6 Expressiveness
To demonstrate that full static typing of virtual types does not sacrice too much expressiveness, we mainly focus on the covariance problem as exemplied by the now classical ColourPointexample.
6.1 Points and ColourPoints
A standard example in the literature on covariance (see e.g.
11, 3, 5]) is the so called ColourPoint problem, which is shown in Figure 12. It is usually stated using signature covariance or self recursive types (see Section 3), but is here refrased with virtual types.
The idea is that both classes are concrete1. The reason for ColourPoint to inherit Point supposedly is twofold: To
1Anabstractclass is a class that is not supposed to be instantiated, but only functions as a superclass. By contrast, aconcreteclass is one that may have instances.
Stmexp PC0M0`e:
PC0M0`e Stmassign PC0M0`e0:0
PC0M0`C=Class(0)
PC`a:T
PC0M0`e:
PC0M0` <:Type(T0)
PC0M0`e0:a:=e Stmreturn PC0M0`e:
PC0`M0:T1:::Tn!T
PC0M0` <:Type(ThC0i)
PC0M0`returne Figure 11: Statements
Point =f x,y: Integer
CompareType<=Point
equal(p: CompareType): Boolf return (this.x=p.x) and (this.y=p.y)
g
g
ColourPoint = Pointf c: Color
CompareType = ColourPoint
equal(p: CompareType): Boolf
return super.equal(p) and (this.c = p.c)
g
g
Figure 12: The usual colour point problem reuse its implementation, and to make references to Point able to polymorphically also refer toColourPoints.
Covariance comes into play with the methodequal, which expects its argument to be of the virtual typeCompareType. In ColourPoint, CompareType has to be further (or in this case nal) bound to ColourPointso that the equalmethod can take its specic attributes into consideration.
Of course, with this structure, calling theequalmethod on a reference to aPointis generally not statically type safe precisely because the reference might contain instances of subclasses (indeed ofColourPoint), which further bindCom- pareType uncontrollably. Alas, we cannot safely compare twoPointsfor equality!
This situation is usually regarded as a shortage of the covariance mechanism. we prefer to view it as a modelling mistake: If aPointis something that can be compared with anotherPointfor equality, then aColourPointis not a sub- type of Point{ since it cannot. Hence, it should not be a subclass either.
6.2 A solution
Instead, the close relationship between the two should be captured by a common abstract superclass as in Figure 13.
All desirable properties of the original approach are re- tained: PointandColourPointstill share most of their imple- mentation, References capable of polymorphically referring both can still be declared, now usingAbstractPoint.
AbstractPoint =f x,y: Integer
CompareType<=Point
equal(p: CompareType): Boolf return (this.x=p.x) and (this.y=p.y)
g
g
Point = AbstractPointf CompareType = Point
g
ColourPoint = AbstractPointf c: Color
CompareType = ColourPoint
equal(p: CompareType): Boolf
return super.equal(p) and (this.c = p.c)
g
g
Figure 13: A slight change xes the problem On top of this comes the fact that Point may now be used in a safe way, and that references to Points that can notcontainColourPointsare now possible.
AbstractPoint =f x,y: Integer
CompareType<=Point
equal(p: CompareType): Boolf return (this.x=p.x) and (this.y=p.y)
g
g
Point = AbstractPointf
CompareType = AbstractPoint
g
ColourPoint = AbstractPointf c: Color
CompareType = AbstractPoint
g
Figure 14: A dierent choice of semantics
Furthermore the programmer now has the full choice of whether or not to allowPointsandColourPointsto be com- pared with each other. If this should be possible, these classes should just nal bindCompareTypetoAbstractPoint instead of to themselves, as shown in Figure 14. The two classes could even have dierent semantics, so that aPoint will accept a ColourPoint, but not vice versa { the choice belongs entirely to the programmer.
This restructuring is always possible: If you need a con- crete version of a class that has open virtual types, make a concrete subclass of it, where you nal bind all the virtuals.
If the creation of such trivial subclasses proves too tedious, one might consider simply adding a language construct for doing it automatically.
In our opinion, this cuts the Gordian knot.
7 Related work
The covariance problem as exemplied through theColour- Pointexample, has been treated in numerous ways over the past decade or so. This section relates some of the proposed solutions to the one presented here.
7.1 Separating subclassing and subtyping
Due to the covariance problem, it was proposed in 4] to separate the subtype and subclass relations. This has the appeal that a variable declared by a given type does not need to be able to hold all subclasses of an associated class, but only those that are known to be substitutable for the declared type.
In Emerald 10] and many theoretical languages (such asLOOM2]) this lead to a complete separation of classes (that describe implementation) and types (that describe in- terface), which in turn leads to quite a specication overhead when types and classes coincide.
To avoid this, Sather 16] reunies types and classes, and only separate the tworelations, subtyping and subclassing.
Clearly, stepping down on the demand that subclassing yields subtyping, gives new possiblities for static type check- ing. It is not without problems however { keeping track of two dierent but closely related relations can be confusing in practice.
A more profound objection seen from our point of view aims at the way this solution views inheritance: Primarily as a code reuse mechanism. Instead of modelling a concep- tually clear specialization relation, subclassing is anad hoc relationship between classes. This is why the need is felt for a seperate, \cleaner" relation.
From the perspective of this article, subtyping and the conceptual specialization relation coincide, and inheritance should only be allowed to be used in this way. As seen in Section 6, this does not prohibit the reuse of code, it just requires it to occur in a slightly more structured way: as in- heritance of a common ancestor rather that as conceptually unsound inheritance from \cows to horses".
7.2 Monomorphic types
Covariance is only a problem because references to classes with covariant parameter types may contain instances of subtypes. Some solutions therefore introduce various con- structs to avoid the unfortunate consequences of subtype substitutability in certain cases { in other words to have monomorphically as well as polymorphically typed variables.
Building on a proposal by Dodani and Tsai 5], Sather
16] divides classes into abstract and concrete, of which only the latter can be instantiated. While concrete classes can have subclasses, they do not have any subtypes. For this reason a variable qualifed by a concrete type can only refer objects ofexactlythat class.
This is reminiscent of Java's nal classes 9], which pro- hibit further specialization, and thus make references quali-
ed by them monomorphic.
A dierent way to do this is to let the references them- selves be declared type exact. This is the case with part objects inBeta12] and with exact types inLOOM, where subtyping has been completely dropped in favour of match- ing see below.
For describing instances of concrete classes, which in a natural way often are (or should be) leaf classes, monomor- phism seems like a sensible idea, although it appears to be somewhat vulnarable to later redesigns of the kind where
one concrete class is turned into an abstract one to intro- duce dierent variants as subclasses.
The reason why it is not considered in our langauage is that it is not necessary. Since all virtual types can be
nal bound, a concrete subclass without covariant parame- ters can aways be declared. As opposed to a nal class, such a \nalized" class (likeCow in Section 2.1) can have sub- classes (likeDairyCow,Herefordetc.), and references qualifed by it can refer to instances of these subclasses.
7.3 Matching
Another approach is to say: well, if inheritance does not give us subtyping, whatdoesit give us then? The answer is matching 1, 2]. InLOOMreferences can be qualifed with so called \hash types", say #C, which cover any classes that matchC, that is, all subclasses ofC. A reference to a hash type is restricted so that only methods without covariant parameters can be called on it. Therefore the covariance problem does not occur.
InLOOM, If you want to refer only toPointsyou use the typePoint(which is monomorphic), while if you want to refer also toColourPointsyou use the type #Point, but are then not allowed to call a covariantequalmethod on it.
Notice how closely this corresponds to Point and Ab- stractPointrespectively in our solution. The only dierence seems to be that we have to declare an extra class, but on the other hand get polymorphism on references to Point, plus the ability to callequalonAbstractPointin special sit- uations, as described in Section 5.3.
8 Genericity
This paper has mainly focused on the covariance issues of virtual types.
Virtual types as an alternativegenericity mechanism to parameterized types (as in Eiel 15], C++ 7] and many others) is usually criticized because of it's alleged depen- dence on dynamic typechecking. With this proposal that argument loses validity { as for static type safety, virtual types must now be seen as an equally valid choice.
Yet, rather than looking at virtual and parameterized types as contenders, it is compelling to ponder the possi- bilities of combining the strengths of the two approaches.
While it is certainly outside the scope of this paper to give a proper proposal for such a fusion, it should be noted in passing, that the statical safety of virtual types brings it a lot closer.
9 Riding the Java Train
Java currently supports neither genericity nor covariance.
Since these are issues that many people have opinions about, a lot of dierent proposals are currently being made for adding such facilities one way or the other.
And yes, a proposal for adding virtual types to Java has also come forth 18]. While blending very elegantly into the syntactic framework of Java, and { as it seems { neatly t- ting the virtual types in with particular Java constructs such as interfaces and abstract classes, this otherwise convincing proposal has one serious drawback: It requires implicit dy- namic type checking.
InBetaall so called reverse assignments2 are statically allowed, but subjected to a runtime type check. The run-
2Assignments from general to more special types
time checking introduced by virtual types ts nicely into this scheme, and can be seen as a special case.
Java, however, is a fully statically type checked language.
With the one unfortunate exception of arrays, which are covariant and require dynamic checks, runtime checking of types can only come about as a result ofexplicittype casts in the code. The introduction ofimplicitruntime checks would profoundly violate this very deliberate principle of Java.
This is where the cavalry comes in. If the type checking scheme proposed here expands well to Java, this last prob- lem is overcome. To gain further insight into this, statically safe virtual types are currently being added to an experi- mental compiler for the JOOS subset of Java (generously provided by Michael Schwartzbach and Laurie Hendren).
This implementation project will serve as a proof of con- cept both of the feasibility of virtual types in Java and of the practicality of the type checking scheme of this paper.
10 Conclusion
The main conclusion to draw from this paper is that covari- ance, static type safety and subtype substitutability are not incompatible after all. But to make them coexist without losing out fatally on expressiveness, a mechanism must be provided to control covariance, and programmers need to be aware of its impact on type checking.
The type checking framework in Section 5 is to the best of our knowledge the rst in-depth account of a type check- ing mechanism for a language with virtual types. Since the permission of dynamic checks is merely a matter of modi- fying the subtype relation<:, the approach might inspire a more formal description of e.g. theBeta type system, al- though admittedly the presence of block structure probably complicates matters somewhat.
While resting heavily on the presence of nal bindings for safety, the proposed solution to theColourPointproblem (Figure 13) in our oppinion also points to a more philosoph- ical consideration. The inheritance relation prescribed by the original version reects a simple minded desire for code reuse. Whether or not it is meaningful to say thatColour- Points actuallyare Points, and to what extend sensible se- mantics for comparing the two dierent kinds of objects may exist, is not at all considered.
Taking aconceptualview, we think that { even without the type safety { the new version is how we would have modelled the situation. This is just one example of what in our experience { but this is just a gut feeling { seems to be a common pattern: That conceptual modelling and type-theoretic soundness tend to go hand in hand.
References
1] Abadi, M., and Cardelli, L. On subtyping and matching. In ECOOP'95 { Object-Oriented Program- ming (1995), pp. 145{167.
2] Bruce, K. B. Subtyping is not a good \match" for object-oriented languages. In ECOOP'97 { Object- Oriented Programming (1997), M. Aksit and S. Mat- suoka, Eds., no. 1241 in Lecture Notes on Computer Science, Springer, pp. 104{127.
3] Bruce, K. B., Cardelli, L., Castagna, G., The Hopkins Object Group, Leavens, G. T., and Pierce, B. On binary methods. Theory and Practice of Object Systems, 1 (1995), 221{242.
4] Cook, W. R., Hill, W. L., and Canning, P. S.
Inheritance is not subtyping. In ACM Conference on Principles of Programming Languages (POPL'90) (1990), ACM Press, pp. 125{135.
5] Dodani, M., and Tsai, C.-S. Acts: A type system for object-oriented programming based on abstract and concrete classes. InECOOP'92 { Object-Oriented Pro- gramming(1992), O. L. Madsen, Ed., no. 615 in Lecture Notes in Computer Science, Springer, pp. 309{328.
6] Drossopoulou, S., and Eisenbach, S. Java is type safe - probably. InECOOP'97 { Object-Oriented Pro- gramming (1997), M. Aksit and S. Matsuoka, Eds., no. 1241 in Lecture Notes on Computer Science, Springer, pp. 389{418.
7] Ellis, M. A., and Stroustrup, B. The Annotated C++ Reference Manual. Addison-Wesley, 1990.
8] Goldberg, A., and Robson, D. Smalltalk-80 { The Language. Addison-Wesley, 1989.
9] Gosling, J., Joy, B., and Steele, G. The Java Language Specication. Addison-Wesley, 1996.
10] Hutchinson, N. Emerald: An Object-Oriented Lan- guage for Distributed Programming. PhD thesis, De- partment of Computer Science, University of Washing- ton, Seattle, WA, January 1987.
11] Madsen, O. L. Open issues in object-oriented programming{a scandinavian perspective. Software{
Practice and Experience 25, S4 (December 1995).
12] Madsen, O. L., Magnusson, B., and Mller- Pedersen, B. Strong typing of object-oriented lan- guages revisited. In Proceedings of OOPSLA'90 (Ot- tawa, Canada, 1990), SIGPLAN, ACM Press.
13] Madsen, O. L., and Mller-Pedersen, B. Virtual classes: A powerful mechanism in object-oriented pro- gramming. InProceedings of OOPSLA'89 (1989), SIG- PLAN, ACM Press.
14] Madsen, O. L., Mller-Pedersen, B., and Ny- gaard, K.Object-Oriented Programming in the BETA Programming Language. Addison-Wesley, 1993.
15] Meyer, B. Object-Oriented Software Construction. Prentice Hall International Series in Computer Science.
Prentice Hall, Englewood Clis, NJ, 1988.
16] Omohundro, S. The Sather Programming Language.
Dr. Dobb's Journal 18, 11 (October 1993).
17] Shang, D. Are cows animals? Object Currents 1, 1 (January 1996). http://www.sigs.com/objectcurrents/.
18] Thorup, K. K. Genericity in java with virtual types.
InECOOP'97 { Object-Oriented Programming (1997), M. Akit and S. Matsuoka, Eds., no. 1241 in Lecture Notes on Computer Science, Springer, pp. 444{471.
