Classes and Mixins

Matthew Flatt Shriram Krishnamurthi Matthias Felleisen

Department of Computer Science^{∗} Rice University

Houston, Texas 77005-1892

Abstract

While class-based object-oriented programming languages provide a flexible mechanism for re-using and managing related pieces of code, they typically lack linguistic facilities for specifying a uniform extension of many classes with one set of fields and methods. As a result, programmers are unable to express certain abstractions over classes.

In this paper we develop a model of class-to-class functions that we refer to as mixins. A mixin function maps a class to an extended class by adding or overriding fields and methods. Programming with mixins is similar to programming with single inheritance classes, but mixins more directly encourage programming to interfaces.

The paper develops these ideas within the context of Java. The results are

1. an intuitive model of an essential Java subset;

2. an extension that explains and models mixins; and

3. type soundness theorems for these languages.

1 Organizing Programs with Functions and Classes

Object-oriented programming languages offer classes, inheritance, and overriding to parameterize over program pieces for management purposes and re-use. Functional programming languages provide various flavors of functional abstractions for the same purpose. The latter model was developed from a well-known, highly developed mathematical theory. The former grew in response to the need to manage large programs and to re-use as many components as possible.

Each form of parameterization is useful for certain situations. With higher-order functions, a programmer can easily define many functions that share a similar core but differ in a few details. As many language designers and programmers readily acknowledge, however, the functional approach to parameterization is best used in situations with a relatively small number of parameters. When a function must

To appear: POPL – January 1998, San Diego, CA consume a large number of arguments, the approach quickly becomes unwieldy, especially if many of the arguments are the same for most of the function’s uses.^{1}

Class systems provide a simple and flexible mechanism for managing collections of highly parameterized program pieces. Using class extension (inheritance) and overriding, a programmer derives a new class by specifying only the elements that change in the derived class. Nevertheless, a pure class-based approach suffers from a lack of abstractions that specify uniform extensions and modifications of classes. For example, the construction of a programming environment may require many kinds of text editor frames, including frames that can contain multiple text buffers and frames that support searching. In Java, for example, we cannot implement all combinations of multiple-buffer and searchable frames using derived classes. If we choose to define a class for all multiple-buffer frames, there can be no class that includes only searchable frames. Hence, we must repeat the code that connects a frame to the search engine in at least two branches of the class hierarchy: once for single-buffer searchable frames and again for multiple-buffer searchable frames. If we could instead specify a mapping from editor frame classes to searchable editor frame classes, then the code connecting a frame to the search engine could be abstracted and maintained separately.

Some class-based object-oriented programming languages provide multiple inheritance, which permits a programmer to create a class by extending more than one class at once. A programmer who also follows a particular protocol for such extensions can mimic the use of class-to-class functions. Common Lisp programmers refer to this protocol as mixin programming [21, 22], because it roughly corresponds to mixing in additional ingredients during class creation. Bracha and Cook [6] designed a language of class manipulators that promote mixin thinking in this style and permit programmers to build mixin-like classes. Unfortunately, multiple inheritance and its cousins are semantically complex and difficult to understand for programmers.^{2} As a result, implementing a mixin protocol with these approaches is error-prone and typically avoided.

For the design of MzScheme’s class and interface system [15], we experimented with a different approach. In MzScheme, classes form a single inheritance hierarchy, but are also first-class values that can be created and extended at run-time. Once this capability was available, the program-

∗This research was partially supported by a NSF Graduate Research Fellowship, NSF grants CCR-9619756, CDA-9713032, and CCR-9708957, and a Texas ATP grant.

1Function entry points à la Fortran or keyword arguments à la Common Lisp are a symptom of this problem, not a remedy.

2Dan Friedman determined in an informal poll in 1996 that almost nobody who teaches C++ teaches multiple inheritance [pers. com.].

interface Place^{i} … interface Barrier^{i} … interface Door^{i} extends Place^{i}, Barrier^{i} … … class Door^{c} extends Object implements Door^{i} {

… Room^{c} Enter(Person^{c} p) { … } … } class LockedDoor^{c} extends Door^{c} … class ShortDoor^{c} extends Door^{c} … ⇒ Place^{i} … Barrier^{i} …

(Door^{i}) / …

… …

Interfaces

[figure] [figure]

Object / …

…

[figure]

… Door^{c}

Enter …

LockedDoor^{c} …

…

…

ShortDoor^{c} …

[figure]

… …

Classes

[figure]

Figure 1: A program determines a static directed acyclic graph of types

[figure: ⊢; ⟨; player:; Person^{c}; room:; Room^{c}; door:; LockedDoor^{c}; …; …; ,; door.Enter(player); ⟩; ↪^{∗}; ⟨; player:; Person^{c}; room:; Room^{c}; door:; LockedDoor^{c}; …; …; ,; room; ⟩]

Figure 2: In the context of a type graph, reductions map a store-expression pair to a new store-expression pair

mers of our team used it extensively for the construction of DrScheme [14], a Scheme programming environment. However, a thorough analysis reveals that the code only contains first-order functions on classes.

In this paper, we present a typed model of such “class functors” for Java [18]. We refer to the functors as mixins due to their similarity to Common Lisp’s multiple inheritance mechanism and Bracha’s class operators. Our proposal is superior in that it isolates the useful aspects of multiple inheritance yet retains the simple, intuitive nature of class-oriented Java programming. In the following section, we develop a calculus of Java classes. In the third section, we motivate mixins as an extension of classes using a small but illuminating example. The fourth section extends the type-theoretic model of Java to mixins. The last section considers implementation strategies for mixins and puts our work in perspective.

2 A Model of Classes

ClassicJava is a small but essential subset of sequential Java. To model its type structure and semantics, we use well-known type elaboration and rewriting techniques for Scheme and ML [13, 19, 29]. Figures 1 and 2 illustrate our strategy. Type elaboration verifies that a program defines a static tree of classes and a directed acyclic graph (dag) of interfaces. A type is simply a node in the combined graph. Each type is annotated with its collection of fields and methods, including those inherited from its ancestors.

Evaluation is modeled as a reduction on expression-store pairs in the context of a static type graph. Figure 2 demonstrates reduction using a pictorial representation of the store as a graph of objects. Each object in the store is a classtagged record of field values, where the tag indicates the run-time type of the object and its field values are references to other objects. A single reduction step may extend the store with a new object, or it may modify a field for an existing object in the store. Dynamic method dispatch is accomplished by matching the class tag of an object in the store with a node in the static class tree; a simple relation on this tree selects an appropriate method for the dispatch.

The class model relies on as few implementation details as possible. For example, the model defines a mathematical relation, rather than a selection algorithm, to associate fields with classes for the purpose of type-checking and evaluation. Similarly, the reduction semantics only assumes that an expression can be partitioned into a proper redex and an (evaluation) context; it does not provide a partitioning algorithm. The model can easily be refined to expose more implementation details [12, 19].

2.1 ClassicJava Programs

The syntax for ClassicJava is shown in Figure 3. A program P is a sequence of class and interface definitions followed by an expression. Each class definition consists of a sequence of field declarations and a sequence of method declarations, while an interface consists of methods only. A method body in a class can be abstract, indicating that the method must be overridden in a subclass before the class is instantiated. A method body in an interface must be abstract. As in Java, classes are instantiated with the new operator, but there are no class constructors in Classic-Java; instance variables are always initialized to null. In the evaluation language for ClassicJava, field uses and super invocations are annotated by the type-checker with extra in-

P = defn* e
defn = class c extends c implements i* { field* meth* }

| interface i extends i* { meth* }

field = t fd
meth = t md ( arg* ) { body }
arg = t var
body = e | abstract
e = new c | var | null | e \underline{: c} .fd | e \underline{: c} .fd = e

| e.md (e* ) | super \underline{≡ this : c} .md (e* ) | view t e | let var = e in e

var = a variable name or this
c = a class name or Object
i = interface name or Empty
fd = a field name
md = a method name
t = c | i

Figure 3: ClassicJava syntax; underlined phrases are inserted by elaboration and are not part of the surface syntax

formation (see the underlined parts of the syntax). Finally, the view and let forms represent Java’s casting expressions and local variable bindings, respectively.

A valid ClassicJava program satisfies a number of simple predicates and relations; these are described in Figure 4. For example, the predicate ClassesOnce(P) states that each class name is defined at most once in the program P. The relation ≺^{c}_{P} associates each class name in P to the class it extends, and the (overloaded) ∈ ∈^{c}_{P} relations capture the field and method declarations of P.

The syntax-summarizing relations induce a second set of relations and predicates that summarize the class structure of a program. The first of these is the subclass relation ≤^{c}_{P}, which is a partial order if the CompleteClasses(P) and WellFoundedClasses(P) predicates hold. In this case, the classes declared in P form a tree that has Object at its root.

If the program describes a tree of classes, we can “decorate” each class in the tree with the collection of fields and methods that it accumulates from local declarations and inheritance. The source declaration of any field or method in a class can be computed by finding the minimum (i.e., farthest from the root) superclass that declares the field or method. This algorithm is described precisely by the ∈^{c}_{P} relations. The ∈^{c}_{P} relation retains information about the source class of each field, but it does not retain the source class for a method. This reflects the property of Java classes that fields cannot be overridden (so instances of a subclass always contain the field), while methods can be overridden (and may become inaccessible).

