Inheritance-based subtyping.
play a dual role in mainstream statically typed object-oriented languages, serving as both object generators and object types. In such languages, inheritance implies subtyping. In contrast, the theoretical language community has viewed this linkage as a mistake and has focused on subtyping relationships determined by the structure of object types, without regard to their underlying implementations. In this paper, we explore why inheritance-based subtyping relations are useful, and we describe two different approaches to extending the MOBY programming language with inheritance-based subtyping relations. In addition, we present a typed object calculus that supports both structural and inheritance-based subtyping, and which provides a formal accounting of our extensions to MOBY.
Introduction
There is a great divide between the study of the foundations of object-oriented languages and the practice
of mainstream object-oriented languages like JAVA[AG98] and C ++ [Str97]. One of the most striking
examples of this divide is the r-ole that class inheritance plays in defining subtyping relations. In most
foundational descriptions of OO languages, and in the language designs that these studies have informed,
inheritance does not define any subtyping relation, whereas in languages like JAVA and C ++ , inheritance
defines a subtyping hierarchy. What is interesting about this distinction is that there are certain id-
ioms, such as friend functions and binary methods, that are natural to express in an inheritance-based
subtyping framework, but which require substantial complication to handle in a structural subtyping
framework.
In this paper, we explore why inheritance-based subtyping relations are useful and present a formal
accounting of a small language that supports such subtyping relations. We begin by examining the common
object-oriented idiom of friend functions and exploring how one might implement this idiom in
MOBY [FR99a], which is a language with only structural subtyping. This example illustrates the deficiency
of relying solely on structural subtyping in the language design. We then describe an extension to
MOBY in Section 3 that adds class types and inheritance-based subtyping to MOBY. We show how this
extension supports a number of common idioms, such as friend functions, binary methods, and object
cloning. We then present XMOC in Section 4, which is an object calculus that supports both structural
and inheritance-based subtyping, as well as privacy. XMOC provides a model of the type system of
extended MOBY, and we prove subject-reduction for its type system to validate the design of Extended
MOBY. In Section 5 we describe related work and we conclude in Section 6.
2 The problem with friends
Both C ++ and JAVA have mechanisms that allow some classes and functions to have greater access privileges
to a class's members than others. In C ++ , a class grants this access by declaring that certain other
classes and functions are friends. In JAVA, members that are not annotated as public, protected,
or private are visible to other classes in the same package, but not to those outside the package. In
this section, we examine how to support this idiom in MOBY, a language with structural subtyping and
type Rep <: Bag
objtype Bag { meth add : Int -> Unit }
val union : (Rep, Rep) -> Unit
val mkBag : Unit -> Rep
{
class Bag {
public field items : var List(Int)
public meth add { self.items := x :: self.items }
public maker mk () { field items = Nil }
objtype
objtype Bag { meth add : Int -> Unit }
{ List.app s1.add s2.items }
fun mkBag () -> new mk()

Figure

1: Bags and friends using type abstraction
flexible control over class-member visibility [FR99a] (we include a brief description of MOBY in Appendix
A). This study demonstrates that while it is possible to encode the friends idiom in a language
with only structural type relations, the resulting encoding is not very appealing.
2.1 Friends via partial type abstraction
A standard way to program friends is to use partially abstract types [PT93, KLM94]. For example,

Figure

1 gives the MOBY code for an implementation of a Bag class that has a union function as a
friend. In this example, we have ascribed the BagM module with a signature that makes the Rep type
partially abstract to the module's clients. Outside the module, if we have an object of type Rep, we
can use both the union function and the add method (since Rep is a subtype of Bag), but we cannot
access the items field. Inside the module, the Rep type allows access to all of the members of the Bag
class; 1 the implementation of the union function exploits this access.
Unfortunately, this approach only works for final classes. If we want to extend the Bag class, we
must reveal the class in the signature of the BagM module (as is done in Figure 2). In this version, an
object created using the mk maker cannot be used as an argument to the union function, because it will
not have the Rep type. This limitation also applies to objects created from subclasses of Bag.
2.2 Friends via representation methods
To support both friends and class extension for the same class requires a public mechanism for mapping
from an object to its abstract representation type. With such a mechanism, we can recover the representation
type required by the friend functions. For example, suppose we extend our Bag class to include
a method that returns the number of items in the bag. We call this new class CBag (for counting bag),
and we want to use the union function on objects created from the CBag class. Figure 3 presents this
new implementation. Notice that we have added a public method bagRep to the interface of the Bag
1 The MOBY notation typeof(C) is shorthand for the object type that consists of the public members of class C.
type Rep <: typeof(Bag)
class Bag {
public meth add : Int -> Unit
public maker mk of Unit
val union : (Rep, Rep) -> Unit
val mkBag : Unit -> Rep
{

Figure

2: Revealing the Bag class
class, which returns self at the representation type (Rep). To apply the union function to two bags
b1 and b2, we write "Bag.union (b1.bagRep(), b2.bagRep())." This expression works
even when b1 and/or b2 are counting bags. Also note that the items field is public inside the BagM
module, but is not part of Bag's interface outside the module. This is an example of why objects created
from subclasses of Bag are not subtypes of Rep.
Although this example does not include friends for the CBag class, we have included the representation
method in its interface, which illustrates the main weakness of this approach. Namely, for each
level in the class hierarchy, we must add representation types and methods. These methods pollute the
method namespace and, in effect, partially encode the class hierarchy in the object types. Furthermore,
it suffers from the source-code version of the fragile base-class problem: if we refactor the class hierarchy
to add a new intermediate class, we have to add a new representation method, which changes the
types of the objects created below that point in the hierarchy. While this encoding approach appears to
be adequate for most of the examples that require a strong connection between the implementation and
types, it is awkward and unpleasant.
3 Extended MOBY
In the previous section, we showed how we can use abstract representation types and representation
methods to tie object types to specific classes. From the programmer's perspective, a more natural
approach is to make the classes themselves serve the r-ole of types when this connection is needed. In
this section, we present an extension of MOBY [FR99a] that supports such class types and inheritance-based
subtyping. Intuitively, an object has a class type #C if the object was instantiated from C or
one of its descendants. Inheritance-based subtyping is a form of by-name subtyping that follows the
inheritance hierarchy. We illustrate this extension using several examples.
3.1 Adding inheritance-based subtyping
Inheritance-based subtyping requires four additions to MOBY's type system, as well as a couple of
changes to the existing rules:
ffl For any class C, we define #C to be its class type, which can be used as a type in any context that
module BagM : {
type Rep <: typeof(Bag)
class Bag : {
public meth add : Int -> Unit
public meth bagRep : Unit -> Rep
public maker mkBag of Unit
val union : (Rep, Rep) -> Unit
{
class Bag {
public field items : var List(Int)
public meth add { self.items := x :: self.items }
public meth bagRep () -> Rep { self }
public maker mkBag () { field items = Nil }
objtype
{
List.app s1.add s2.items
module {
type Rep <: typeof(CBag)
class CBag : {
public meth add : Int -> Unit
public meth bagRep : Unit -> BagM.Rep
public meth size : Unit -> Int
public meth cbagRep : Unit -> Rep
public maker mkCBag of Unit
{
class CBag {
inherits BagM.Bag
public field nItems : var Int
public meth add {
self.nItems := self.nItems+1;
public meth size () -> Int { self.nItems }
public meth cbagRep () -> Rep { self }
public maker mkCBag () { super mkBag(); field nItems
objtype

Figure

3: Bags and friends using representation methods
class B {
public meth m1 () -> Int { . }
public meth m2 .
class C {
{ public meth m2 . }
public meth m1 () -> Bool { . }
maker mkC of Unit { . }

Figure

4: Example of reusing a private method name
is in C's scope. Note that the meaning of a class type depends on its context. Inside a method
body, the class type of the host class allows access to all members, whereas outside the class, only
the public members can be accessed.
ffl We extend class interfaces to allow an optional inherits clause. If in a given context, a class
C has an interface that includes an "inherits B" clause, then we view #C as a subtype of #B.
Omitting the inherits clause from C's interface causes the relationship between B and C to be
hidden.
ffl We say that #C is a subtype of relation corresponds to Fisher's observation
that implementation types are subtypes of interface types [Fis96]).
ffl The existing typing judgements for method and field selection require the argument to have an
object type. We add new judgements for the case where the argument has a class type. We add
new rules, instead adding of subtyping to the existing rules, to avoid a technical problem that is
described in Section 3.2.
ffl When typing the methods of a class C, we give self the type #C (likewise, if B is C's superclass,
then super has the type #B).
ffl When typing a new expression, we assign the corresponding class type to the result.
3.2 Inheritance-based subtyping vs. privacy
There is a potential problem in the Extended MOBY type system that has to do with the interaction of
inheritance-based subtyping and MOBY's support for privacy. Because MOBY allows signature ascription
to hide object members (e.g., the items field in Figure 2), #C can be a subtype of #B even when
typeof(C) is not a subtype of typeof(B). The problem arises in the case where class C has defined
a method that has the same name as one of B's private methods. Consider the code fragment in Figure 4,
for example. 2 Given these definitions, how do we typecheck the expression: "(new mkC()).m1()?"
If we allow subtyping on the left-hand side of the method selection, then there are two incompatible ways
This example uses a class interface annotation on the class B; this syntactic form avoids the need to wrap B in a module
and signature to hide the m2 meth.
module BagM : {
class Bag : {
public meth add : Int -> Unit
public maker mkBag of Unit
val union : (#Bag, #Bag) -> Unit
{
class Bag {
public field items : var List(Int)
public meth add { self.items := x :: self.items }
public maker mkBag () { field items = Nil }
{
List.app s1.add s2.items
module {
class CBag : {
inherits BagM.Bag
public meth size : Unit -> Int
public maker mkCBag of Unit
{
class CBag {
inherits BagM.Bag
public field nItems : var Int
public meth add {
self.nItems := self.nItems+1;
public meth size () -> Int { self.nItems }
public maker mkCBag () { super mkBag(); field nItems

Figure

5: Bags with friends in Extended MOBY
to typecheck this expression. To avoid this ambiguity, we have different rules for the case where the
left-hand side has a class type vs. an object type. 3
3.3 Friends revisited
We can now revisit our bag class example using the inheritance-based subtyping features of Extended
MOBY. In this new implementation (see Figure 5), we use the class type #Bag instead of the Rep
type, which allows us to simplify the code by both eliminating the Rep type and the representation
method. Note that the interface for the CBag class includes an inherits clause that specifies that it is
a subclass of Bag. This relation allows the union function to be used on values that have the #CBag
type.
3 Note that the MOBY typing rules do not include a subsumption rule.
class {
public meth getX : Unit -> Int
public meth clone : Unit -> #B
public maker mkB of Int
maker copyB of #B
{
public meth getX () -> Int { self.pvtX }
public meth clone () -> #B { new copyB(self) }
public maker mkB { field
field
maker { field
class C {
inherits B
public meth clone () -> #C { new copyC(self) }
public maker mkC (y : Int) { super mkB(y) }
maker { super copyB(orig) }

Figure

Cloning with privacy in Extended MOBY
3.4 Binary methods
Binary methods are methods that take another object of the same class as an argument [BCC There
are a number of different flavors of binary methods, depending on how objects from subclasses are
treated. Using class types, we can implement binary methods that require access to the private fields of
their argument objects. For example, the union function in the previous example can be implemented
as a binary method as follows:
class Bag {
field items : var List(Int)
public meth add { self.items := x :: self.items }
public meth union { List.app self.add s.items }
public maker mkBag () { field items = Nil }
Object cloning
Another case where inheritance-based subtyping is useful is in the typing of copy constructors, which
can be used to implement a user-defined object cloning mechanism. 4 Figure 6 gives an example of
cloning in Extended MOBY. Class B has a private field (pvtX), which makes object types insufficient to
type check C's use of the copyB maker function. The problem arises because the object type associated
with self in type-checking C does not have a pvtX field (because that field is private to B), but the
copyB maker function requires one. Thus, we need the inheritance-based subtyping relationship to
allow the copyC maker to pass self, typed with #C, as a parameter to the copyB maker. Because we
4 Note that in MOBY, constructors are called makers.
signature HAS_SHOW {
type InitB
class {
meth show : Unit -> String
maker mk of InitB
module
{
class Pr {
inherits M.B
public meth print () -> Unit { ConsoleIO.print(self.show()) }
maker { super mk(x) }
class A {
public meth show () -> String { "Hi" }
public meth anotherMeth () -> Unit { . }
maker mk () { }
module
class PrA {
inherits P.Pr
public meth anotherMeth () -> Unit { (self : #A).anotherMeth() }

Figure

7: Encoding mixins in Extended MOBY
know that C inherits from B, this application typechecks. We also exploit this subtyping relation when
we override the clone method.
3.6 Encoding mixins
MOBY does not support any form of multiple inheritance, but with the combination of parameterized
modules and class types, it is possible to encode mixins [BC90, FKF98]. In this encoding, a mixin
is implemented as a class parameterized over its base class using a parameterized module. The class
interface of the base class contains only those components that are necessary for the mixin. After
applying the mixin to a particular base class, we create a new class that inherits from the mixed base
class and uses the class types to reconstitute the methods of the base class that were hidden as a result
of the module application. Without class types, it would not be possible to make the original class's
methods visible again. For example, Figure 7 gives the encoding of a mixin class that adds a print
method to a class that has a show method. After applying PrintMix to class A, we define a class PrA
that reconstitutes A's anotherMeth method. Notice that we need to use an explicit type constraint to
convert the type of self from #PrA to #A, since we do not have subtyping at method dispatch.
While this encoding is cumbersome, it illustrates the power of class types. Also, it might serve as
the definition of a derived form that supported mixins directly.
d ::= class C
oe
e ::= x
new C(e)

Figure

8: Syntax of XMOC terms
3.7 Efficiency of method dispatch
Although it is not our main motivation, it is worth noting that method dispatch and field selection from
an object with a class type can be implemented easily as a constant time operation. When the dispatched
method is final in the class type, the compiler can eliminate the dispatch altogether and call the method
directly. In contrast, when an object has an object type, the compiler knows nothing about the layout
of the object, making access more expensive. Even when the exact layout of the class is not known
because of abstraction (e.g., the mixin encoding from the previous section), we can implement dispatch
for objects that have a class type with two memory references and an indirect jump [FRR99].
We have developed a functional object calculus, called XMOC, that models the type system of Extended
MOBY and validates its design. XMOC supports both traditional structural subtyping and inheritance-based
subtyping. In this section, we discuss the intuitions behind XMOC and state subject reduction
results; space considerations preclude a more detailed presentation. The full system is given in Appendices
B and C.
4.1 Syntax
The term syntax of XMOC is given in Figure 8. An XMOC program consists of a sequence of class
declarations terminated by an expression. Class declarations come in two forms. In the first, a class C
can be declared to inherit from a parent class b (when b is None, we say that C is a base-class). The
class is parameterized by x; whenever an object is constructed from C , x is bound to the supplied initial
value. In the second form of class declaration, a class C can be derived from an existing class C 0 by
class-interface ascription, which produces a class that inherits its implementation from C 0 , but has the
more restrictive class interface oe. A class interface gives the type of the class parameter, the name of
the nearest revealed ancestor class (or None), and a typed list of available methods. Types include type
variables, function types, recursive object types, and class types.
In a class declaration, we denote the base class either by the special symbol None or by the name of
the base class applied to an argument. Each method (-) takes a single parameter and has an expression
for its body. The syntax of expressions (e) includes variables, functions, function application, new object
creation, the special variable self (only allowed inside method bodies), and method dispatch. The last
expression form (e @C) is an object-view coercion. Unlike Extended MOBY, XMOC does not map
the inheritance relation directly to the subtyping relation; instead we rely on object-view coercions to
explicitly coerce the type of an expression from a class to one of its superclasses. This approach avoids
the problem discussed in Section 3.2 without requiring two typing judgements for method dispatch. It
is possible to automatically insert these coercions into the XMOC representation of a program as part
of typechecking (such a translation is similar to the type-directed representation wrapping that has been
done for polymorphic languages [Ler92]).
4.2 Dynamic Semantics
Evaluation of an XMOC program occurs in two phases. The first phase is defined by the class linking
relation, written K; p ae K which takes a dynamic class environment K and links the left-most
class definition in p to produce K 0 . Class linking terminates with a residual expression once all of
the class declarations have been linked. The second phase evaluates the residual expression to a value
(assuming termination). This phase is defined by the expression evaluation relation, which we write as
Defining the semantics of linking and evaluation requires extending the term syntax with
run-time forms.
Correctly handling class-interface ascription provides the greatest challenge in defining the semantics
for XMOC. Using this mechanism, a public method m in B can be made private in a subclass C ,
and subsequently m can be reused to name an unrelated method in some descendant class of C (recall
the example in Figure 4). Methods inherited from B must invoke the original m method when they
send the m message to self, while methods defined in D must get the new version. One solution to
this problem is to use Riecke-Stone dictionaries in the semantics [RS98, FR99b]. Dictionaries provide
the ff-conversion needed to avoid capture by mapping method names to slots. For XMOC, we use a
related technique, which we call views. When we process a class C , we tag each method newly defined
in C with the label C , using the notation C :: -. Inherited and overridden methods retain their existing
labels. Furthermore, we replace each occurrence of self in C's new and overridden methods with
the object view self @C . Rule 4 in Appendix B describes this annotation formally. At runtime, we
represent each object as a pair of a raw object (denoted by meta-variable obj ) and a view (denoted by
a class name). The raw object contains the list of annotated methods implemented by the object. The
view represents the visibility context in which the message send occurs; those methods in scope in class
C are available. With this information, we check two conditions when we lookup method m in runtime
object hobj ; Ci: first, that m is in the list of methods provided by obj , and second, that C descends from
the class annotating the m method. If these two conditions are met, we return the associated method
otherwise, we search in the portion of the object inherited from its base class. Rules 1 and 2 in


Appendix

formally specify method lookup.
4.3 Static semantics
The XMOC typing judgements are written with respect to a static environment \Gamma, which consists of a
set of bound type variables (A), a subtype assumption map (S), a class environment (C), and a variable
environment (V). The definition of these environments and the complete set of XMOC typing
judgements are given in Appendix C. Here we briefly discuss some of the more important rules.
As mentioned earlier, each XMOC class name doubles as an object type. We associate such a type
with an object whenever we instantiate an object from a class, according to the typing rule
(C of \Gamma)(C
new C(e) . #C
which looks up class C in \Gamma, infers a type - 0 for the constructor argument e, and insures that this type is
a subtype of the type of the class parameter - .
In contexts that allow subtyping, we can treat a class type as an object type according to the following
subtyping judgement:
This rule corresponds to the property that #C is a subtype of typeof(C) in Extended MOBY. Note that
ff cannot occur free in the types - m , but the object type obj is subject to recursive
winding and unwinding.
Unlike Extended MOBY, we do not treat a class type #C as being a subtype of its superclass type.
Instead we use an object view constraint, which is typed as follows:
Because we do not treat inheritance directly as subtyping in XMOC, we only need one rule for typing
method dispatch.
4.4 Subject reduction
We have proven subject reduction theorems for XMOC. The first states that the linking relation produces
a dynamic class environment that is consistent with the static environment defined by the program, and
that linking does not change the type of the program.
Theorem 1 If (fg; fg; fg; fg) ' p . \Gamma; - and fg; p ae   K; e, then \Gamma ' K and \Gamma; K ' e .
The second theorem states that a well-typed expression evaluations to an expression with a compatible
type.
Theorem
We say that a program p yields the value w and K, if there exists an expression e such that
Given this definition, we can characterize the complete evaluation of a program.
Theorem 3 If (fg; fg; fg; fg) ' p . \Gamma; - and p yields w and K, then \Gamma; K ' w . - 0 with
5 Related work
Our class types are motivated by the r-ole that classes play in languages like C ++ and JAVA. The main
difference between Extended MOBY and the class types provided by these other languages is in the
way that abstraction is supported. Extended MOBY allows partial hiding of inherited components using
signature ascription, which means that typeof(C) may not be a subtype of typeof(B) even when
C is known to inherit from B (see Section 3.2). A related mechanism is C ++ 's private inheritance, which
allows a subclass to inherit from a base class while hiding the inherited members and concealing the
subtyping relationship. Extended MOBY is more flexible, since it allows hiding on a per-member basis.
Extended MOBY also allows the class hierarchy to be hidden by omitting the inherits clause in
class interfaces. In C ++ and JAVA the full class hierarchy is manifest in the class types (except for classes
related using C ++ 's private inheritance). Another point of difference is that Extended MOBY supports
structural subtyping on object types; JAVA has object types (called interfaces), but subtyping is by-name.
C ++ does not have an independent notion of object type.
Fisher's Ph.D. dissertation [Fis96] is the earliest formalization of class types that we are aware of.
In her work, each class is tagged with a row variable using a form of bounded existential row. In our
work, we adopt classes as a primitive notion and use the names of such classes in a fashion analogous
to Fisher's row variables. A weakness of the earlier work is its treatment of private names; it provides
no way to hide a method and then later add an unrelated method with the same name.
Our use of class names to label methods in an object value in XMOC (see Appendix B) is similar
to the use of role tags on methods in Ghelli and Palmerini's calculus for modeling objects with
roles [GP99]. Likewise, our pairing of an object's state with the class name that defines the current view
of the object is similar to their representation of object values. The main difference between XMOC
and their calculus is in the surface language features being modeled.
More recently, Igarashi et al. have described Featherweight Java, which is an object calculus designed
to model the core features of JAVA's type system [IPW99]. Like our calculus, Featherweight Java
has a notion of subtyping based on class inheritance. Our calculus is richer, however, in a number of
ways. Our calculus models private members and narrowing of class interfaces. We also have a notion
of structural subtyping and we relate the implementation and structural subtyping notions.
The notion of type identity based on implementation was present in the original definition of Standard
ML in the form of structure sharing [MTH90]. The benefits of structure sharing were fairly limited
and it was dropped in the 1997 revision of SML [MTHM97].
6 Conclusion
This paper presents an extension to MOBY that supports classes as types. We have illustrated the utility
of this extension with a number of examples. We have also developed a formal model of this extension
and have proven subject reduction for it. We are continuing to work on improving our formal treatment
of class types and implementation-based inheritance. 5 One minor issue is that XMOC requires that
5 Since this paper was written, we have developed a more elegant treatment of XMOC based on Riecke-Stone dictionaries
and have proven type soundness. A paper describing this revised system is available on the MOBY web page
(http://www.cs.bell-labs.com/-jhr/moby).
class names be unique in a program; this restriction can be avoided by introducing some mechanism,
such as stamps, to distinguish top-level names (e.g., see Leroy's approach to module system semantics
[Ler96]). We would also like to generalize the rule that relates class types with object types (rule
in

Appendix

C) to allow positive occurrences of #C to be replaced by the object type's bound type
variable. While we believe that this generalization is sound, we have not yet proven it.



--R

The Java Programming Language.

The Hopkins Object Group
Type Systems for Object-oriented Programming Languages
Classes and mixins.
The design of a class mechanism for Moby.
Foundations for MOBY classes.
A calculus for compiling and linking classes.
Foundations for extensible objects with roles.
Featherweight Java: A minimal core calculus for Java and GJ.
A type system for prototyping languages.
Unboxed objects and polymorphic typing.
A syntactic theory of type generativity and sharing.
The Definition of Standard ML.
The Definition of Standard ML - Revised <Year>1997</Year>
Statically typed friendly functions via partially abstract types.
Privacy via subsumption.

--TR
Mixin-based inheritance
Unboxed objects and polymorphic typing
A type system for prototyping languages
On binary methods
Classes and mixins
The Java programming language (2nd ed.)
The design of a class mechanism for Moby
Featherwieght Java
The C++ Programming Language, Third Edition
The Definition of Standard ML
The Definition of Standard ML
Type systems for object-oriented programming languages
inheritance;type theory;programming languages;object-orientation;subtyping