A Programmer’s Reduction Semantics for Classes and Mixins

TR 97-293: Corrected Version, June 8, 1999

Original in Formal Syntax and Semantics of Java, LNCS volume 1523 (1999)

Matthew Flatt, Shriram Krishnamurthi, Matthias Felleisen

Rice University

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 higherorder 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 consume a large number of arguments, the approach quickly

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

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 [7] 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 [16], 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 programmers of our team used it extensively for the construction of DrScheme [15], a Scheme programming environment. A thorough analysis, however, 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, single-inheritance Java program-

1 Function entry points à la Fortran or keyword arguments à la Common Lisp are a

symptom of this problem, not a remedy. 2 Dan Friedman determined in an informal poll in 1996 that almost nobody who

teaches C++ teaches multiple inheritance [pers. com.].

ming. 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.

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 / …

… …

Door^{c}

Enter …

LockedDoor^{c} …

… …

ShortDoor^{c} …

[figure]

… …

Classes

[figure]

Fig. 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; ⟩]

Fig. 2. Given a type graph, reductions map a store-expression pair to a new pair

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 [14, 19, 30]. Figures 1 and 2 illustrate the essence of 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 tagged record of field values, where the tag indicates the class 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 [13, 19].

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

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

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 ClassicJava; instance variables are always initialized to null. Finally, the view and let forms represent Java’s casting expressions and local variable bindings, respectively.

The evaluation rules for ClassicJava are defined in terms of individual expressions, but certain rules require information about the context of the expression in the original program. For example, the evaluation rule for a field use depends on the syntactic type of the object position, which is determined by the expression’s type environment in the original program. To remove such context dependencies before evaluation, the type-checker annotates field uses and super invocations with extra source-context information (see the underlined parts of the syntax).

A valid ClassicJava program satisfies a number of simple predicates and relations; these are described in Figures 4 and 5. For example, the ClassesOnce(P) predicate 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 set methods of an interface, as described by ∈^{i}_{P}, is 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.

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 (t … ⟶ t), V for variable lists (var…), and Γ 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 (not spanning a class or interface definition).

ClassesOnce(P)  Each class name is declared only once

class c ⋯ class c′ ⋯ is in P ⟹ c ≠ c′

FieldOncePerClass(P) Field names in each class declaration are unique

class ⋯ { ⋯ fd ⋯ fd′ ⋯ } is in P ⟹ fd ≠ fd′

MethodOncePerClass(P) Method names in each class declaration are unique

class ⋯ { ⋯ md ( ⋯) { ⋯ } ⋯ md′ ( ⋯) { ⋯ } ⋯ } is in P ⟹ md ≠ md′

InterfacesOnce(P)  Each interface name is declared only once

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

InterfacesAbstract(P) Method declarations in an interface are abstract
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

(⟨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′′})

Fig. 4. Predicates and relations in the model of ClassicJava (Part I)

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 in Γ
P, Γ ⊢_{s} e ⇒ e′ : t  e has type t using subsumption in Γ
P ⊢_{t} t  t exists

≤^{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) Interface inheritance or redeclaration of methods is consistent
⟨md, T, V, abstract⟩ ∈ ∈^{i}_{P} i and ⟨md, T′, V′, abstract⟩ ∈ ∈^{i}_{P} i′
⟹ (T = T′ or ∀i′′(i′′ ≰^{i}_{P} i 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

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⟩ ∈^{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}

Fig. 5. Predicates and relations in the model of ClassicJava (Part II)

⊢_{p}

\frac{ClassesOnce(P) InterfacesOnce(P) MethodOncePerClass(P) FieldOncePerClass(P) CompleteClasses(P) WellFoundedClasses(P)  CompleteInterfaces(P) WellFoundedInterfaces(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{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}]

Fig. 6. Context-sensitive checks and type elaboration rules for ClassicJava (Part I)

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 ⊢_{t} t}{P, Γ ⊢_{e} abstract ⇒ abstract : t} [abs]

\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]

⊢_{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}]

Fig. 7. Context-sensitive checks and type elaboration rules for ClassicJava (Part II)

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 annotated expression 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 annotated expression 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 Figures 6 and 7. A program is welltyped 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 F is a mapping from elaborated field

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, F⟩]⟩  [new]

where object ∉ dom(S) and F = {c′.fd↦null | c ≤^{c}_{P} c′ and ∃t s.t. ⟨c′.fd, t⟩ ∈ ∈^{c}_{P} c′}

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[view t′ null], S⟩ ↪ ⟨error: bad cast, S⟩  [ncast]
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]

Fig. 8. Operational semantics for ClassicJava

names to values. The evaluation rules are a straightforward modification of those for imperative Scheme [14].

The complete evaluation rules are in Figure 8. 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 ClassicJava produce either a value that has a subtype of t, or one of two errors. Put differently, an evaluation cannot go wrong, which our model model means getting stuck. This property can be formulated as a type soundness theorem.

Theorem 1 (Type Soundness). 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; or

– P′ ⊢ ⟨e, ∅⟩ ↪^{∗} ⟨null, S⟩; or – 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) [30]. 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.

Definition 2 (Environment-Store Consistency).

P,Γ ⊢_{σ} S
⇔ (S(object) = ⟨c,F⟩

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

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

Σ_{5}: and object ∈ dom(Γ) ⇒ object ∈ dom(S)^{3} Σ_{6}: and dom(S) ⊆ dom(Γ)

Since the rewriting rules reduce annotated terms, we derive new type judgements ⊢\underline{s} and ⊢\underline{e} that relate annotated terms to show that reductions preserve type correctness. Each of the new rules performs the same checks as the rule it is derived from without removing or adding annotation. Thus, ⊢\underline{s} is derived from ⊢_{s}, and so forth.

The judgement on view expressions is altered slightly; we retain the view operation in all cases, and we collapse the [wcast^{c}] and [ncast^{c}] relations to a new [cast^{c}] relation that permits any casting operation:

\frac{P,Γ ⊢\underline{e} e : t′}{P,Γ ⊢\underline{e} view t e : t} [cast^{c}]

The new [cast^{c}] relation lets us prove that every intermediate expresion in a reduction is well-typed, whereas [wcast^{c}] and [ncast^{c}] more closely approximate Java, which rejects certain expressions because they would certainly produce error: bad cast. For example, assuming that LockedDoor^{c} and ShortDoor^{c} extend Door^{c} separately, a legal source program

let x = o.GetDoor() in (view LockedDoor^{c} x)

might reduce to view LockedDoor^{c} shortDoorObject

where shortDoorObject is an instance of ShortDoor^{c}. Unlike the [wcast^{c}] and [ncast^{c}] rules in ⊢_{e}, the [cast^{c}] rule in ⊢\underline{e} assigns a type to the reduced expression.

3 In Σ_{5}, it would be wrong to write dom(Γ) ⊆ dom(S) because Γ may contain bindings for lexical variables.

The ⊢\underline{e} relation also generalizes the [super^{c}] judgement to allow an arbitrary expression within a super expression’s annotation (in place of this). The generalized judgement permits replacement and substitution lemmas that treat super annotations in the same manner as other expression. Nevertheless, at each reduction step, every super expression’s annotation contains either this or an object. This fact is crucial to proving the soundness of ClassicJava, so we formalize it as a SuperOk predicate.

Definition 3 (Well-Formed Super Calls).

SuperOk(e) ⇔ For all super \underline{≡ e_{0} : c} .md(e_{1}, … e_{n}) in e, either e_{0} = this or ∃ object s.t. e_{0} = object.

Although ⊢\underline{e} types more expressions than ⊢_{e}, we are only concerned with source expressions typed by ⊢_{e}. The following lemma establishes that the new typing judgements conserve the result of the original typing judgements.

Lemma 4 (Conserve). If ⊢_{p} P ⇒ P′ : t and P′ = defn_{1} … defn_{n} e, then P′,∅ ⊢\underline{e} e′ : t.

Proof. The claim follows from a copy-and-patch argument. □

Lemma 5 (Subject Reduction). If P,Γ ⊢\underline{e} e : t, P,Γ ⊢_{σ} S, SuperOk(e), and P ⊢ ⟨e,S⟩ ↪ ⟨e′,S′⟩, then e′ is an error configuration or ∃ Γ′ such that

1. P,Γ′ ⊢\underline{s} e′ : t,

2. P,Γ′ ⊢_{σ} S′, and

3. SuperOk(e′).

Proof. The proof examines reduction steps. For each case, if execution has not halted with an error configuration, we construct the new environment Γ′ and show that the two consequents of the theorem are satisfied relative to the new expression, store, and environment. See Appendix A for the complete proof. □

Lemma 6 (Progress). If P,Γ ⊢\underline{e} e : t, P,Γ ⊢_{σ} S, and SuperOk(e), then either e is a value or there exists an ⟨e′,S′⟩ such that P ⊢ ⟨e,S⟩ ↪ ⟨e′,S′⟩.

Proof. The proof is by analysis of the possible cases for the current redex in e (in the case that e is not a value). See Appendix A for the complete proof. □

By combinining the Subject Reduction and Progress lemmas, we can prove that every non-value ClassicJava program reduces while preserving its type, thus estrablishing the soundness of ClassicJava.

2.5 Related Work on Classes

Our model for class-based object-oriented languages is similar to two recently published semantics for Java [10, 29], but entirely motivated by prior work on Scheme and ML models [14, 19, 30]. 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 [12, 20, 25, 23, 26] or as “native” object calculi (with a record flavor) [1–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^{4} 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 first-order functional programming enriched with a language for expressing hierarchical relationships among data types.

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 9 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

4 Dynamic 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.

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);

} }