Interfaces have a similar set of relations: the superinterface declaration relation ≺^{i}_{P} induces a subinterface relation ≤^{i}_{P}. Unlike classes, a single interface can have multiple proper superinterfaces, so the subinterface order forms a dag instead of a tree. The methods of an interface, as described by ∈^{i}_{P}, are the union of the interface’s declared methods and the methods of its superinterfaces.

Finally, classes and interfaces are related by implements declarations, as captured in the ≺ ≺^{c}_{P} relation. This relation is a set of edges joining the class tree and the interface graph, completing the subtype picture of a program. A type in the full graph is a subtype of all of its ancestors.

2.2 ClassicJava Type Elaboration

The type elaboration rules for ClassicJava are defined by the following judgements:

⊢_{p} P ⇒ P′ : t P elaborates to P′ with type t
P ⊢_{d} defn ⇒ defn′ defn elaborates to defn′
P, t ⊢_{m} meth ⇒ meth′ meth in t elaborates to meth′
P, Γ ⊢_{e} e ⇒ e′ : t  e elaborates to e′ with type t
P, Γ ⊢_{s} e ⇒ e′ : t  e has type t using subsumption
P ⊢_{t} t  t exists

The type elaboration rules translate expressions that access a field or call a super method into annotated expressions (see the underlined parts of Figure 3). For field uses, the annotation contains the compile-time type of the instance expression, which determines the class containing the declaration of the accessed field. For super method invocations, the annotation contains the compile-time type of this, which determines the class that contains the declaration of the method to be invoked.

The complete typing rules are shown in Figure 5. A program is well-typed if its class definitions and final expression are well-typed. A definition, in turn, is well-typed when its field and method declarations use legal types and the method body expressions are well-typed. Finally, expressions are typed and elaborated in the context of an environment that binds free variables to types. For example, the get^{c} and set^{c} rules for fields first determine the type of the instance expression, and then calculate a class-tagged field name using ∈_{P}; this yields both the type of the field and the class for the installed annotation. In the set^{c} rule, the right-hand side of the assignment must match the type of the field, but this match may exploit subsumption to coerce the type of the value to a supertype. The other expression typing rules are similarly intuitive.

2.3 ClassicJava Evaluation

The operational semantics for ClassicJava is defined as a contextual rewriting system on pairs of expressions and stores. A store S is a mapping from objects to class-tagged field records. A field record is a mapping from elaborated field names to values. The evaluation rules are a straightforward modification of those for imperative Scheme [13].

The complete evaluation rules are in Figure 6. For example, the call rule invokes a method by rewriting the method call expression to the body of the invoked method, syntactically replacing argument variables in this expression with the supplied argument values. The dynamic aspect of method calls is implemented by selecting the method based on the run-time type of the object (in the store). In contrast, the super reduction performs super method selection using the class annotation that is statically determined by the type-checker.

2.4 ClassicJava Soundness

For a program of type t, the evaluation rules for Classic-Java produce either a value that has a subtype of t, or one of two errors. Put differently, an evaluation cannot get stuck. This property can be formulated as a type soundness theorem.

ClassesOnce(P)  Each class name is declared only once
∀c,c′ class c ⋯ class c′ ⋯ is in P ⟹ c ≠ c′
FieldOncePerClass(P)  Field names in each class declaration are unique
∀fd,fd′ class ⋯ { ⋯ fd ⋯ fd′ ⋯ } is in P ⟹ fd ≠ fd′
MethodOncePerClass(P)  Method names in each class declaration are unique
∀md,md′ class ⋯ { ⋯ md ( ⋯) { ⋯ } ⋯ md′ ( ⋯) { ⋯ } ⋯ } is in P ⟹ md ≠ md′
InterfacesOnce(P)  Each interface name is declared only once

∀i,i′ interface i ⋯ interface i′ ⋯ is in P ⟹ i ≠ i′

InterfacesAbstract(P)  Method declarations in an interface are abstract
∀md,e interface ⋯ { ⋯ md ( ⋯) {e} ⋯ } is in P ⟹ e is abstract
≺^{c}_{P}  Class is declared as an immediate subclass
c ≺^{c}_{P} c′ ⇔ class c extends c′ ⋯ { ⋯ } is in P
∈ ∈^{c}_{P}  Field is declared in a class
⟨c.fd, t⟩ ∈ ∈^{c}_{P} c ⇔ class c ⋯ { ⋯ t fd ⋯ } is in P
∈ ∈^{c}_{P}  Method is declared in class
⟨md, (t_{1} … t_{n} ⟶ t), (var_{1} … var_{n}), e⟩ ∈ ∈^{c}_{P} c ⇔ class c ⋯ { ⋯ t md (t_{1} var_{1} … t_{n} var_{n}) {e} ⋯ } is in P
≺^{i}_{P}  Interface is declared as an immediate subinterface

i ≺^{i}_{P} i′ ⇔ interface i extends ⋯ i′ ⋯ { ⋯ } is in P

∈ ∈^{i}_{P}  Method is declared in an interface

⟨md, (t_{1} … t_{n} ⟶ t), (var_{1} … var_{n}), e⟩ ∈ ∈^{i}_{P} i ⇔ interface i ⋯ { ⋯ t md (t_{1} var_{1} … t_{n} var_{n}) {e} ⋯ } is in P

≺ ≺^{c}_{P}  Class declares implementation of an interface

c ≺ ≺^{c}_{P} i ⇔ class c ⋯ implements ⋯ i ⋯ { ⋯ } is in P

≤^{c}_{P}  Class is a subclass

≤^{c}_{P} ≡ the transitive, reflexive closure of ≺^{c}_{P}

CompleteClasses(P)  Classes that are extended are defined

rng(≺^{c}_{P}) ⊆ dom(≺^{c}_{P})∪{Object}

WellFoundedClasses(P)  Class hierarchy is an order

≤^{c}_{P} is antisymmetric

ClassMethodsOK(P)  Method overriding preserves the type

∀c,c′,e,e′,md, T, T′, V, V′ (⟨md, T, V, e⟩ ∈ ∈^{c}_{P} c and ⟨md, T′, V′, e′⟩ ∈ ∈^{c}_{P} c′) ⟹ (T = T′ or c ≰^{c}_{P} c′)

∈^{c}_{P}  Field is contained in a class

⟨c′.fd, t⟩ ∈^{c}_{P} c ⇔ ⟨c′.fd, t⟩ ∈ ∈^{c}_{P} c′ and c′ = min{c′′ | c ≤^{c}_{P} c′′ and ∃t′ s.t. ⟨c′′.fd, t′⟩ ∈ ∈^{c}_{P} c′′}

∈^{c}_{P}  Method is contained in a class

⟨md, T, V, e⟩ ∈^{c}_{P} c ⇔ (⟨md, T, V, e⟩ ∈ ∈^{c}_{P} c′ and c′ = min{c′′ | c ≤^{c}_{P} c′′ and ∃e′, V′ s.t. ⟨md, T, V′, e′⟩ ∈ ∈^{c}_{P} c′′})

≤^{i}_{P}  Interface is a subinterface
≤^{i}_{P} ≡ the transitive, reflexive closure of ≺^{i}_{P}
CompleteInterfaces(P)  Extended/implemented interfaces are defined
rng(≺^{i}_{P}) ∪ rng(≺ ≺^{c}_{P}) ⊆ dom(≺^{i}_{P})∪{Empty}
WellFoundedInterfaces(P) Interface hierarchy is an order
≤^{i}_{P} is antisymmetric
≪^{c}_{P}  Class implements an interface
c ≪^{c}_{P} i ⇔ ∃c′,i′ s.t. c ≤^{c}_{P} c′ and i′ ≤^{i}_{P} i and c′ ≺ ≺^{c}_{P} i′
InterfaceMethodsOK(P)  Redeclarations of methods are consistent
∀i,i′,md, T, T′, V, V′ ⟨md, T, V, abstract⟩ ∈ ∈^{i}_{P} i and ⟨md, T′, V′, abstract⟩ ∈ ∈^{i}_{P} i′ ⟹ (T = T′ or i ≰^{i}_{P} i′)
∈^{i}_{P}  Method is contained in an interface
⟨md, T, V, abstract⟩ ∈^{i}_{P} i ⇔ ∃i′ s.t. i ≤^{i}_{P} i′ and ⟨md, T, V, abstract⟩ ∈ ∈^{i}_{P} i′
ClassesImplementAll(P)  Classes supply methods to implement interfaces
∀i,c c ≺ ≺^{c}_{P} i ⟹ (∀md, T, V ⟨md, T, V, abstract⟩ ∈^{i}_{P} i ⟹ ∃e, V′ s.t. ⟨md, T, V′, e⟩ ∈^{c}_{P} c)
NoAbstractMethods(P, c)  Class has no abstract methods (can be instantiated)
∀md, T, V,e ⟨md, T, V, e⟩ ∈^{c}_{P} c ⟹ e ≠ abstract
≤_{P}  Type is a subtype
≤_{P} ≡ ≤^{c}_{P} ∪ ≤^{i}_{P} ∪ ≪^{c}_{P}
∈_{P}  Field or method is in a type
∈_{P} ≡ ∈^{c}_{P} ∪ ∈^{i}_{P}

The sets of names for variables, classes, interfaces, fields, and methods are assumed to be mutually distinct. The meta-variable T is used for method signatures of the form (t … ⟶ t), V is used for variable lists of the form (var…), and Γ is used for environments mapping variables to types. Ellipses on the baseline (…) indicate a repeated pattern or continued sequence, while centered ellipses (⋯) indicate arbitrary missing program text (without straddling a class or interface definition).

Figure 4: Predicates and relations in the model of ClassicJava

Theorem: If ⊢_{p} P ⇒ P′ : t and

P′ = defn_{1} … defn_{n} e, then either

• P′ ⊢ ⟨e, ∅⟩ ↪^{∗} ⟨object, S⟩ and S(object) = ⟨t′, F⟩ and t′ ≤_{P} t;

• P′ ⊢ ⟨e, ∅⟩ ↪^{∗} ⟨null, S⟩;

• P′ ⊢ ⟨e, ∅⟩ ↪^{∗} ⟨error: bad cast, S⟩; or

• P′ ⊢ ⟨e, ∅⟩ ↪^{∗} ⟨error: dereferenced null, S⟩. The main lemma in support of this theorem states that each step taken in the evaluation preserves the type correctness of the expression-store pair (relative to the program) [29]. Specifically, for a configuration on the left-hand side of an evaluation step, there exists a type environment that establishes the expression’s type as some t. This environment must be consistent with the store:

P, Γ ⊢_{σ} S

⇔ (S(object) = ⟨c, F⟩

⇒ Γ(object) = c and dom(F) = {c_{1}.fd | ⟨c_{1}.fd, c_{2}⟩ ∈^{c}_{P} c_{1}} and rng(F) ⊆ dom(S) ∪ {null} and (F(c_{1}.fd) = object′ and ⟨c_{1}.fd, c_{2}⟩ ∈^{c}_{P} c_{1})

⇒ (S(object′) = ⟨c′, F′⟩ ⇒ c′ ≤_{P} c_{2}))

and object ∈ dom(Γ) ⇒ object ∈ dom(S)

and dom(S) ⊆ dom(Γ)

⊢_{p}

ClassesOnce(P)  InterfacesOnce(P)  MethodOncePerClass(P)  FieldOncePerClass(P)
CompleteClasses(P) WellFoundedClasses(P) CompleteInterfaces(P) WellFoundedInterfaces(P)
ClassFieldsOK(P) ClassMethodsOK(P)  InterfaceMethodsOK(P)  InterfacesAbstract(P)
ClassesImplementAll(P)  P ⊢_{d} defn_{j} ⇒ defn′_{j} for j ∈ [1, n]  P, [ ] ⊢_{e} e ⇒ e′ : t
where P = defn_{1} … defn_{n} e
⊢_{p} defn_{1} … defn_{n} e ⇒ defn′_{1} … defn′_{n} e′ : t

[prog^{c}]

⊢_{d}

\frac{P ⊢_{t} t_{j} for each j ∈ [1, n]  P, c ⊢_{m} meth_{k} ⇒ meth′_{k} for each k ∈ [1, p]}{P ⊢_{d} class c ⋯ \{ t_{1} fd_{1} … t_{n} fd_{n} meth_{1} … meth_{p} \} ⇒ class c ⋯ \{ t_{1} fd_{1} … t_{n} fd_{n} meth′_{1} … meth′_{p} \}} [defn^{c}]

\frac{P, i ⊢_{m} meth_{j} ⇒ meth′_{j} for each j ∈ [1, p]}{P ⊢_{d} interface i ⋯ \{ meth_{1} … meth_{p} \} ⇒ interface i ⋯ \{ meth′_{1} … meth′_{p} \}} [defn^{i}]

⊢_{m}

\frac{P ⊢_{t} t  P ⊢_{t} t_{j} for j ∈ [1, n]  P,[this : t_{o}, var_{1} : t_{1}, … var_{n} : t_{n}] ⊢_{s} e ⇒ e′ : t}{P, t_{o} ⊢_{m} t md (t_{1} var_{1} … t_{n} var_{n}) \{ e \} ⇒ t md (t_{1} var_{1} … t_{n} var_{n}) \{ e′ \}} [meth]

⊢_{e}

\frac{P ⊢_{t} c  NoAbstractMethods(P, c)}{P, Γ ⊢_{e} new c ⇒ new c : c} [new^{c}] \frac{where var ∈ dom(Γ)}{P, Γ ⊢_{e} var ⇒ var : Γ(var)} [var] \frac{P ⊢_{t} t}{P, Γ ⊢_{e} null ⇒ null : t} [null]

\frac{P, Γ ⊢_{e} e ⇒ e′ : t′  ⟨c.fd, t⟩ ∈_{P} t′}{P, Γ ⊢_{e} e.fd ⇒ e′ \underline{: c} .fd : t} [get^{c}]  \frac{P, Γ ⊢_{e} e ⇒ e′ : t′  ⟨c.fd, t⟩ ∈_{P} t′  P, Γ ⊢_{s} e_{v} ⇒ e′_{v} : t}{P, Γ ⊢_{e} e.fd = e_{v} ⇒ e′ \underline{: c} .fd = e′_{v} : t} [set^{c}]

\frac{P, Γ ⊢_{e} e ⇒ e′ : t′  ⟨md, (t_{1} … t_{n} ⟶ t), (var_{1} … var_{n}), e_{b}⟩ ∈_{P} t′ P, Γ ⊢_{s} e_{j} ⇒ e′_{j} : t_{j} for j ∈ [1, n]}{P, Γ ⊢_{e} e.md (e_{1} … e_{n}) ⇒ e′.md (e′_{1} … e′_{n}) : t} [call^{c}]

\frac{P, Γ ⊢_{e} this ⇒ this : c′  c′ ≺^{c}_{P} c  ⟨md, (t_{1} … t_{n} ⟶ t), (var_{1} … var_{n}), e_{b}⟩ ∈_{P} c P, Γ ⊢_{s} e_{j} ⇒ e′_{j} : t_{j} for j ∈ [1, n]  e_{b} ≠ abstract}{P, Γ ⊢_{e} super.md(e_{1} … e_{n}) ⇒ super \underline{≡ this : c} .md(e′_{1} … e′_{n}) : t} [super^{c}]

\frac{P, Γ ⊢_{s} e ⇒ e′ : t}{P, Γ ⊢_{e} view t e ⇒ e′ : t} [wcast^{c}]  \frac{P, Γ ⊢_{e} e ⇒ e′ : t′  t ≤_{P} t′ or t ∈ dom(≺^{i}_{P}) or t′ ∈ dom(≺^{i}_{P})}{P, Γ ⊢_{e} view t e ⇒ view t e′ : t} [ncast^{c}]

\frac{P, Γ ⊢_{e} e_{1} ⇒ e′_{1} : t_{1}  P, Γ[var : t_{1}] ⊢_{e} e_{2} ⇒ e′_{2} : t}{P, Γ ⊢_{e} let var = e_{1} in e_{2} ⇒ let var = e′_{1} in e′_{2} : t} [let] \frac{P ⊢_{t} t}{P, Γ ⊢_{e} abstract ⇒ abstract : t} [abs]

⊢_{s}, ⊢_{t}

\frac{P, Γ ⊢_{e} e ⇒ e′ : t′  t′ ≤_{P} t}{P, Γ ⊢_{s} e ⇒ e′ : t} [sub^{c}]  \frac{t ∈ dom(≺^{c}_{P}) ∪ dom(≺^{i}_{P})∪\{Object, Empty\}}{P ⊢_{t} t} [type^{c}]

Figure 5: Context-sensitive checks and type elaboration rules for ClassicJava

An evaluation step yields one of two possible configurations: either a well-defined error state or a new expression-store pair. In the latter case, there exists a new type environment that is consistent with the new store, and it establishes that the new expression has a type below t. A complete proof is available in an extended version of the paper [16].

2.5 Related Work on Classes

Our model for class-based object-oriented languages is similar to two recently published semantics for Java [9, 28], but entirely motivated by prior work on Scheme and ML models [13, 19, 29]. The approach is fundamentally different from most of the previous work on the semantics of objects. Much of that work has focused on interpreting object systems and the underlying mechanisms via record extensions of lambda calculi [11, 20, 24, 23, 25] or as “native” object calculi (with a record flavor) [1, 2, 3]. In our semantics, types are simply the names of entities declared in the program; the collection of types forms a dag, which is specified by the programmer. The collection of types is static during evaluation^{3} and is only used for field and method lookups and casts. The evaluation rules describe how to transform statements, formed over the given type context, into plain values. The rules work on plain program text such that each intermediate stage of the evaluation is a complete program. In short, the model is as simple and intuitive as that of firstorder functional programming enriched with a language for expressing hierarchical relationships among data types.

3Dynamic class loading could be expressed in this framework as an addition to the static context. Still, the context remains the same for most of the evaluation.

e = … | object
v = object | null

E = [ ] | E \underline{: c} .fd | E \underline{: c} .fd = e | v \underline{: c} .fd = E
| E.md(e …) | v.md(v … E e …)
| super \underline{≡ v : c} .md(v … E e …)
| view t E | let var = E in e
P ⊢ ⟨E[new c], S⟩ ↪ ⟨E[object], S[object↦⟨c, {c′.fd↦null | c ≤^{c}_{P} c′ and ∃t s.t. ⟨c′.fd, t⟩ ∈ ∈^{c}_{P} c′}⟩]⟩ [new]