/* Cannot merge for 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}));

Fig. 9. Some class definitions and their translation to composable mixins

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 9 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 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 10. Each of the new mixins extends Door^{i} since the right hand mixin in the composition, Secure^{m}, extends Door^{i}.

The 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

interface Secure^{i} extends Door^{i} {

Object neededItem(); } mixin Secure^{m} extends Door^{i} implements Secure^{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 NeedsKey^{m} extends Secure^{i} {

Object neededItem() { return theKey;

} } mixin NeedsSpell^{m} extends Secure^{i} {

Object neededItem() {

return theSpellBook; }

}

mixin Locked^{m} = NeedsKey^{m} compose Secure^{m}; mixin Magic^{m} = NeedsSpell^{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}); …

Fig. 10. Composing mixins for localized parameterization

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 declarations of its superclasses, up to Object.^{5} In MixedJava, 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:

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

– 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 the interfaces that are implemented by its constituents. Composite mixins can be composed with other mixins, producing arbitrarily long chains of atomic mixin compositions.^{6}

Figure 11 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 Secure^{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.

6 Our composition operator is associative semantically, but not type-theoretically. The type system could be strengthened to make composition associative—giving Mixed-Java 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.

[figure: NeedsKey^{m}; neededItem; Secure^{i}; Secure^{m}; neededItem; canOpen; Door^{i}; NeedsSpell^{m}; neededItem; Secure^{i}; Secure^{m}; neededItem; canOpen; Door^{i}; Door^{m}; canPass; canOpen; Locked^{m}; Magic^{m}; LockedMagic^{m}; LockedMagicDoor^{m}]

Fig. 11. The LockedMagicDoor^{m} mixin corresponds to a sequence of atomic mixins

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 12 contains the syntax for MixedJava; the missing productions are inherited from the grammar of ClassicJava in Figure 3. The primary change to the syntax is the replacement of class declarations with mixin declarations. Another change concerns the annotations added by type elaboration. First, view expressions are annotated with the syntactic type of the object expression. Second, a type is no longer included in the super annotation or the field use annotations. In addition, type elaboration inserts extra view expressions into a program to implement subsumption.

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.fd | e.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

Fig. 12. Syntax extensions for MixedJava

The predicates and relations in Figures 13 and 14 (along with the interfacespecific parts of Figures 4 and 5) summarize the syntactic content of a Mixed-Java 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.

MixinsOnce(P)  Each mixin name is declared only once

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

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

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

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

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

NoAbstractMixins(P)  Methods in a mixin are not abstract

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

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′) 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

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) and (m′ <⊲ ^{m}_{P} i xor m′′ <⊲ ^{m}_{P} i))

MixinCompositionsOK(P) Mixins are composed safely

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

MixinMethodsOK(P)  Method definitions match inheritance interface

(⟨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 and visible in a mixin

⟨m′.fd, t⟩ ∈^{m}_{P} m ⇔ m ⊴ ^{m}_{P} m′ and {⟨m′.fd, t⟩} = {⟨m′.fd, t⟩ | m ≤^{m}_{P} m′ and ⟨m′.fd, t⟩ ∈ ∈^{m}_{P} m′}

\underline{∈}^{m}_{P}  Method is potentially visible in a mixin (used for ∈^{m}_{P})
⟨md, T ⟩ \underline{∈}^{m}_{P} m ⇔ (∃V, e s.t. ⟨md, T, V, e⟩ ∈ ∈^{m}_{P} m) or (∃i, V s.t. m ≺^{m}_{P} i and ⟨md, T, V, abstract⟩ ∈^{i}_{P} i) or (\begin{matrix}∃m′, m′′ s.t. m ≐^{m}_{P} m′ ∘ m′′ \\ and (⟨md, T ⟩ \underline{∈}^{m}_{P} m′ or ⟨md, T ⟩ \underline{∈}^{m}_{P} m′′)) \end{matrix}

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

⟨md, T ⟩ ∈^{m}_{P} m ⇔ ⟨md, T ⟩ \underline{∈}^{m}_{P} m and (\begin{matrix}(∃i s.t. m ≺^{m}_{P} i) \\ or (\begin{matrix}∃m′, m′′, i s.t. m ≐^{m}_{P} m′ ∘ m′′ and m′ ≺|^{m}_{P} i \\ and (⟨md, T′⟩ \underline{∈}^{m}_{P} m′ ⇒ ⟨md, T′⟩ ∈^{m}_{P} m′) \\ and (⟨md, T′′⟩ \underline{∈}^{m}_{P} m′′ ⇒ ⟨md, T′′⟩ ∈^{m}_{P} m′′) \\ and (\begin{matrix}(⟨md, T′⟩ ∈^{m}_{P} m′ and ⟨md, T′′⟩ ∈^{m}_{P} m′′) \\ ⇒ (∃V s.t. ⟨md, T, V, abstract⟩ ∈^{i}_{P} i)))) \end{matrix} \end{matrix} \end{matrix}

Fig. 13. Predicates and relations in the model of MixedJava (Part I)

MixinsImplementAll(P) Mixins supply methods to implement interfaces

m ≺ ≺^{m}_{P} i ⟹ (\begin{matrix}∀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′))) \end{matrix}

∈^{i}_{P}  Method with type in an interface

⟨md, T ⟩ ∈^{i}_{P} i ⇔ ∃V s.t. ⟨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}
:: and @  Chain constructors

:: adds an element to the beginning of a chain; @ appends two chains

⟶_{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}  Chains have an inverted subsequence order

M ≤^{M} M′ ⇔ ∃M′′ s.t. M = M′′@M′

•/• ▷ •/•  Mixin view operation selects a new chain

M/m ▷ M′/m′ ⇔ (m = m′ and M = M′) or (\begin{matrix}∃m′′, m′′′ s.t. m ≐^{m}_{P} m′′ ∘ m′′′ \\ and (\begin{matrix}(m′′ ≤^{m}_{P} m′ and M/m′′ ▷ M′/m′) \\ or (m′′′ ≤^{m}_{P} m′ and ∃M_{l}, M_{r} s.t. \begin{matrix}m′′ ⟶_{P} M_{l} and M = M_{l}@M_{r} \\ and M_{r}/m′′′ ▷ M′/m′)) \end{matrix} \end{matrix} \end{matrix}

•/• ▷ •/•  Interface view operation selects a new chain

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

•.• ∝ •.•  Method in a chain is the same as in another chain

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

•∈^{rt}_{P} • in •  Method selects a view within a chain and subchain

⟨md, T, V, e, m::M/m⟩ ∈^{rt}_{P} M_{v} in M_{o}

⇔ ⟨md, T, V, e⟩ ∈ ∈^{m}_{P} m and m_{x}::M_{x} = min\{m_{x}::M_{x} | M_{v}≤^{M}m_{x}::M_{x} and ⟨md, T ⟩ ∈^{m}_{P} m_{x}\} and M_{b} = max\{M′ | m_{x}::M_{x}.md ∝ M′.md\} and m::M = min\{m::M | \begin{matrix}M_{o}≤^{M}m::M \\ and m::M.md ∝ M_{b}.md \\ and ∃V′,e′ s.t. ⟨md, T, V′, e′⟩ ∈ ∈^{m}_{P} m\} \end{matrix}

Fig. 14. Predicates and relations in the model of MixedJava (Part II)

Since each composite mixin has two supertypes, the type graph for mixins is a dag, rather than a tree as for classes. This dag would result in ambiguities if subsumption were based on subtypes. For example, LockedMagic^{m} is a subtype of Secure^{m}, but it contains two copies of Secure^{m} (see Figure 11). Hence, interpreting an instance of LockedMagic^{m} as an instance of Secure^{m} is ambiguous. More concretely, the fragment

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

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

4.2 MixedJava Type Elaboration

Despite the replacement of the subtype relation with the “viewable as” relation, ClassicJava’s type elaboration strategy applies equally well for typing Mixed-Java. The typing rules in Figure 15 are combined with the defn^{i}, meth, let, var, null, and abs rules from Figures 6 and 7.

⊢_{p}

\frac{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′.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′.fd = e′_{v} : t} [set^{m}]

\frac{P, Γ ⊢_{e} e ⇒ e′ : t′  ⟨md, (t_{1} … t_{n} ⟶ t)⟩ ∈_{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}]

\frac{P, Γ ⊢_{e} this ⇒ this : m  m ≺|^{m}_{P} i  ⟨md, (t_{1} … t_{n} ⟶ t)⟩ ∈_{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}

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

⊢_{t}

\frac{t ∈ dom(≺^{m}_{P}) ∪ dom(≐^{m}_{P}) ∪ dom(≺^{i}_{P})∪\{Empty\}}{P ⊢_{t} t} [type^{m}]

Fig. 15. Context-sensitive checks and type elaboration rules for MixedJava

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 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 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.^{7} 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.

Each view is represented as a chain of mixins. The chain is always a subchain of the object’s full chain of mixins, i.e., the chain of mixins for the object’s instantiation type. For example, when an instance of LockedMagicDoor^{m} is used as a Magic^{m} instance, the object’s view corresponds to the boxed part of the following chain:

[NeedsKey^{m} Secure^{m} NeedsSpell^{m} Secure^{m} Door^{m}]

The full chain correponds to LockedMagicDoor^{m} and the boxed part correponds to Magic^{m}. The view designates a specific point in the full mixin chain for selecting methods during dynamic dispatch. With the above view, a search for the neededItem method of the object begins in the NeedsSpell^{m} element of the chain.

Our notation for views exploits the fact that an object in MixedJava encodes its full chain of mixins (in the same way that an object in ClassicJava encodes

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

its class). Thus, the part of the chain before the box is not needed to describe the view:

[ NeedsSpell^{m} Secure^{m} Door^{m}]

Since the view is always at the start of the remaining chain, we can replace the box with the name of the type it represents, which provides a purely textual notation for views:^{8}

[NeedsSpell^{m} Secure^{m} Door^{m}]/Magic^{m}.

The view-based dispatching algorithm, described by the ∈^{rt}_{P} relation, proceeds in two phases. The first phase of a search for 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 determined by the second phase, which locates an overriding declaration of x that is contained in the object’s instantiated mixin. Among the declarations that override the base declaration, the leftmost declaration is selected as the destination, following customary overriding conventions. The location of the overriding declaration determines both the method definition that is invoked and the view of the object within the destination method body (i.e., the view for this).

The dispatching algorithm explains how Secure^{m}’s canOpen method calls the appropriate neededItem method in an instance of LockedMagicDoor^{m}, sometimes dispatching to the method in NeedsKey^{m} and sometimes to the one in NeedsSpell^{m}. The following example illustrates the essence of dispatching from Secure^{m}’s canOpen:

Object canOpen(Secure^{m} o) { … o.neededItem() … }

let door = new LockedMagicDoor^{m}

in canOpen(\underline{view Secure^{m}} view Locked^{m} door) … canOpen(\underline{view Secure^{m}} view Magic^{m} door)

The new LockedMagicDoor^{m} expression produces door as an ⟨object∥view⟩ pair, where object is a new object in the store and view is (recall Figure 11)

[NeedsKey^{m} Secure^{m} NeedsSpell^{m} Secure^{m} Door^{m}]/LockedMagicDoor^{m}.

The view expressions shift the view part of door. Thus, for the first call to canOpen, o is replaced by a reference with the view

[Secure^{m} NeedsSpell^{m} Secure^{m} Door^{m}]/Secure^{m}.

8 We could also use numeric position pairs to denote sub-chains, but the tail/type encoding works better for defining the operational semantics and soundness of Mixed-Java.

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 NeedsKey^{m}, which appears to the left of Secure^{m} in the instantiated chain and extends an interface that contains neededItem.

In contrast, the second call to canOpen receives a reference with the view

[Secure^{m} Door^{m}]/Secure^{m}.

In this view, the base definition of neededItem is in the rightmost Secure^{m} of the full chain, and it is overridden in NeedsSpell^{m}. Neither the definition of neededItem in NeedsKey^{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 16 contains the complete operational semantics for MixedJava as a rewriting system on expression-store pairs, similar to the class semantics described in Section 2.3. In the MixedJava 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.

Theorem 7 (Type Soundness for MixedJava). If ⊢_{p} P ⇒ P′ : t and P′ = defn_{1} … defn_{n} e, then either

– P′ ⊢ ⟨e, ∅⟩ ↪^{∗} ⟨⟨object∥M/t⟩, S⟩ and S(object) = ⟨t′, F⟩ and t′ ≤_{P} t; or – P′ ⊢ ⟨e, ∅⟩ ↪^{∗} ⟨null, S⟩; or

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

– P′ ⊢ ⟨e, ∅⟩ ↪^{∗} ⟨error: dereferenced null, S⟩.

The proof of soundness for MixedJava is analogous to the proof for ClassicJava, but we must update the type of the environment and the environmentstore consistency relation (⊢_{σ}) to reflect the differences between ClassicJava and MixedJava. In MixedJava, the environment Γ maps object-view pairs to the type part of the view, i.e., Γ (⟨object||M/t⟩) = t. The updated consistency relation is defined as follows:

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

E = [ ] | E.fd | E.fd = e | v.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/m⟩], S[object↦⟨m, [M_{1}.fd_{1}↦null, … M_{n}.fd_{n}↦null]⟩]⟩  [new]

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

P ⊢ ⟨E[⟨object∥M/m⟩.fd], S⟩ ↪ ⟨E[v], S⟩  [get]

where S(object) = ⟨m, F⟩ and ⟨m′.fd, t⟩ ∈_{P} m and M/m ▷ M′/m′ and F(M′.fd) = v

P ⊢ ⟨E[⟨object∥M/m⟩.fd = v], S⟩ ↪ ⟨E[v], S[object↦⟨m, F[M′.fd↦v]⟩]⟩  [set]

where S(object) = ⟨m, F⟩ and ⟨m′.fd, t⟩ ∈_{P} m and M/m ▷ M′/m′

P ⊢ ⟨E[⟨object∥M/t⟩.md(v_{1}, … v_{n})], S⟩ ↪ ⟨E[e[⟨object∥m′::M′/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′::M′/m′⟩ ∈^{rt}_{P} M in M_{o}

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

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

P ⊢ ⟨E[view \underline{t′ as} t ⟨object∥M/t′⟩], S⟩ ↪ ⟨E[⟨object∥M′/t⟩], S⟩  [view]

where t′ ⊴ _{P} t and M/t′ ▷ M′/t

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

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

P ⊢ ⟨E[let var = v in e], S⟩ ↪ ⟨E[e[v/var]], S⟩  [let]
P ⊢ ⟨E[view \underline{t′ as} t ⟨object∥M/t′⟩], S⟩ ↪ ⟨error: bad cast, S⟩  [xcast]

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

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

Fig. 16. Operational semantics for MixedJava

Definition 8 (Environment-Store Consistency).

P,Γ ⊢_{σ} S
⇔ (S(object) = ⟨m,F⟩

Σ_{1}: ⇒ (Γ (⟨object||M/t⟩) = t′

⇒ (WF(M/t) and t = t′ and m ≤_{P} t))

Σ_{2}: and dom(F) = {m′::M′.fd | |m| ≤^{M} m′::M′ and

∃ t s.t. ⟨m′.fd,t⟩ ∈∈_{P}^{m} m′}

Σ_{3}: and {object | ⟨object|| ⟩ ∈ rng(F)} ⊆ dom(S) ∪ {null} Σ_{4}: and (F(m′::M′.fd) = ⟨object′||M′′/t′⟩ and ⟨m′.fd,t⟩ ∈∈_{P}^{m} m′)

⇒ (t′ = t))

Σ_{5}: and ⟨object|| ⟩ ∈ dom(Γ) ⇒ object ∈ dom(S) Σ_{6}: and object ∈ dom(S) ⇒ ⟨object|| ⟩ ∈ dom(Γ)

This definition of ⊢_{σ} relies on the WF predicate on views, which is true of wellformed views. A well-formed view combines 1) a chain that is a tail of some mixin’s chain, and 2) a type, either a mixin whose chain is a prefix of the view’s chain or an interface implemented by the first mixin in the view’s chain. Formally, WF is defined as follows:

Definition 9 (Well-Formed View).

WF(M/t) ⇔ ∃ m_{o},M_{o} s.t. m_{o} ⟶_{P} M_{o} and M_{o} ≤^{M} M

and ((∃ M′,M′′ s.t. M = M′ @ M′′ and t ⟶_{P} M′)

or (∃ m,M′ s.t. M = m::M′ and m ⊴_{P} t))

The lemmata for proving MixedJava soundness are mostly the same as for ClassicJava, based on a revised typing relation ⊢\underline{e}. The annotations in MixedJava programs eliminate implicit subsumption by inserting explicit view expressions, so the ⊢\underline{s} relation for proving MixedJava soundness is the same as ⊢\underline{e}. The ⊢\underline{e} relation is like ⊢_{e}, except for the handling of view expressions:

\frac{P,Γ ⊢\underline{e} e : t′}{P,Γ ⊢\underline{e} view \underline{t′ as} t e : t} [cast^{m}]

Also, as in ClassicJava, we define a SuperOk predicate for validating the shape of super calls:

Definition 10 (Well-Formed Super Calls).

SuperOk(e) ⇔ For all super \underline{≡ e_{0}} .md(e_{1}, … e_{n}) in e, either e_{0} = this or ∃ object,M,m s.t. e_{0} = ⟨object||m::M/m⟩

Lemma 11 (Conserve for MixedJava). If ⊢_{p} P ⇒ P′ : t and P′ = defn_{1} … defn_{n} e, then P′,∅ ⊢\underline{e} e′ : t.

Proof. The claim follows from a copy-and-patch argument. □

Lemma 12 (Subject Reduction for MixedJava). If P,Γ ⊢\underline{e} e : t, P,Γ ⊢_{σ} S, SuperOk(e), and ⟨e,S⟩ ↪ ⟨e′,S′⟩, then e′ is an error configuration or ∃ Γ′ such that

1. P,Γ′ ⊢\underline{e} e′ : t,

2. P,Γ′ ⊢_{σ} S′, and

3. SuperOk(e′).

Proof. The proof examines reduction steps. For each case, if execution has not halted with an answer or in an error configuration, we construct the new environment Γ′ and show that the two consequents of the theorem are satisfied relative to the new expression, store, and environment. See Appendix B for the complete proof. □

Lemma 13 (Progress for MixedJava). If P,Γ ⊢\underline{e} e : t, P,Γ ⊢_{σ} S, and SuperOk(e), then either e is a value or there exists an ⟨e′,S′⟩ such that ⟨e,S⟩ ↪ ⟨e′,S′⟩.

Proof. The proof is by analysis of the possible cases for the current redex in e (in the case that e is not a value). See Appendix B for the complete proof. □

By combinining the Subject Reduction and Progress lemmas, we can prove that every non-value MixedJava program reduces while preserving its type, thus estrablishing the soundness of MixedJava.

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. Although this relation depends on two inputs, it nevertheless 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 [11], which makes it difficult to use CLOS for proper mixin programming. The CommonObjects [28] 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 [6–8]. His system is based on earlier work by Cook [9], and its underlying semantics was more recently reformulated in categorical terms by Ancona and Zucca [5]. 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. The language, however, 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.

Agesen et al. [4] suggest that a Java variant with type parameterization can support mixins. Their approach provides a form of separately-compiled mixins. The resulting mixins are less powerful than ours because they do not resolve name collisions. Instead, any name collision introduced by a mixin application triggers a compile-time error.

5 Conclusion

We have presented a language of mixins that relies on the same programming 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. From the programmer’s global perspective, however, 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.

Using mixins is inherently more expensive than using classes, but the additional cost is justified, 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 firstorder systems. In Theoretical Aspects of Computer Software, M. Hagiya and J. C. Mitchell, Eds., vol. 789 of Lecture Notes in Computer Science. 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 (1994), D. Sannella, Ed., vol. 788 of Lecture Notes in Computer Science, Springer-Verlag, pp. 1–25.

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

4. Agesen, O., Freund, S., and Mitchell, J. C. Adding type parameterization to Java. In Proc. ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (Oct. 1997), pp. 49–65.

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

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

7. 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).

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

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

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

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

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

13. Felleisen, M. Programming languages and lambda calculi.

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

14. 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, pp. 235–271.

15. 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 (Sept. 1997), pp. 369–388.

16. Flatt, M. PLT MzScheme: Language manual. Tech. Rep. TR97-280, 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-Wesley, Reading, MA, USA, June 1996.

19. Harper, R., and Stone, C. A type-theoretic interpretation of Standard ML. In Proof, Language and Interaction: Essays in Honour of Robin Milner, G. Plotkin, C. Stirling, and M. Tofte, Eds. MIT Press, 1998.

20. Kamin, S. Inheritance in smalltalk-80: a denotational definition. In Proc. ACM Symposium 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. Palsberg, J., and Schwartzbach, M. I. Object-oriented Type Systems. John Wiley & Sons, 1994.

25. Reddy, U. S. Objects as closures: Abstract semantics of object oriented languages. In Proc. Conference on Lisp and Functional Programming (July 1988), pp. 289– 26. 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, Springer-Verlag, pp. 321–346.

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

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

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

30. Wright, A., and Felleisen, M. A syntactic approach to type soundness. Tech. Rep. 160, Rice University, 1991. Information and Computation, volume 115(1), 1994, pp. 38–94.

Appendix A: ClassicJava Proofs

Lemma 5 (Subject Reduction). If P,Γ ⊢\underline{e} e : t, P,Γ ⊢_{σ} S, SuperOk(e), and P ⊢ ⟨e,S⟩ ↪ ⟨e′,S′⟩, then e′ is an error configuration or ∃ Γ′ such that

1. P,Γ′ ⊢\underline{s} e′ : t,

2. P,Γ′ ⊢_{σ} S′, and

3. SuperOk(e′).

Proof. The proof examines reduction steps. For each case, if execution has not halted with an error configuration, we construct the new environment Γ′ and show that the two consequents of the theorem are satisfied relative to the new expression, store, and environment.

Case [new]. Set Γ′ = Γ [object : c].

1. We have P,Γ ⊢\underline{e} E[new c] : t. From [new], object ∉ dom(S). Then, by Σ_{5}, object ∉ dom(Γ). Thus P,Γ′ ⊢\underline{e} E[new c] : t by Lemma 14. Since P,Γ′ ⊢\underline{e} new c : c and P,Γ′ ⊢\underline{e} object : c, Lemma 15 implies P,Γ′ ⊢\underline{e} E[object] : t.

2. Let S′(object) = ⟨c,F⟩. object is the only new element in dom(S′) and dom(Γ′). Σ_{1}: Γ′(object) = c.

Σ_{2}: dom(F) is correct by construction.

Σ_{3}: rng(F) = {null}.

Σ_{4}: Since rng(F) = {null}, this property is unaffected.

Σ_{5} and Σ_{6}: The only change to Γ and S is object.

3. Since E[object] contains the same super expressions as E[new c], and no instance of this or object is replaced in the new expression, SuperOk(e′) holds.

Case [get].

1. Let t′ be such that P,Γ ⊢\underline{e} object \underline{: c′} .fd : t′. If v is null, it can be typed as t′, so P,Γ′ ⊢\underline{e} E[v] : t by Lemma 15. If v is not null, then by Σ_{4}, S(v) = ⟨c′′, ⟩ where c′′ ≤_{P} t′. By Lemma 17, P,Γ′ ⊢\underline{s} E[v] : t.

2. S and Γ are unchanged.

3. SuperOk(e′) holds because no super expression is changed.

Case [set].

1. The proof is by a straightforward extension of the proof for [get].

2. The only change to the store is a field update; thus only Σ_{3} and Σ_{4} are affected. Let v be the assigned value, and assume that v is not null. Σ_{3}: Since v is typable, it must be in dom(Γ). By Σ_{5}, it is therefore in

dom(S).

Σ_{4}: The typing of the assignment expression demands that the type of v can be treated as the type of the field fd by subsumption. Combining this with Σ_{1} indicates that the type tag of v will preserve Σ_{4}.

3. SuperOk(e′) holds because no super expression is changed.

Case [call].

1. From P,Γ ⊢\underline{e} object.md(v_{1}, … v_{n}) : t we know P,Γ ⊢\underline{e} object : t′, P,Γ ⊢\underline{s} v_{i} : t_{i} for i in [1, n], and ⟨md, (t_{1} … t_{n} → t), (var_{1}, ..., var_{n}), e_{m}⟩ ∈_{P}^{c} t′. The type-checking of P proves that P,t_{0} ⊢\underline{m} t md (t_{1} var_{1}, … t_{n} var_{n}) \{e_{m}\}, which implies that P,[this : t_{0}, var_{1} : t_{1}, … var_{n} : t_{n}] ⊢\underline{s} e_{m} : t where t_{0} is the defining class of md. Further, we know that t′ ≤_{P} t_{0} from ∈_{P}^{c} for methods and ClassMethodsOk(P). Thus, Lemma 16 shows that P,Γ ⊢\underline{s} e_{m}[object/this, v_{1}/var_{1}, … v_{n}/var_{n}] : t.

2. S and Γ are unchanged.

3. The reduction may introduce new super expressions into the complete expression, but each new super must originate directly from P, which contains super expressions with this annotations only. The [object/this] part of the substitution may replace this in a super annotation with object, but no other part of the substitution can affect super annotations. Thus, SuperOk(e′) holds.

Case [super]. The proof is essentially the same as the proof for [call].

Case [cast].

1. By assumption, S(object) = ⟨c, ⟩ where c ≤_{P} t. Since c ≤_{P} t, P,Γ ⊢\underline{s} object : t.

2. S and Γ are unchanged.

3. SuperOk(e′) holds because no super expression is changed.

Case [let].

1. P,Γ ⊢\underline{e} let var = v in e : t implies P,Γ ⊢\underline{e} v : t′ for some type t′ and P,Γ [var : t′] ⊢\underline{e} e : t. By Lemma 16, P,Γ′ ⊢\underline{s} e [v/var] : t.

2. S and Γ are unchanged.

3. SuperOk(e′) holds because no super expression is changed.

Case [xcast], [ncast], [nget], [nset], and [ncall]. e′ is an error configuration. □

Lemma 6 (Progress). If P,Γ ⊢\underline{e} e : t, P,Γ ⊢_{σ} S, and SuperOk(e), then either e is a value or there exists an ⟨e′,S′⟩ such that P ⊢ ⟨e,S⟩ ↪ ⟨e′,S′⟩.

Proof. The proof is by analysis of the possible cases for the current redex in e (in the case that e is not a value).

Case new c. The [new] reduction rules constructs the appropriate e′ and S′. Case v \underline{: c} .fd. If v is null, then the [nget] reduction rule applies. Otherwise, v

= object, and we show that [get] applies.

Type-checking combined with Σ_{5} implies S(object) = ⟨c,F⟩ for some c and F. Type-checking also implies that ⟨c′.fd,t⟩ ∈_{P} c for some c′ by [get^{c}]. By the definition of ∈_{P} (∈_{P}^{c} in this case), we have c ≤_{P} c′. Finally, by Σ_{2}, c′.fd ∈ dom(F).

Case v \underline{: c} .fd = v′. Similar to v \underline{: c} .fd, either [nset] or [set] applies. Case v.md(v_{1}, … v_{n}). If v is null, then the [ncall] reduction rule applies. Oth-

erwise, v = object, and [call] applies: type-checking combined with Σ_{5} implies S(object) = ⟨c,F⟩ for some c and F, and type-checking also implies ⟨md,T,V,e_{m}⟩ ∈_{P}^{c} c.

Case super \underline{≡ v : c} (v_{1}, … v_{n}). By SuperOk(e), v must be of the form object.

Type-checking ensures ⟨md,T,V,e_{m}⟩ ∈_{P}^{c} c. Case view t v. If v is null, then [ncast] applies. Otherwise, v = object, and

by Σ_{5}, S(object) = ⟨c,F⟩ for some c and F. Either [cast] or [xcast] applies, depending on whether c ≤_{P} t.

Case let var = v ∈ e. The [let] reduction always applies, constructing an e′ and S′ (= S). □

Lemma 14 (Free). If P,Γ ⊢\underline{e} e : t and a ∉ dom(Γ), then P,Γ [a : t′] ⊢\underline{e} e : t.

Proof. The claim follows by reasoning about the shape of the derivation. □

Lemma 15 (Replacement). If P,Γ ⊢\underline{e} E[e] : t, P,Γ ⊢\underline{e} e : t′, P,Γ ⊢\underline{e} e′ : t′, then P,Γ ⊢\underline{e} E[e′] : t.

Proof. The proof is a replacement argument in the derivation tree. □

Lemma 16 (Substitution). If P,Γ [var_{1} : t_{1}, … var_{n} : t_{n}] ⊢\underline{e} e : t and \{var_{1}, … var_{n}\} ∩ dom(Γ) = ∅ and P,Γ ⊢\underline{s} v_{i} : t_{i} for i ∈ [1,n], then P,Γ ⊢\underline{s} e [v_{1}/var_{1}, … v_{n}/var_{n}] : t.

Proof. Let σ denote the substitution [v_{1}/var_{1}, … v_{n}/var_{n}], let γ denote the type environment [var_{1} : t_{1}, … var_{n} : t_{n}], and let e′ = σ(e). The proof proceeds by induction on the structure of the derivation showing that P,Γ γ ⊢\underline{e} e : t. We perform a case analysis on the last step in the derivation.

Case e = new c. Since e′ = new c and its type does not depend on Γ, then P,Γ ⊢\underline{e} e′ : c.

Case e = var. If var ∉ dom(σ), then e′ = var and Γ (var) = t, so P,Γ ⊢\underline{e} e′ : t. Otherwise, var = var_{i} for some i ∈ [1,n], and e′ = σ(var_{i}) = v_{i}. By assumption, P,Γ ⊢\underline{s} v_{i} : t_{i}, so P,Γ ⊢\underline{s} e′ : t_{i}.

Case e = null. By [null], any type is derivable for null.

Case e = e_{1} \underline{: c} .fd. By [get^{c}], P,Γ γ ⊢\underline{e} e_{1} : t′ and ⟨c.fd,t⟩ ∈_{P} t′ from some t′. By induction, P,Γ ⊢\underline{e} σ(e_{1}) : t′′ where t′′ is a sub-type of t′. Since ∈_{P} for fields is closed over subtypes on the right-hand side, ⟨c.fd,t⟩ ∈_{P} t′′. Thus, by [get^{c}] on e′ = σ(e_{1}) \underline{: c} .fd, P,Γ ⊢\underline{e} e′ : t.

Case e = e_{1} \underline{: c} .fd = e_{2}. This case is similar to the previous case, relying on subsumption for the right-hand side of an assignment as allowed by [set^{c}].

Case e = view t e_{1}. By [cast^{c}], P,Γ γ ⊢\underline{e} e_{1} : t′ for some t′. By induction, P,Γ ⊢\underline{s} σ(e_{1}) : t′. Since e′ = σ(view t e_{1}) = view t σ(e_{1}), [cast^{c}] gives P, Γ ⊢\underline{e} e′ : t.

Case e = let var = e_{1} in e_{2}. Let σ_{1} = σ and γ_{1} = γ, and lexically rename var in e so that var ∉ dom(γ_{1}). By [let], P,Γ γ_{1} ⊢\underline{e} e_{1} : t_{1}. By induction, P,Γ ⊢\underline{s} σ_{1}(e_{1}) : t_{1}. Let γ_{2} = [var : t_{1}], so that P,Γ γ_{1}γ_{2} ⊢\underline{e} e_{2} : t. Since var ∉ dom(γ_{1}), we can reverse the order of the γ_{1} and γ_{2} extensions to Γ, so P,Γ γ_{2}γ_{1} ⊢\underline{e} e_{2} : t. By induction, P,Γ γ_{2} ⊢\underline{s} σ_{1}(e_{2}) : t. Finally, by [let] on e′ = σ_{1}(let var = e_{1} in e), P,Γ ⊢\underline{s} e′ : t.

Case e = e_{0}.md (e_{1}, … e_{n}). By [call^{c}], P,Γ γ ⊢\underline{s} e_{i} : t_{i} for i ∈ [1,n] and P,Γ γ ⊢\underline{e} e_{0} : t_{0} such that ⟨md, (t_{1} … t_{n} → t), (var_{1}, ..., var_{n}), e_{m}⟩ ∈_{P} t_{0}. By induction, P,Γ ⊢\underline{s} σ(e_{i}) : t_{i} for each e_{i}, and P,Γ ⊢\underline{e} σ(e_{0}) : t_{0}′ where t_{0}′ ≤_{P} t_{0}. Since ∈_{P} must preserve the type of methods over subtypes on the right-hand side (by ClassMethodsOk), ⟨md,(t_{1} … t_{n} → t),(var_{1}′, … var_{n}′),e_{m}′⟩ ∈_{P} t_{0}′. Thus, by [call^{c}] on e′ = σ(e_{0}.md (e_{1}, … e_{n})), P,Γ ⊢\underline{e} e′ : t.

Case e = super \underline{≡ this : c} .md (e_{1}, … e_{n}). This case is similar to the previous case. □

Lemma 17 (Replacement with Subtyping). If P,Γ ⊢\underline{e} E[e] : t, P,Γ ⊢\underline{e} e : t′, and P,Γ ⊢\underline{e} e′ : t′′ where t′′ ≤_{P} t′, then P,Γ ⊢\underline{s} E[e′] : t.

Proof. The proof is by induction on the depth of the evaluation context E. If E is the empty context [ ] we are done. Otherwise, partition E[e] = E_{1}[E_{2}[e]] where E_{2} is a singular evaluation context, i.e., a context whose depth is one. Consider the shape of E_{2}[•], which must be one of:

Case • \underline{: c} .fd. Since c is fixed, •’s type does not matter; the expression’s type is the type of the field.

Case • \underline{: c} .fd = e. Same as the previous case.

Case v \underline{: c} .fd = •. Since [set^{c}] allows subsumption on the right-hand side of the assignment, the type of the expression is the same replacing • with e or e′.

Case •.md(e …). Since t′′ ≤_{P} t′ and methods in an inheritance chain preserve the return type, the type of the expression is the same replacing • with e or e′.

Case v.md(v … • e …). Since [call^{c}] allows subsumption on method arguments, the type of the expression is the same replacing • with e or e′.

Case super \underline{≡ v : c} .md (v … • e …). Same as the previous case.

Case view t •. Since t is fixed, •’s type does not matter in [cast^{c}] (our less restrictive typing rule); the expression’s type is t.

Case let var = • in e_{2}. By [let] with P,Γ ⊢\underline{e} e : t′, P,Γ γ_{1} ⊢\underline{e} e_{2} : t_{1} for some type t_{1} where γ_{1} is [var : t′]. We must show that P,Γ γ_{2} ⊢\underline{s} e_{2} : t_{1} where γ_{2} = [var : t′′], which follows from Lemma 19. □

Definition 18. Γ ≤_{Γ} Γ′ if dom(Γ) = dom(Γ′) and ∀ v ∈ dom(Γ), Γ′(v) ≤_{P} Γ (v).

Lemma 19. If P,Γ ⊢\underline{e} e : t and Γ ≤_{Γ} Γ′, then P,Γ′ ⊢\underline{s} e : t.

Proof. The proof is a straightforward adaptation of the proof for Lemma 16. □

Appendix B: MixedJava Proofs

Lemma 12 (Subject Reduction for MixedJava). If P,Γ ⊢\underline{e} e : t, P,Γ ⊢_{σ} S, SuperOk(e), and ⟨e,S⟩ ↪ ⟨e′,S′⟩, then e′ is an error configuration or ∃ Γ′ such that

1. P,Γ′ ⊢\underline{e} e′ : t,

2. P,Γ′ ⊢_{σ} S′, and

3. SuperOk(e′).

Proof. The proof examines reduction steps. For each case, if execution has not halted with an answer or in an error configuration, we construct the new environment Γ′ and show that the two consequents of the theorem are satisfied relative to the new expression, store, and environment.

Case [new]. Set Γ′ = Γ [⟨object||M/m⟩ : m].

1. We have P,Γ ⊢\underline{e} E[new m] : t. From Σ_{5}, object ∉ dom(S) ⇒ ⟨object|| ⟩ ∉ dom(Γ). Thus P,Γ′ ⊢\underline{e} E[new m] : t by Lemma 20. Since P,Γ′ ⊢\underline{e} new m : m and P,Γ′ ⊢\underline{e} ⟨object||M/m⟩ : m, Lemma 21 implies P,Γ′ ⊢\underline{e} E[⟨object||M/m⟩] : t.

2. Let S′(object) = ⟨m,F⟩, so object is the only new element in dom(S′) and ⟨object||M/m⟩ is the only new element in dom(Γ′). Σ_{1}: Γ′(⟨object||M/m⟩) = m and m ≤_{P} m. Since m ⟶_{P} M, WF(M/m).

Σ_{2}: dom(F) is correct by construction.

Σ_{3}: rng(F) = {null}.

Σ_{4}: Since rng(F) = {null}, this property is unaffected.

Σ_{5} and Σ_{6}: The only addition to the domains of Γ and S is object.

3. Since E[⟨object||M/m⟩] contains the same super expressions as E[new m], and no instance of this or object is replaced in the new expression, SuperOk(e′) holds.

Case [get]. Set Γ′ = Γ.

1. If v is null, it can be typed as t, so P,Γ′ ⊢\underline{e} E[v] : t by Lemma 21. If v is not null, then by Σ_{4}, v = ⟨object||M/t⟩ for some object and M. By Σ_{1}, Γ (v) = t, so by Lemma 21, P,Γ′ ⊢\underline{e} E[v] : t.

2. S and Γ are unchanged.

3. SuperOk(e′) holds because no super expression is changed.

Case [set]. Set Γ′ = Γ.

1. The proof is by a straightforward extension of the proof for [get].

2. The only change to the store is a field update; thus only Σ_{3} and Σ_{4} are affected. Let v be the assigned value, and assume that v is not null. Σ_{3}: Since v is typable, it must be in dom(Γ). By Σ_{5}, its object part is

therefore in dom(S).

Σ_{4}: The typing of the assignment expression indicates that the type of v is t, so v must be of the form ⟨object′||M′′/t⟩.

3. SuperOk(e′) holds because no super expression is changed.

Case [call]. Set Γ′ = Γ [⟨object||m′::M′/m′⟩ : m′].

1. We are given ⟨md, (t_{1} … t_{n} → t), (var_{1}, ..., var_{n}), e_{m}, m′ :: M′/m′⟩ ∈_{P}^{rt} M_{v} in M_{o}, which implies ⟨md,T,V,e_{m}⟩ ∈∈_{P}^{m} m′ by the definition of ∈_{P}^{rt} , where T = (t_{1} … t_{n} → t) and V = (var_{1} … var_{n}). We are also given P,Γ ⊢\underline{e} ⟨object||M_{v}/t′⟩.md(v_{1}, … v_{n}) : t, which implies ⟨md,T′⟩ ∈_{P} t′. By Lemma 25, T′ = T. Since the method call type-checks and T′ = T, P,Γ ⊢\underline{e} v_{i} : t_{i} for i in [1, n]. Type-checking for the program P ensures that P,m′ ⊢\underline{m} t md (t_{1} var_{1}, … t_{n} var_{n}) \{e_{m}\}, and thus P,[this : m′, var_{1} : t_{1}, … var_{n} : t_{n}] ⊢\underline{e} e : t. Hence, by Lemma 22, P,Γ′ ⊢\underline{e} e_{m}[⟨object||m′::M′/m′⟩/this, v_{1}/var_{1}, … v_{n}/var_{n}] : t.

2. S′ = S. If Γ′ contained a mapping for ⟨object||m′::M′/m′⟩, it was m′ by Σ_{1}, so Γ′ = Γ. Otherwise, ⟨object||m′::M′/m′⟩ is new in Γ′, which might affect Σ_{1}, Σ_{5}, and Σ_{6}: Σ_{1}: Γ′(⟨object||m′::M′/m′⟩) = m′. The ∈_{P}^{rt} relation ensures that m ≤_{P}

m′ because M_{o} ≤^{M} m′::M′. WF(m′::M′/m′) is immediate.

Σ_{5} and Σ_{6}: Since Γ (⟨object||M_{v}/t′⟩) = t′, object ∈ dom(S) by Σ_{5} on S and Γ. Thus, adding ⟨object||m′::M′/m′⟩ to Γ′ does not require any new elements in S′.

3. The reduction may introduce new super expressions into the complete expression, but each new super expression must originate directly from P, which contains super expressions with this annotations only. The [⟨object||m′::M′/m′⟩/this] part of the substitution may replace this in a super annotation with ⟨object||m′::M′/m′⟩, but no other part of the substitution can affect super annotations. Thus, SuperOk(e′) holds.

Case [super]. Set Γ′ = Γ [⟨object||m′::M′/m′⟩ : m′].

1. Similar to [call]. The object for dispatching is ⟨object||m::M/m⟩, and we are given m ≺_{P}^{m} i and ⟨md,T ⟩ ∈_{P} i. (The i in [super^{m}] and the i in [call] are the same, since a mixin extends only one interface.) To apply Lemma 25, we need WF(M′′/i), where M/i ▷ M′′/i. Lemma 23 is not strong enough to gurantee WF(M′′/i), since M/i is not necessarily well-formed. However, ▷ with an interface always produces a well-formed view on the right-hand side by construction, so WF(M′′/i). Thus, we can apply Lemma 25 as for [call].

2. Similar to [call]. If ⟨object||m′::M′/m′⟩ is new:

Σ_{1}: Γ′(⟨object||m′::M′/m′⟩) = m′. If S(object) = ⟨m_{o}, ⟩, m_{o} ≤_{P} m′ because Σ_{1} on Γ ensures that the original view m::M is part of m_{o}, ▷ selects a sub-view of M as M′′, and ∈_{P}^{rt} selects m′::M′ within M′′.

Σ_{5} and Σ_{6}: Same as [call].

3. Same as [call].

Case [view]. Set Γ′ = Γ [⟨object||M′/t⟩ : t].

1. Since Γ (⟨object||M′/t⟩) = t, by Lemma 21, P,Γ′ ⊢\underline{e} E[⟨object||M′/t⟩] : t.

2. Similar to [call]. If ⟨object||M′/t⟩ ∉ Γ:

Σ_{1}: Γ′(⟨object||M′/t⟩) = t. The side condition for [view] requires t′ ⊴_{P} t, which implies t′ ≤_{P} t. Σ_{1} on Γ ensures m ≤_{P} t′ when S(object)

= ⟨m, ⟩, so m ≤_{P} t by transitivity.

Σ_{5} and Σ_{6}: Same as [call].

3. SuperOk(e′) holds because no super expression is changed.

Case [cast]. Set Γ′ = Γ [⟨object||M′′/t⟩ : t].

1. Same as [view].

2. Similar to [call]. If ⟨object||M′′/t⟩ is new:

Σ_{1}: Γ′(⟨object||M′′/t⟩) = t. The side condition for [cast] requires m ⊴_{P} t, which implies m ≤_{P} t.

Σ_{5} and Σ_{6}: Same as [call].

3. SuperOk(e′) holds because no super expression is changed.

Case [let]. P,Γ ⊢\underline{e} let var = v in e : t implies P,Γ ⊢\underline{e} v : t′ for some type t′ and P,Γ [var : t′] ⊢\underline{e} e : t. Set Γ′ = Γ.

1. By Lemma 22, P,Γ′ ⊢\underline{e} e [v/var] : t.

2. S and Γ are unchanged.

3. SuperOk(e′) holds because no super expression is changed.

Case [xcast], [ncast], [nget], [nset] and [ncall]. e′ is an error configuration. □

Lemma 13 (Progress for MixedJava). If P,Γ ⊢\underline{e} e : t, P,Γ ⊢_{σ} S, and SuperOk(e), then either e is a value or there exists an ⟨e′,S′⟩ such that ⟨e,S⟩ ↪ ⟨e′,S′⟩.

Proof. The proof is by analysis of the possible cases for the current redex in e (in the case that e is not a value).

Case new m. The [new] reduction rules constructs the appropriate e′ and S′. Case v.fd. If v is null, then the [nget] reduction rule applies. Otherwise, v =

⟨object||M/t⟩, and we show that [get] applies. Type-checking combined with Σ_{5} implies S(object) = ⟨m_{o},F⟩ for some m_{o} and F. Type-checking also implies that t = m for some mixin m, and ⟨m′.fd,t⟩ ∈_{P} m for some m′ by [get^{m}]. By the definition of ∈_{P} (∈_{P}^{m} in this case), we have m ⊴_{P} m′, so there is a unique m′ such that M/m ▷ M′/m′, and M ≤^{M} M′. Environment-store consistency implies M_{o} ≤^{M} M, where m_{o} ⟶_{P} M_{o}. By transitivity, M_{o} ≤^{M} M′. Finally, by Σ_{2}, M′.fd ∈ dom(F).

Case v.fd = v′. Similar to v.fd; either [nset] or [set] applies. Case v.md(v_{1}, … v_{n}). If v is null, then the [ncall] reduction rule applies. Oth-

erwise, v = ⟨object||M/t′⟩, and we show that [call] applies. Type-checking combined with Σ_{5} implies S(object) = ⟨m_{o},F⟩ for some m_{o} and F. Define M_{o} as m_{o} ⟶_{P} M_{o}. By [call^{m}], ⟨md, T ⟩ ∈_{P} t′. The ∈_{P}^{rt} relation necessarily selects some m′::M′/m′ and e:

1. m_{x}::M_{x} exists because WF(M/t′) and ⟨md,T ⟩ ∈_{P} t′ implies that some atomic mixin in M contains md.

2. M_{b} exists because ∝ can at least relate m_{x}::M_{x}.md to itself. More specifically, we know that M_{b} starts with an atomic mixin m_{b} such that ⟨md,T,V,e⟩ ∈∈_{P}^{m} m_{b}:

– If there is no i such that m_{x} ≺_{P}^{m} i and ⟨md,T ⟩ ∈_{P} i, then ⟨md,T,V,e⟩ ∈∈_{P}^{m} m_{x} by the definition of ∈_{P}^{m}.

– Otherwise, there must be some m_{y}::M_{y} such that M_{x}/i ▷ m_{y}::M_{y}/i, or else m_{o} would not be a proper mixin composition. Thus, m_{x}::M_{x}.md ∝ m_{y}::M_{y}.md where m_{x}::M_{x} ≤^{M} m_{y}::M_{y}. This argument on m_{x}::M_{x} applies inductively to m_{y}::M_{y}, showing that ⟨md,T,V,e⟩ ∈∈_{P}^{m} m_{b}.

3. By WF(M/t′) and M ≤^{M} M_{b}, then M_{o} ≤^{M} M_{b}, so the final phase of the ∈_{P}^{rt} calculation must succeed (although the selected view is not necessarily M_{b}).

Case super \underline{≡ v} (v_{1}, … v_{n}). By SuperOk(e), v must be of the form ⟨object||m::M/m⟩. Thus, we show that the [super] reduction applies. Since m ≺_{P}^{m} i, there must be some atomic mixin in M that implements i, otherwise the object’s instantiation mixin would not be a proper composition. Thus, there is some M′ such that M/i ▷ M′/i. Since type-checking ensures that ⟨md,T ⟩ ∈_{P} i, we can apply the same reasoning as for the v.md(v_{1}, … v_{n}) case, showing that the ∈_{P}^{rt} relation necessarily selects some m′::M′/m′ and e.

Case view \underline{t′ as} t v. If v is null, then [ncast] applies. Otherwise, v = ⟨object||M/t′⟩ for some M, and by Σ_{5} S(object) = ⟨m_{o},F⟩ for some m_{o} and F. If t′ ⊴_{P} t, then [view] applies since M′/t clearly exists for M/t ▷ M′/t. Assume that t′ ⋬_{P} t. If m_{o} ⋬_{P} t′, then [xcast] applies. Otherwise, [cast] applies since m_{o} ⊴_{P} t means that M′′/t clearly exists for M′/m ▷ M′′/t, where m ⟶_{P} M′.

Case let var = v ∈ e. The [let] reduction always applies, constructing an e′ and S′ (= S). □

By combinining the Subject Reduction and Progress lemmas, we can prove that every non-value MixedJava program reduces while preserving its type, thus estrablishing the soundness of MixedJava.

Lemma 20 (Free for MixedJava). If P,Γ ⊢\underline{e} e : t and a ∉ dom(Γ), then P,Γ [a : t′] ⊢\underline{e} e : t.

Proof. This follows by reasoning about the shape of the derivation. □

Lemma 21 (Replacement for MixedJava). If P,Γ ⊢\underline{e} E[e] : t, P,Γ ⊢\underline{e} e : t′, and P,Γ ⊢\underline{e} e′ : t′, then P,Γ ⊢\underline{e} E[e′] : t.

Proof. The proof is a replacement argument in the derivation tree. □

Lemma 22 (Substitution for MixedJava). If P,Γ [var_{1} : t_{1}, … var_{n} : t_{n}] ⊢\underline{e} e : t and \{var_{1}, … var_{n}\} ∩ dom(Γ) = ∅ and P,Γ ⊢\underline{s} v_{i} : t_{i} for i ∈ [1,n], then P,Γ ⊢\underline{e} e [v_{1}/var_{1}, … v_{n}/var_{n}] : t.

Proof. Unlike the Substituion lemma for ClassicJava, the proof of this lemma follows simply from reasoning about the shape of the derivation, since it makes no claims about subsumption. The proof uses nested induction over the number of variables var_{1}, … var_{n} and over the number of replacements for each variable. □

Lemma 23 (•/• ▷ •/• Preserves Well-Formedness). If WF(M/t), and M/t ▷ M′/t′, then WF(M′/t′).

Proof. There are two cases, depending on whether t′ is a mixin or an interface:

Case t and t′ are mixins, m and m′. The proof is by lexicographic induction on the length of M and size of m (i.e., the number atomic mixins composed to define m). If M is [m] (the base case), then t′ = m, M′ = M, and WF([m′]/m′). Also, if m = m′ and M = M′, then WF(M/m) = WF(M′/m′). Otherwise, m′ = m′′ ∘ m′′′, and there are two sub-cases:

– If m′′ ≤_{P}^{M} m′ and M/m′′ ▷ M′/m′, then WF(M′/m′) by induction: m′′ is smaller than m, and WF(M/m′′) since m′′ is a prefix of m.

– If m′′′ ≤_{P}^{M} m′ and M_{r}/m′′′ ▷ M′/m′, then WF(M′/m′) by induction: M_{r} is smaller than M, and WF(M_{r}/m′′′) because m′′′ is a prefix of M_{r}.

Case t′ is an interface, i. M′ is constructed as m::M′′ where m ≺≺_{P}^{m} i. Thus, WF(M′/i) because M′ = m::M′′ and m ⊴_{P} i. □

Lemma 24 (Consistency of •.• ∝ •.•). If ⟨md,T ⟩ ∈_{P} m and m::M.md ∝ m′::M′.md, then ⟨md,T ⟩ ∈_{P} m′.

Proof. The proof is by induction on the length of M. If M = [], then m′ = m and M′ = [], because ▷ (used in the definition of ∝) cannot select any chain other than [m].

Otherwise, m ≺_{P}^{m} i for some i where ⟨md,T ⟩ ∈_{P}^{i} i. Since M/i ▷ M′′/i and ▷ preserves well-formedness of views, M′′ is of the form m′′::M′′′ for some m′′ and M′′′ where m′′ ≺_{P}^{m} i. By MixinsImplementAll, MixinMethodsOk, m′′ ≺_{P}^{m} i, and ⟨md,T ⟩ ∈_{P}^{i} i, we have ⟨md,T ⟩ ∈_{P} m′′. Finally, m′′::M′′′.md ∝ m′::M′, so ⟨md,T ⟩ ∈_{P} m′ by induction. □

Lemma 25 (Soundess of • ∈_{P}^{rt} • in •). If ⟨md,T, , ,m::M/m⟩ ∈_{P}^{rt} M_{v} in M_{o}, WF(M_{v}/t_{v}), and ⟨md,T′⟩ ∈_{P} t_{v}, then T = T′.

Proof. To get ⟨md,T, , ,m::M/m⟩, the ∈_{P}^{rt} relation first finds m_{x}::M_{x} such that ⟨md,T′′⟩ ∈_{P} m_{x}. Since WF(M_{v}/t_{v}) and ⟨md,T′⟩ ∈_{P} t_{v}, then T′′ = T′ by reasoning about the possible forms of t:

Case t_{v} is an interface i. Then, WF(M_{v}/t_{v}) implies m_{x}::M_{x} = M_{v} and m_{x} ⊴_{P} t. Since m_{x} ⊴_{P} t, T′′ = T′ by MixinMethodsOk and MixinsImplementAll.

Case t_{v} is an atomic mixin m′. Then, WF(M_{v}/t_{v}) implies m_{x}::M_{x} = M_{v} and m_{x} = t, so T′′ = T′ by MethodOncePerMixin.

Case t_{v} is a composite mixin m′. Then, ⟨md,T′⟩ ∈_{P} t_{v} implies ⟨md,T′⟩ ∈_{P}^{m} m′′ for some m′′ where m′ ≤_{P} m′′, which means that some canditate for m_{x} exists within m′. Furthermore, ⟨md,T′′′⟩ ∈_{P}^{m} m′′ where m′ ≤_{P} m′′ implies T′′′ = T′′ by the definition of ∈_{P}^{m} (because ∈_{P}^{m} eliminates ambiguities), so every candidate for m_{x} with m′ gives the same type to method md. Since M_{v} starts with the chain of atomic mixins of m′, then m_{x} must be part of m′. Finally, T′′ = T′ because m′ ≤_{P} m_{x}.

Next, ∈_{P}^{rt} finds an M_{b} such that m_{x}::M_{x}.md ∝ M_{b}.md. From WF(m_{x}::M_{x}/m_{x}), ⟨md,T′⟩ ∈_{P} m_{x}, and Lemma 24, the first element of M_{b} must be an atomic mixin m_{b} such that ⟨md,T′⟩ ∈_{P} m_{b}. Finally, the ∈_{P}^{rt} relation selects a m::M such that ⟨md,T, , ⟩ ∈∈_{P}^{m} m and m::M.md ∝ M_{b}.md. Thus, by Lemma 24 again, ⟨md,T ⟩ ∈_{P} m_{b}. Since m_{b} is an atomic mixin, ∈_{P}^{m} implies ∈∈_{P}^{m}, so we have both ⟨md,T, , ⟩ ∈∈_{P}^{m} m_{b} and ⟨md,T′, , ⟩ ∈∈_{P}^{m} m_{b}. By MethodOncePerMixin, those must be the same method in m_{b}, so T = T′. □