where object ∉ dom(S)

P ⊢ ⟨E[object \underline{: c′} .fd], S⟩ ↪ ⟨E[v], S⟩  [get]

where S(object) = ⟨c, F⟩ and F(c′.fd) = v

P ⊢ ⟨E[object \underline{: c′} .fd = v], S⟩ ↪ ⟨E[v], S[object↦⟨c, F[c′.fd↦v]⟩]⟩  [set]

where S(object) = ⟨c, F⟩

P ⊢ ⟨E[object.md(v_{1}, … v_{n})], S⟩ ↪ ⟨E[e[object/this, v_{1}/var_{1}, … v_{n}/var_{n}]], S⟩  [call]

where S(object) = ⟨c, F⟩ and ⟨md, (t_{1} … t_{n} ⟶ t), (var_{1} … var_{n}), e⟩ ∈^{c}_{P} c

P ⊢ ⟨E[super \underline{≡ object : c′} .md(v_{1}, … v_{n})], S⟩ ↪ ⟨E[e[object/this, v_{1}/var_{1}, … v_{n}/var_{n}]], S⟩  [super]

where ⟨md, (t_{1} … t_{n} ⟶ t), (var_{1} … var_{n}), e⟩ ∈^{c}_{P} c′

P ⊢ ⟨E[view t′ object], S⟩ ↪ ⟨E[object], S⟩  [cast]

where S(object) = ⟨c, F⟩ and c ≤_{P} t′

P ⊢ ⟨E[let var = v in e], S⟩ ↪ ⟨E[e[v/var]], S⟩  [let]
P ⊢ ⟨E[view t′ object], S⟩ ↪ ⟨error: bad cast, S⟩  [xcast]

where S(object) = ⟨c, F⟩ and c ≰_{P} t′

P ⊢ ⟨E[null \underline{: c} .fd], S⟩ ↪ ⟨error: dereferenced null, S⟩  [nget]
P ⊢ ⟨E[null \underline{: c} .fd = v], S⟩ ↪ ⟨error: dereferenced null, S⟩  [nset]
P ⊢ ⟨E[null.md(v_{1}, … v_{n})], S⟩ ↪ ⟨error: dereferenced null, S⟩  [ncall]

Figure 6: Operational semantics for ClassicJava

3 From Classes to Mixins: An Example

Implementing a maze adventure game [17, page 81] illustrates the need for adding mixins to a class-based language. A player in the adventure game wanders through rooms and doors in a virtual world. All locations in the virtual world share some common behavior, but also differ in a wide variety of properties that make the game interesting. For example, there are many kinds of doors, including locked doors, magic doors, doors of varying heights, and doors that combine several varieties into one. The natural class-based approach for implementing different kinds of doors is to implement each variation with a new subclass of a basic door class, Door^{c}. The left side of Figure 7 shows the Java definition for two simple Door^{c} subclasses, LockedDoor^{c} and ShortDoor^{c}. An instance of LockedDoor^{c} requires a key to open the door, while an instance of ShortDoor^{c} requires the player to duck before walking through the door.

A subclassing approach to the implementation of doors seems natural at first because the programmer declares only what is different in a particular door variation as compared to some other door variation. Unfortunately, since the superclass of each variation is fixed, door variations cannot be composed into more complex, and thus more interesting, variations. For example, the LockedDoor^{c} and ShortDoor^{c} classes cannot be combined to create a new LockedShortDoor^{c} class for doors that are both locked and short.

A mixin approach solves this problem. Using mixins, the programmer declares how a particular door variation differs from an arbitrary door variation. This creates a function from door classes to door classes, using an interface as the input type. Each basic door variation is defined as a separate mixin. These mixins are then functionally composed to create many different kinds of doors.

A programmer implements mixins in exactly the same way as a derived class, except that the programmer cannot rely on the implementation of the mixin’s superclass, only on its interface. We consider this an advantage of mixins because it enforces the maxim “program to an interface, not an implementation” [17, page 11].

The right side of Figure 7 shows how to define mixins for locked and short doors. The mixin Locked^{m} is nearly identical to the original LockedDoor^{c} class definition, except that the superclass is specified via the interface Door^{i}. The new LockedDoor^{c} and ShortDoor^{c} classes are created by applying Locked^{m} and Short^{m} to the class Door^{c}, respectively. Similarly, applying Locked^{m} to ShortDoor^{c} yields a class for locked, short doors.

Consider another door variation: MagicDoor^{c}, which is similar to a LockedDoor^{c}, except the player needs a book of spells instead of a key. We can extract the common parts of the implementation of MagicDoor^{c} and LockedDoor^{c} into a new mixin, Secure^{m}. Then, key- or book-specific information is composed with Secure^{m} to produce Locked^{m} and Magic^{m}, as shown in Figure 8. Each of the new mixins extends Door^{i} since the right hand mixin in the composition, Secure^{m}, extends Door^{i}.

The new Locked^{m} and Magic^{m} mixins can also be composed to form LockedMagic^{m}. This mixin has the expected behavior: to open an instance of LockedMagic^{m}, the player must have both the key and the book of spells. This combinational effect is achieved by a chain of super.canOpen() calls that use distinct, non-interfering versions of neededItem. The neededItem declarations of Locked^{m} and Magic^{m} do not interfere with each other because the interface extended by Locked^{m} is Door^{i}, which does not contain neededItem. In contrast, Door^{i} does contain canOpen, so the canOpen method in Locked^{m} overrides and chains to the canOpen in Magic^{m}.

4 Mixins for Java

MixedJava is an extension of ClassicJava with mixins. In ClassicJava, a class is assembled as a chain of class expressions. Specifically, the content of a class is defined by its immediate field and method declarations and by the

class LockedDoor^{c} extends Door^{c} {

boolean canOpen(Person^{c} p) {

if (!p.hasItem(theKey)) { System.out.println(”You don’t have the Key”); return false;

} System.out.println(”Using key...”); return super.canOpen(p);

} } class ShortDoor^{c} extends Door^{c} {

boolean canPass(Person^{c} p) {

if (p.height() > 1) { System.out.println(”You are too tall”); return false;

} System.out.println(”Ducking into door...”); return super.canPass(p);

} }

/* These classes cannot implement LockedShortDoor^{c} */ interface Door^{i} {

boolean canOpen(Person^{c} p); boolean canPass(Person^{c} p);

} mixin Locked^{m} extends Door^{i} {

boolean canOpen(Person^{c} p) {

if (!p.hasItem(theKey)) { System.out.println(”You don’t have the Key”); return false;

}

System.out.println(”Using key...”);

return super.canOpen(p); }

} mixin Short^{m} extends Door^{i} {

boolean canPass(Person^{c} p) {

if (p.height() > 1) { System.out.println(”You are too tall”); return false;

}

System.out.println(”Ducking into door...”); return super.canPass(p);

} } class LockedDoor^{c} = Locked^{m}(Door^{c}); class ShortDoor^{c} = Short^{m}(Door^{c}); class LockedShortDoor^{c} = Locked^{m}(Short^{m}(Door^{c}));

Figure 7: Some class definitions and their translation to composable mixins

interface SecureDoor^{i} extends Door^{i} {

Object neededItem(); } mixin Secure^{m} extends Door^{i} implements SecureDoor^{i} {

Object neededItem() { return null; } boolean canOpen(Person^{c} p) {

Object item = neededItem(); if (!p.hasItem(item)) {

System.out.println(”You don’t have the ” + item); return false;

} System.out.println(”Using ” + item + ”...”); return super.canOpen(p);

} } mixin LockedNeeded^{m} extends SecureDoor^{i} {

Object neededItem() {

return theKey; }

} mixin MagicNeeded^{m} extends SecureDoor^{i} {

Object neededItem() {

return theSpellBook; }

} mixin Locked^{m} = LockedNeeded^{m} compose Secure^{m}; mixin Magic^{m} = MagicNeeded^{m} compose Secure^{m}; mixin LockedMagic^{m} = Locked^{m} compose Magic^{m}; mixin LockedMagicDoor^{m} = LockedMagic^{m} compose Door^{m}; class LockedDoor^{c} = Locked^{m}(Door^{c}); …

Figure 8: Composing mixins for localized parameterization

declarations of its superclasses, up to Object.^{4} In Mixed-Java, a “class” is assembled by composing a chain of mixins. The content of the class is defined by the field and method declarations in the entire chain.

MixedJava provides two kinds of mixins:

• An atomic mixin declaration is similar to a class declaration. An atomic mixin declares a set of fields and methods that are extensions to some inherited set of fields and methods. In contrast to a class, an atomic mixin specifies its inheritance with an inheritance interface, not a static connection to an existing class. By abuse of terminology, we say that a mixin extends its inheritance interface. A mixin’s inheritance interface determines how method declarations within the mixin are combined with inherited methods. If a mixin declares a method x that is not contained in its inheritance interface, then that declaration never overrides another x. An atomic mixin implements one or more interfaces as specified in the mixin’s definition. In addition, a mixin always implements its inheritance interface.

• A composite mixin does not declare any new fields or methods. Instead, it composes two existing mixins to create a new mixin. The new composite mixin has all of the fields and methods of its two constituent mixins. Method declarations in the left-hand mixin override declarations in the right-hand mixin according to the left-hand mixin’s inheritance interface. Composition is allowed only when the right-hand mixin implements the left-hand mixin’s inheritance interface. A composite mixin extends the inheritance interface of its right-hand constituent, and it implements all of

4We use boldfaced class to refer to the content of a single class expression, as opposed to an actual class.

[figure: LockedNeeded^{m}; neededItem; SecureDoor^{i}; Secure^{m}; neededItem; canOpen; Door^{i}; MagicNeeded^{m}; neededItem; SecureDoor^{i}; Secure^{m}; neededItem; canOpen; Door^{i}; Door^{m}; canPass; canOpen; Locked^{m}; Magic^{m}; LockedMagic^{m}; LockedMagicDoor^{m}]

Figure 9: The LockedMagicDoor^{m} mixin corresponds to a sequence of atomic mixins

the interfaces that are implemented by its constituents. Composite mixins can be composed with other mixins, producing arbitrarily long chains of atomic mixin compositions.^{5}

Figure 9 illustrates how the mixin LockedMagicDoor^{m} from the previous section corresponds to a chain of atomic mixins. The arrows connecting the tops of the boxes represent mixin compositions; in each composition, the inheritance interface for the left-hand side is noted above the arrow. The other arrows show how method declarations in each mixin override declarations in other mixins according to the composition interfaces. For example, there is no arrow from the first Secure^{m}’s neededItem to Magic^{m}’s method because neededItem is not included in the Door^{i} interface. The canOpen method is in both Door^{i} and SecureDoor^{i}, so that corresponding arrows connect all declarations of canOpen.

Mixins completely subsume the role of classes. A mixin can be instantiated with new when the mixin does not inherit any services. In MixedJava, this is indicated by declaring that the mixin extends the special interface Empty. Consequently, we omit classes from our model of mixins, even though a realistic language would include both mixins and classes.

The following subsections present a precise description of MixedJava. Section 4.1 describes the syntax and type structure of MixedJava programs, followed by the type elaboration rules in Section 4.2. Section 4.3 explains the operational semantics of MixedJava, which is significantly different from that of ClassicJava. Section 4.4 presents a type soundness theorem, Section 4.5 briefly considers implementation issues, and Section 4.6 discusses related work.

4.1 MixedJava Programs

Figure 10 contains the syntax for MixedJava; the missing productions are inherited from the grammar of Classic-Java in Figure 3. The primary change to the syntax is the replacement of class declarations with mixin declarations. Another change is in the annotations added by type elaboration. First, view expressions are annotated with the source type of the expression. Second, a type is no longer included in the super annotation. Type elaboration also inserts extra view expressions into a program to implement subsumption.

The predicates and relations in Figure 11 (along with the interface-specific parts of Figure 4) summarize the syntactic

defn = mixin m extends i implements i* { field* meth* }

| mixin m = m compose m

| interface i extends i* { meth* }

e = new m | var | null | e \underline{: m} .fd | e \underline{: m} .fd = e

| e.md (e*) | super \underline{≡ this} .md (e*) | view \underline{t as} t e | let var = e in e

m = mixin name
t = m | i

Figure 10: Syntax extensions for MixedJava

content of a MixedJava program. A well-formed program induces a subtype relation ≤^{m}_{P} on its mixins such that a composite mixin is a subtype of each of its constituent mixins. Since each composite mixin has two supertypes, the type graph for mixins is a dag, rather than a tree as for classes. This dag can lead to ambiguities if subsumption is based on subtypes. For example, LockedMagic^{m} is a subtype of Secure^{m}, but it contains two copies of Secure^{m} (see Figure 9), so an instance of LockedMagic^{m} is ambiguous as an instance of Secure^{m}. More concretely, the fragment

LockedMagicDoor^{m} door = new LockedMagicDoor^{m}; (view Secure^{m} door).neededItem();

is ill-formed because LockedMagic^{m} is not viewable as Secure^{m}. The “viewable as” relation ⊴_{P} is a restriction on the subtype relation that eliminates ambiguities. Subsumption is thus based on ⊴_{P} rather than ≤_{P}. The relations ∈^{m}_{P}, which collect the fields and methods contained in each mixin, similarly eliminate ambiguities.

4.2 MixedJava Type Elaboration

Despite replacing the subtype relation with the “viewable as” relation for subsumption, ClassicJava’s type elaboration strategy applies equally well to MixedJava. The typing rules in Figure 12 are combined with the defn^{i}, meth, let, var, null, and abs rules from Figure 5.

Three of the new rules deserve special attention. First, the super^{m} rule allows a super call only when the method is declared in the current mixin’s inheritance interface, where the current mixin is determined by looking at the type of this. Second, the wcast^{m} rule strips out the view part of the expression and delegates all work to the subsumption rules. Third, the sub^{m} rule for subsumption inserts a view operator to make subsumption coercions explicit.

4.3 MixedJava Evaluation

The operational semantics for MixedJava differs substantially from that of ClassicJava. The rewriting semantics of

5Our composition operator is associative semantically, but not type-theoretically. The type system could be strengthened to make composition associative—giving MixedJava a categorical flavor—by letting each mixin declare a set of interfaces for inheritance, rather than a single interface. Each required interface must then either be satisfied or propagated by a composition. We have not encountered a practical use for the extended type system.

MixinsOnce(P)  Each mixin name is declared only once

∀m,m′ mixin m ⋯ mixin m′ ⋯ is in P ⟹ m ≠ m′

FieldOncePerMixin(P)  Field names in each mixin declaration are unique

∀fd,fd′ mixin ⋯ { ⋯ fd ⋯ fd′ ⋯ } is in P ⟹ fd ≠ fd′

MethodOncePerMixin(P) Method names in each mixin declaration are unique

∀md,md′ mixin ⋯ { ⋯ md ( ⋯) { ⋯ } ⋯ md′ ( ⋯) { ⋯ } ⋯ } is in P ⟹ md ≠ md′

NoAbstractMixins(P)  Methods in a mixin are not abstract

∀md,e mixin ⋯ { ⋯ md ( ⋯) { e } ⋯ } is in P ⟹ e ≠ abstract

≺^{m}_{P}  Mixin declares an inheritance interface

m ≺^{m}_{P} i ⇔ mixin m extends i ⋯ { ⋯ } is in P

≺ ≺^{m}_{P}  Mixin declares implementation of an interface

m ≺ ≺^{m}_{P} i ⇔ mixin m ⋯ implements ⋯ i ⋯ { ⋯ } is in P

• ≐^{m}_{P} • ∘ •  Mixin is declared as a composition

m ≐^{m}_{P} m′ ∘ m′′ ⇔ mixin m = m′ compose m′′ is in P

∈ ∈^{m}_{P}  Method is declared in a mixin

⟨md, (t_{1} … t_{n} ⟶ t), (var_{1} … var_{n}), e⟩ ∈ ∈^{m}_{P} m ⇔ mixin m ⋯ { ⋯ t md (t_{1} var_{1} … t_{n} var_{n}) { e } ⋯ } is in P

∈ ∈^{m}_{P}  Field is declared in a mixin

⟨m.fd, t⟩ ∈ ∈^{m}_{P} m ⇔ mixin m ⋯ { ⋯ t fd ⋯ } is in P

≤^{m}_{P}  Mixin is a submixin

m ≤^{m}_{P} m′ ⇔ m = m′ or (∃m′′, m′′′ s.t. m ≐^{m}_{P} m′′ ∘ m′′′ and (m′′ ≤^{m}_{P} m′ or m′′′ ≤^{m}_{P} m′))

⊴ ^{m}_{P}  Mixin is viewable as a mixin (i.e., mixin is uniquely a submixin)

m ⊴ ^{m}_{P} m′ ⇔ m = m′ or (∃m′′, m′′′ s.t. m ≐^{m}_{P} m′′ ∘ m′′′ and (m′′ ⊴ ^{m}_{P} m′ xor m′′′ ⊴ ^{m}_{P} m′))

CompleteMixins(P)  Mixins that are composed are defined

rng(≐^{m}_{P}) ⊆ {m ∘ m′ | m,m′ ∈ dom(≺^{m}_{P}) ∪ dom(≐^{m}_{P})}

WellFoundedMixins(P)  Mixin hierarchy is an order

≤^{m}_{P} is antisymmetric

CompleteInterfaces(P)  Extended/implemented interfaces are defined

rng(≺^{i}_{P}) ∪ rng(≺^{m}_{P}) ∪ rng(≺ ≺^{m}_{P}) ⊆ dom(≺^{i}_{P})∪{Empty}

≺|^{m}_{P}  Mixin extends an interface

m ≺|^{m}_{P} i ⇔ m ≺^{m}_{P} i or (∃m′,m′′ s.t. m ≐^{m}_{P} m′ ∘ m′′ and m′′ ≺|^{m}_{P} i)

≪^{m}_{P}  Mixin implements an interface

m ≪^{m}_{P} i ⇔ ∃m′,i′ s.t. m ≤^{m}_{P} m′ and i′ ≤^{i}_{P} i and (m′ ≺^{m}_{P} i′ or m′ ≺ ≺^{m}_{P} i′)

<⊲ ^{m}_{P}  Mixin is viewable as an interface (i.e., mixin uniquely implements an interface)

m <⊲ ^{m}_{P} i ⇔ (∃i′ s.t. i ≤^{i}_{P} i′ and (m ≺^{m}_{P} i′ or m ≺ ≺^{m}_{P} i′)) or (∃m′, m′′ s.t. m ≐^{m}_{P} m′ ∘ m′′ and (m′ <⊲ ^{m}_{P} i xor m′′ <⊲ ^{m}_{P} i))

MixinCompositionsOK(P) Mixins are composed safely

∀m,m′,m′′ m ≐^{m}_{P} m′ ∘ m′′ ⟹ ∃i s.t. m′ ≺|^{m}_{P} i and m′′ <⊲ ^{m}_{P} i

:: and @ Sequence constructors :: adds an element to the beginning of a sequence; @ appends two sequences
⟶_{P}  Mixin corresponds to a chain of atomic mixins

m ⟶_{P} M ⇔ (∃i s.t. m ≺^{m}_{P} i and M = [m]) or (∃m′, m′′, M′, M′′ s.t. m ≐^{m}_{P} m′ ∘ m′′ and m′ ⟶_{P} M′ and m′′ ⟶_{P} M′′ and M = M′@M′′)

≤^{M}  Views have an inverted subsequence order  M ≤^{M} M′ ⇔ ∃M′′ s.t. M = M′′@M′
MixinMethodsOK(P)  Method definitions match inheritance interface

∀m,i,e,md, T, T′, V, V′ (⟨md, T, V, e⟩ ∈ ∈^{m}_{P} m and ⟨md, T′, V′, abstract⟩ ∈ ∈^{m}_{P} i) ⟹ (T = T′ or m ⊀|^{m}_{P} i)

∈^{m}_{P}  Field is contained in a mixin

⟨m′.fd, t⟩ ∈^{m}_{P} m ⇔ ∃M, M′ s.t. m ⟶_{P} M and ⟨m′.fd, t⟩ ∈ ∈^{m}_{P} m′ and {m′::M′} = {m′::M′ | M ≤^{M} m′::M′ and ∃t′ s.t. ⟨m′.fd, t′⟩ ∈ ∈^{m}_{P} m′}

∈^{m}_{P}  Method is contained in a mixin

⟨md, T, V, e⟩ ∈^{m}_{P} m ⇔ ∃M, m′, M′ s.t. m ⟶_{P} M and ⟨md, T, V, e⟩ ∈ ∈^{m}_{P} m′ and {m′::M′} = {m′::M′ | M ≤^{M} m′::M′ and ∃V′,e′ s.t. ⟨md, T, V′, e′⟩ ∈ ∈^{m}_{P} m′}

MixinsImplementAll(P)  Mixins supply methods to implement interfaces

∀m,i m ≺ ≺^{m}_{P} i ⟹ (∀md, T ⟨md, T, V, abstract⟩ ∈^{i}_{P} i ⟹ (∃ e s.t. ⟨md, T, V, e⟩ ∈ ∈^{m}_{P} m or ∃ i′ s.t. (m ≺|^{m}_{P} i′ and ⟨md, T, V, abstract⟩ ∈^{i}_{P} i′)))

≤_{P}  Type is a subtype  ≤_{P} ≡ ≤^{m}_{P} ∪ ≤^{i}_{P} ∪ ≪^{m}_{P}
⊴ _{P}  Type is viewable as another type  ⊴ _{P} ≡ ⊴ ^{m}_{P} ∪ ≤^{i}_{P} ∪ <⊲ ^{m}_{P}
∈_{P}  Field or method is in a type  ∈_{P} ≡ ∈^{m}_{P} ∪ ∈^{i}_{P}
•/• ▷ •  Mixin selects a view in a chain

M/m ▷ M′ ⇔ {M′} = {M′′@M′′′ | m ⟶_{P} M′′ and M ≤^{M} M′′@M′′′}

•/• ▷ •  Interface selects a view in a chain

M/i ▷ M′ ⇔ M′ = min{m::M′′ | m ≺|^{m}_{P} i and M ≤^{M} m::M′′}

•/• ∝ •  Method in a sequence is the same as in a subsequence

m::M/md ∝ M′ ⇔ m::M = M′ or (∃i, T, V, M′′ s.t. m ≺|^{m}_{P} i and ⟨md, T, V, abstract⟩ ∈ ∈^{i}_{P} i and M′/i ▷ M′′ and M′′/md ∝ M′)

•∈^{rt}_{P} • in •  Method and view is selected by a view in a chain

⟨md, T, V, e, m::M⟩ ∈^{rt}_{P} M_{v} in M_{o} ⇔ ⟨md, T, V, e⟩ ∈ ∈^{m}_{P} m and M_{b} = max{M′ | M_{v}/md ∝ M′} and {m::M} = {m::M | m::M≤^{M}M_{o} and m::M/md ∝ M_{b} and ∃V′,e′ s.t. ⟨md, T, V′, e′⟩ ∈ ∈^{m}_{P} m}

Figure 11: Predicates and relations in the model of MixedJava

the latter relies on the uniqueness of each method name in the chain of classes associated with an object. This uniqueness is not guaranteed for chains of mixins. Specifically, a composition m_{1} compose m_{2} contains two methods named x if both m_{1} and m_{2} declare x and m_{1}’s inheritance interface does not contain x. Both x methods are accessible in an instance of the composite mixin since the object can be viewed specifically as an instance of m_{1} or m_{2}.

One strategy to avoid the duplication of x is to rename it in m_{1} and m_{2}. At best, this is a global transformation on the program, since x is visible to the entire program as a public method. At worst, renaming triggers an exponential

⊢_{p}

MixinsOnce(P)  MethodOncePerMixin(P)  InterfacesOnce(P)  CompleteMixins(P)
WellFoundedMixins(P)  CompleteInterfaces(P)  WellFoundedInterfaces(P)
MixinFieldsOK(P) MixinMethodsOK(P) InterfaceMethodsOK(P) InterfacesAbstract(P)
NoAbstractMixins(P)  MixinsImplementAll(P)  P ⊢_{d} defn_{j} ⇒ defn′_{j} for j ∈ [1, n]
P, [ ] ⊢_{e} e ⇒ e′ : t  where P = defn_{1} … defn_{n} e
⊢_{p} defn_{1} … defn_{n} e ⇒ defn′_{1} … defn′_{n} e′ : t

[prog^{m}]

⊢_{d}

\frac{P ⊢_{t} t_{j} for each j ∈ [1, n]  P, m ⊢_{m} meth_{k} ⇒ meth′_{k} for each k ∈ [1, p]}{P ⊢_{d} mixin m ⋯ \{ t_{1} fd_{1} … t_{n} fd_{n} meth_{1} … meth_{p} \} ⇒ mixin m ⋯ \{ t_{1} fd_{1} … t_{n} fd_{n} meth′_{1} … meth′_{p} \}} [defn^{m}]

⊢_{e}

\frac{P ⊢_{t} m  m ≺|^{m}_{P} Empty}{P, Γ ⊢_{e} new m ⇒ new m : m} [new^{m}]  \frac{P, Γ ⊢_{e} e ⇒ e′ : m  ⟨m′.fd, t⟩ ∈_{P} m}{P, Γ ⊢_{e} e.fd ⇒ e′ \underline{: m′} .fd : t} [get^{m}]

\frac{P, Γ ⊢_{e} e ⇒ e′ : m  ⟨m′.fd, t⟩ ∈_{P} m  P, Γ ⊢_{s} e_{v} ⇒ e′_{v} : t}{P, Γ ⊢_{e} e.fd = e_{v} ⇒ e′ \underline{: m′} .fd = e′_{v} : t} [set^{m}]

\frac{P, Γ ⊢_{e} e ⇒ e′ : t′  ⟨md, (t_{1} … t_{n} ⟶ t), (var_{1} … var_{n}), e_{b}⟩ ∈_{P} t′ P, Γ ⊢_{s} e_{j} ⇒ e′_{j} : t_{j} for j ∈ [1, n]}{P, Γ ⊢_{e} e.md (e_{1} … e_{n}) ⇒ e′.md (e′_{1} … e′_{n}) : t} [call^{m}]

P, Γ ⊢_{e} this ⇒ this : m  m ≺|^{m}_{P} i  ⟨md, (t_{1} … t_{n} ⟶ t), (var_{1} … var_{n}), abstract⟩ ∈_{P} i
P, Γ ⊢_{s} e_{j} ⇒ e′_{j} : t_{j} for j ∈ [1, n]
P, Γ ⊢_{e} super.md(e_{1} … e_{n}) ⇒ super \underline{≡ this} .md(e′_{1} … e′_{n}) : t

[super^{m}]

\frac{P, Γ ⊢_{s} e ⇒ e′ : t}{P, Γ ⊢_{e} view t e ⇒ e′ : t} [wcast^{m}]  \frac{P, Γ ⊢_{e} e ⇒ e′ : t′  t′ ≰_{P} t}{P, Γ ⊢_{e} view t e ⇒ view \underline{t′ as} t e′ : t} [ncast^{m}]

⊢_{s}, ⊢_{t}

\frac{P, Γ ⊢_{e} e ⇒ e′ : t′  t′ ⊴_{P} t}{P, Γ ⊢_{s} e ⇒ view \underline{t′ as} t e′ : t} [sub^{m}]  \frac{t ∈ dom(≺^{m}_{P}) ∪ dom(≐^{m}_{P}) ∪ dom(≺^{i}_{P})∪\{Empty\}}{P ⊢_{t} t} [type^{m}]

Figure 12: Context-sensitive checks and type elaboration rules for MixedJava

explosion in the size of the program, which occurs when m_{1} and m_{2} are actually the same mixin m. Since the mixin m represents a type, renaming x in each use of m splits it into two different types, which requires type-splitting at every expression in the program involving m.

Our MixedJava semantics handles the duplication of method names with run-time context information: the current view of an object.^{6} During evaluation, each reference to an object is bundled with its view of the object, so that values are of the form ⟨object∥view⟩. A reference’s view can be changed by subsumption, method calls, or explicit casts.

A view is represented as a chain of mixins. This chain is always a tail of the object’s full chain of mixins, i.e., the chain of mixins for the object’s instantiation type. The tail designates a specific point in the full mixin chain for selecting methods during dynamic dispatch. For example, when an instance of LockedMagicDoor^{m} is used as a Magic^{m} instance, the view of the object is [MagicNeeded^{m} Secure^{m} Door^{m}]. With this view, a search for the neededItem method of the object begins in the MagicNeeded^{m} element of the chain.

The first phase of a search for some method x locates the base declaration of x, which is the unique non-overriding declaration of x that is visible in the current view. This declaration is found by traversing the view from left to right, using the inheritance interface at each step as a guide for the next step (via the ∝ and ▷ relations). When the search reaches a mixin whose inheritance interface does not include x, the base declaration of x has been found. But the base declaration is not the destination of the dispatch; the destination is an overriding declaration of x for this base that is contained in the object’s instantiated mixin. Among the declarations that override this base, the leftmost declaration is selected as the destination. The location of that overriding declaration determines both the method definition that is invoked and the view of the object (i.e., the representation of this) within the destination method body. This dispatching algorithm is encoded in the ∈^{rt}_{P} relation.

Let us apply the algorithm to o.getNeeded() in the following example:

mixin Getter^{m} extends Empty {

Object get(Secure^{m} o) { o.neededItem() } } let door = new LockedMagicDoor^{m} in let g = new Getter^{m}

in g.get(\underline{view Secure^{m}} view Locked^{m} door); g.get(\underline{view Secure^{m}} view Magic^{m} door)

For the first call to g.get, o is replaced by a reference with the view [Secure^{m} MagicNeeded^{m} Secure^{m} Door^{m}]. In this view, the base declaration of neededItem is in the leftmost Secure^{m} since neededItem is not in the interface extended by Secure^{m}. The overriding declaration is in LockedNeeded^{m}, which appears to the left of Secure^{m} in the instantiated chain and extends an interface that contains neededItem.

6A view is analogous to a “subobject” in languages with multiple inheritance, but without the complexity of shared superclasses [26].

e = … | ⟨object∥M⟩
v = ⟨object∥M⟩ | null

E = [ ] | E \underline{: m} .fd | E \underline{: m} .fd = e | v \underline{: m} .fd = E
| E.md(e …) | v.md(v … E e …)
| super \underline{≡ v} .md(v … E e …)
| view \underline{t as} t E | let var = E in e
P ⊢ ⟨E[new m], S⟩ ↪ ⟨E[⟨object∥M⟩], S[object↦⟨m, [M_{1}.fd_{1}↦null, … M_{n}.fd_{n}↦null]⟩]⟩  [new]

where object ∉ dom(S) and m ⟶_{P} M and {M_{1}.fd_{1}, … M_{n}.fd_{n}} = {m′::M′.fd | M ≤^{M} m′::M′ and ∃t s.t. ⟨m′.fd, t⟩ ∈ ∈^{m}_{P} m′}

P ⊢ ⟨E[⟨object∥M⟩ \underline{: m′} .fd], S⟩ ↪ ⟨E[v], S⟩  [get]
where S(object) = ⟨m, F⟩ and M/m′ ▷ M′ and F(M′.fd) = v
P ⊢ ⟨E[⟨object∥M⟩ \underline{: m′} .fd = v], S⟩ ↪ ⟨E[v], S′[object↦⟨m, F[M′.fd↦v]⟩]⟩  [set]
where S(object) = ⟨m, F⟩ and M/m′ ▷ M′
P ⊢ ⟨E[⟨object∥M⟩.md(v_{1}, … v_{n})], S⟩ ↪ ⟨E[e[⟨object∥M′⟩/this, v_{1}/var_{1}, … v_{n}/var_{n}]], S⟩  [call]

where S(object) = ⟨m, F⟩ and m ⟶_{P} M_{o} and ⟨md, T, (var_{1} … var_{n}), e, M′⟩ ∈^{rt}_{P} M in M_{o}

P ⊢ ⟨E[super \underline{≡ ⟨object∥m::M⟩} .md(v_{1}, … v_{n})], S⟩ ↪ ⟨E[e[⟨object∥M′⟩/this, v_{1}/var_{1}, … v_{n}/var_{n}]], S⟩ [super]

where m ≺|^{m}_{P} i and M/i ▷ M′′ and ⟨md, T, (var_{1} … var_{n}), e, M′⟩ ∈^{rt}_{P} M′′ in M′′

P ⊢ ⟨E[view \underline{t′ as} t ⟨object∥M⟩], S⟩ ↪ ⟨E[⟨object∥M′⟩], S⟩  [view]
where t′ ⊴_{P} t and M/t ▷ M′
P ⊢ ⟨E[view \underline{t′ as} t ⟨object∥M⟩], S⟩ ↪ ⟨E[⟨object∥M′′⟩], S⟩  [cast]

where t′ ⋬_{P} t and S(object) = ⟨m, F⟩ and m ⊴_{P} t and m ⟶_{P} M′ and M′/t ▷ M′′

P ⊢ ⟨E[let var = v in e], S⟩ ↪ ⟨E[e[v/var]], S⟩  [let]
P ⊢ ⟨E[view \underline{t′ as} t ⟨object∥M⟩], S⟩ ↪ ⟨error: bad cast, S⟩  [xcast]
where t′ ⋬_{P} t and S(object) = ⟨m, F⟩ and m ⋬_{P} t
P ⊢ ⟨E[null \underline{: m} .fd], S⟩ ↪ ⟨error: dereferenced null, S⟩  [nget]
P ⊢ ⟨E[null \underline{: m} .fd = v], S⟩ ↪ ⟨error: dereferenced null, S⟩  [nset]
P ⊢ ⟨E[null.md(v_{1}, … v_{n})], S⟩ ↪ ⟨error: dereferenced null, S⟩  [ncall]

Figure 13: Operational semantics for MixedJava

In contrast, the second call to g.get receives a reference with the view [Secure^{m} Door^{m}]. In this view, the base definition of neededItem is in the rightmost Secure^{m} of the full chain, and it is overridden in MagicNeeded^{m}. Neither the definition of neededItem in LockedNeeded^{m} nor the one in the leftmost occurrence of Secure^{m} is a candidate relative to the given view, because Secure^{m} extends an interface that hides neededItem.

MixedJava not only differs from ClassicJava with respect to method dispatching, but also in its treatment of super. In MixedJava, super dispatches are dynamic, since the “supermixin” for a super expression is not statically known. The super dispatch for mixins is implemented like regular dispatches with the ∈^{rt}_{P} relation, but using a tail of the current view in place of both the instantiation and view chains; this ensures that a method is selected from the leftmost mixin that follows the current view.

Figure 13 contains the complete operational semantics for MixedJava as a rewriting system on expression-store pairs, like the class semantics described in Section 2.3. In this semantics, an object in the store is tagged with a mixin instead of a class, and the values are null and ⟨object∥view⟩ pairs.

4.4 MixedJava Soundness

The type soundness theorem for MixedJava is mutatis mutandis the same as the soundness theorem for ClassicJava as described in Section 2.4. To prove the soundness theorem, we introduce a conservative extension, MixedJava′, which is defined by revising some of the MixedJava relations (see Figure 14).

In the extended language, the subtype relation is used directly for the “viewable as” relation without eliminating ambiguities. Thus, MixedJava′ allows coercions and method

≤_{P}  Type is a subtype
Extended for views: M ≤_{P} m ⇔ M contains m’s sequence; M ≤_{P} i ⇔ M contains an m s.t. m ≺^{m}_{P} i
⊴ _{P}  Type is viewable as another type  ⊴ _{P} ≡ ≤_{P}
∈_{P}  Field or method is contained in a type

Choose the leftmost field/method instance

•/• ▷ •  Mixin selects a view in a chain

Choose the leftmost instance in the chain

•∈^{rt}_{P} • in • Method and view is selected by a view in a chain

Choose the minimum view with a method

Figure 14: Revised relations for MixedJava′

calls that are rejected as ambiguous in MixedJava. This makes MixedJava′ less suitable as a programming language, but the proof of its type soundness theorem is significantly simpler. The soundness theorem for MixedJava′ then applies to MixedJava by the following two lemmas:

1. Every MixedJava program is a MixedJava′ program.

2.

P ⊢ ⟨e, S⟩ ↪ ⟨e′, S′⟩ in MixedJava ⇒ P ⊢ ⟨e, S⟩ ↪ ⟨e′, S′⟩ in MixedJava′.

A complete definition of MixedJava′, its soundness proof, and proofs for the above lemmas are available in the extended paper [16].

4.5 Implementation Considerations

The MixedJava semantics is formulated at a high level, leaving open the question of how to implement mixins efficiently. Common techniques for implementing classes can be applied to mixins, but two properties of mixins require new implementation strategies. First, each object reference must carry a view of the object. This can be implemented using double-wide references, one half for the object pointer and the other half for the current view. Second, method invocation depends on the current view as well as the instantiation mixin of an object, as reflected in the ∈^{rt}_{P} relation. Nevertheless, this relation determines a static, per-mixin method table that is analogous to the virtual method tables typically generated for classes.

The overall cost of using mixins instead of classes is equivalent to the cost of using interface-typed references instead of class-typed references. The justification for this cost is that mixins are used to implement parts of a program that cannot be easily expressed using classes. In a language that provides both classes and mixins, portions of the program that do not use mixins do not incur any extra overhead.

4.6 Related Work on Mixins

Mixins first appeared as a CLOS programming pattern [21, 22]. Unfortunately, the original linearization algorithm for CLOS’s multiple inheritance breaks the encapsulation of class definitions [10], which makes it difficult to use CLOS for proper mixin programming. The CommonObjects [27] dialect of CLOS supports multiple inheritance without breaking encapsulation, but the language does not provide simple composition operators for mixins.

Bracha has investigated the use of “mixin modules” as a general language for expressing inheritance and overriding in objects [5, 6, 7]. His system is based on earlier work by Cook [8]; its underlying semantics was recently reformulated in categorical terms by Ancona and Zucca [4]. Bracha’s system gives the programmer a mechanism for defining modules (classes, in our sense) as a collection of attributes (methods). Modules can be combined into new modules through various merging operators. Roughly speaking, these operators provide an assembly language for expressing class-to-class functions and, as such, permit programmers to construct mixins. However, this language forces the programmer to resolve attribute name conflicts manually and to specify attribute overriding explicitly at a mixin merge site. As a result, the programmer is faced with the same problem as in Common Lisp, i.e., the low-level management of details. In contrast, our system provides a language to specify both the content of a mixin and its interaction with other mixins for mixin compositions. The latter gives each mixin an explicit role in the construction of programs so that only sensible mixin compositions are allowed. It distinguishes method overriding from accidental name collisions and thus permits the system to resolve name collisions automatically in a natural manner.

5 Conclusion

We have presented a programming language of mixins that relies on the same intuition as single inheritance classes. Indeed, a mixin declaration in our language hardly differs from a class declaration since, from the programmer’s local perspective, there is little difference between knowing the properties of a superclass as described by an interface and knowing the exact implementation of a superclass. However, from the programmer’s global perspective, mixins free each collection of field and method extensions from the tyranny of a single superclass, enabling new abstractions and increasing the re-use potential of code.

While using mixins is inherently more expensive than using classes—because mixins enforce the distinction between implementation inheritance and subtyping—the cost is reasonable and offset by gains in code re-use. Future work on mixins must focus on exploring compilation strategies that lower the cost of mixins, and on studying how designers can exploit mixins to construct better design patterns.

Acknowledgements: Thanks to Corky Cartwright, Robby Findler, Cormac Flanagan, and Dan Friedman for their comments on early drafts of this paper.

References

[1] Abadi, M., and Cardelli, L. A theory of primitive objects — untyped and first-order systems. In Theoretical Aspects of Computer Software, M. Hagiya and J. C. Mitchell, Eds., vol. 789 of LNCS. Springer-Verlag, Apr. 1994, pp. 296–320.

[2] Abadi, M., and Cardelli, L. A theory of primitive objects: second-order systems. In Proc. European Symposium on Programming (New York, N.Y., 1994), D. Sannella, Ed., Lecture Notes in Computer Science 788, Springer Verlag, pp. 1–25.

[3] Abadi, M., and Cardelli, L. An imperative object calculus. In TAPSOFT’95: Theory and Practice of Software Development (May 1995), P. D. Mosses, M. Nielsen, and M. I. Schwartzbach, Eds., Lecture Notes in Computer Science 915, Springer-Verlag, pp. 471–485.

[4] Ancona, D., and Zucca, E. An algebraic approach to mixins and modularity. In Proc. Conference on Algebraic and Logic Programming (Berlin, 1996), M. Hanus and M. Rodríguez-Artalejo, Eds., Lecture Notes in Computer Science 1139, Springer Verlag, pp. 179–193.

[5] Bracha, G. The Programming Language Jigsaw: Mixins, Modularity and Multiple Inheritance. Ph.D. thesis, Dept. of Computer Science, University of Utah, Mar. 1992.

[6] Bracha, G., and Cook, W. Mixin-based inheritance. In Proc. Joint ACM Conf. on Object-Oriented Programming, Systems, Languages and Applications and the European Conference on Object-Oriented Programming (Oct. 1990).

[7] Bracha, G., and Lindstrom, G. Modularity meets inheritance. In Proc. IEEE Computer Society International Conference on Computer Languages (Washington, DC, Apr. 1992), IEEE Computer Society, pp. 282– 290.

[8] Cook, W. R. A Denotational Semantics of Inheritance. Ph.D. thesis, Department of Computer Science, Brown University, Providence, RI, May 1989.

[9] Drossopolou, S., and Eisenbach, S. Java is typesafe – probably. In Proc. European Conference on Object Oriented Programming (June 1997).

[10] Ducournau, R., Habib, M., Huchard, M., and Mugnier, M. L. Monotonic conflict resolution mechanisms for inheritance. In Proc. Conference on Object-Oriented Programming Systems, Languages, and Applications (Oct. 1992), pp. 16–24.

[11] Eifrig, J., Smith, S., Trifonov, V., and Zwarico, A. Application of OOP type theory: State, decidability, integration. In Proc. Conference on Object-Oriented Programming Systems, Languages, and Applications (Oct. 1994), pp. 16–30.

[12] Felleisen, M. Programming languages and lambda calculi.

URL: www.cs.rice.edu/~matthias/411web/mono.ps.

[13] Felleisen, M., and Hieb, R. The revised report on the syntactic theories of sequential control and state. Tech. Rep. 100, Rice University, June 1989. Theoretical Computer Science, volume 102, 1992.

[14] Findler, R. B., Flanagan, C., Flatt, M., Krishnamurthi, S., and Felleisen, M. DrScheme: A pedagogic programming environment for Scheme. In Proc. International Symposium on Programming Languages, Implementations, Logics, and Programs (1997).

[15] Flatt, M. PLT MzScheme: Language manual. Tech. Rep. TR97-280, Rice University, 1997.

[16] Flatt, M., Krishnamurthi, S., and Felleisen, M. Classes and mixins. Tech. Rep. TR97-293, Rice University, 1997.

[17] Gamma, E., Helm, R., Johnson, R., and Vlissides, J. Design Patterns: Elements of Reusable Object-Oriented Software. Addison Wesley, Massachusetts, 1994.

[18] Gosling, J., Joy, B., and Steele, G. The Java Language Specification. The Java Series. Addison-Wes-ley, Reading, MA, USA, June 1996.

[19] Harper, R., and Stone, C. A type-theoretic semantics for Standard ML 1996. Submitted for publication, 1997.

[20] Kamin, S. Inheritance in smalltalk-80: a denotational definition. In Proc. Conference on Principles of Programming Languages (Jan. 1988).

[21] Kessler, R. R. LISP, Objects, and Symbolic Programming. Scott, Foresman and Company, Glenview, IL, USA, 1988.

[22] Koschmann, T. The Common LISP Companion. John Wiley and Sons, New York, N.Y., 1990.

[23] Mason, I. A., and Talcott, C. L. Reasoning about object systems in VTLoE. International Journal of Foundations of Computer Science 6, 3 (Sept. 1995), 265–298.

[24] Reddy, U. S. Objects as closures: Abstract semantics of object oriented languages. In Proc. Conference on Lisp and Functional Programming (July 1988), pp. 289–297.

[25] Rémy, D. Programming objects with ML-ART: An extension to ML with abstract and record types. In Theoretical Aspects of Computer Software (New York, N.Y., Apr. 1994), M. Hagiya and J. C. Mitchell, Eds., Lecture Notes in Computer Science 789, Springer-Verlag, pp. 321–346.

[26] Rossie, J. G., Friedman, D. P., and Wand, M. Modeling subobject-based inheritance. In Proc. European Conference on Object-Oriented Programming (Berlin, Heidelberg, and New York, July 1996), P. Cointe, Ed., Lecture Notes in Computer Science 1098, Springer-Verlag, pp. 248–274.

[27] Snyder, A. Inheritance and the development of encapsulated software components. In Research Directions in Object-Oriented Programming. MIT Press, 1987, pp. 165–188.

[28] Syme, D. Proving Java type soundness. Tech. Rep. 427, University of Cambridge, July 1997.

[29] Wright, A., and Felleisen, M. A syntactic approach to type soundness. Tech. Rep. 160, Rice University, 1991. Information and Computation, volume 115, 1994.