Featherweight Java

A Minimal Core Calculus for Java and GJ

Atsushi Igarashi Dept. of Comp. & Info. Sci. University of Pennsylvania

igarasha@saul.cis.upenn.edu

Benjamin Pierce Dept. of Comp. & Info. Sci. University of Pennsylvania

bcpierce@cis.upenn.edu

Philip Wadler Bell Laboratories Lucent Technologies

                wadler@research.bell-labs.com

Abstract

Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step further, omitting almost all features of the full language (including interfaces and even assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only possible but easy.

Featherweight Java bears a similar relation to full Java as the lambda-calculus does to languages such as ML and Haskell. It offers a similar computational “feel,” providing classes, methods, fields, inheritance, and dynamic typecasts, with a semantics closely following Java’s. A proof of type safety for Featherweight Java thus illustrates many of the interesting features of a safety proof for the full language, while remaining pleasingly compact. The syntax, type rules, and operational semantics of Featherweight Java fit on one page, making it easier to understand the consequences of extensions and variations.

As an illustration of its utility in this regard, we extend Featherweight Java with generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and sketch a proof of type safety. The extended system formalizes for the first time some of the key features of GJ.

Subject areas: theoretical foundations, language design and implementation.

1 Introduction

“Inside every large language is a small language struggling to get out...”

Formal modeling can offer a significant boost to the design of complex real-world artifacts such as programming languages. A formal model may be used to describe some aspect of a design precisely, to state and prove its properties, and to direct attention to issues that might otherwise be overlooked. In formulating a model, however, there is a tension between completeness and compactness: the more aspects the model addresses at the same time, the more unwieldy it becomes. Often it is sensible to choose a model that is less complete but more compact, offering maximum insight for minimum investment. This strategy may be seen in a flurry of recent papers on the formal properties of Java, which omit advanced features such as concurrency and reflection and concentrate on fragments of the full language to which well-understood theory can be applied.

We propose Featherweight Java, or FJ, as a new contender for a minimal core calculus for modeling Java’s type system. The design of FJ favors compactness over completeness almost obsessively, having just five forms of expression: object creation, method invocation, field access, casting, and variables. Its syntax, typing rules, and operational semantics fit comfortably on a single page. Indeed, our aim has been to omit as many features as possible – even assignment – while retaining the core features of Java typing. There is a direct correspondence between FJ and a purely functional core of Java, in the sense that every FJ program is literally an executable Java program.

FJ is only a little larger than Church’s lambda calculus [3] or Abadi and Cardelli’s object calculus [1], and is significantly smaller than previous formal models of class-based languages like Java, including those put forth by Drossopoulou, Eisenbach, and Khurshid [?], Syme [20], Nipkow and Oheimb [17], and Flatt, Krishnamurthi, and Felleisen [14]. Being smaller, FJ lets us focus on just a few key issues. For example, we have discovered that capturing the behavior of Java’s cast construct in a traditional “small-step” operational semantics is trickier than we would have expected, a point that has been overlooked or underemphasized in other models.

One use of FJ is as a starting point for modeling languages that extend Java. Because FJ is so compact, we can focus attention on essential aspects of the extension. Moreover, because the proof of soundness for pure FJ is very simple, a rigorous soundness proof for even a significant extension may remain manageable. The second part of the paper illustrates this utility by enriching FJ with generic classes and methods à la GJ [7]. Although, the model omits a few important aspects of GJ (such as “raw types” and type argument inference for generic method calls), it has already revealed portions of the design that were underspecified and bugs in the GJ compiler.

Our main goal in designing FJ was to make a proof of type soundness (“well-typed programs don’t get stuck”) as concise as possible, while still capturing the essence of the soundness argument for the full Java language. Any language feature that made the soundness proof longer without making it significantly different was a candidate for omission. As in previous studies of type soundness in Java, we don’t treat advanced features such as concurrency, inner classes, and reflection. Other Java features omitted from FJ include assignment, interfaces, overloading, messages to super, null pointers, base types (int, bool, etc.), abstract method declarations, shadowing of superclass fields by subclass fields, access control (public, private, etc.), and exceptions. The features of Java that we do model include mutually recursive class definitions, object creation, field access, method invocation, method override, method recursion through this, subtyping, and casting.

One key simplification in FJ is the omission of assignment. We assume that an object’s fields are initialized by its constructor and never changed afterwards. This restricts FJ to a “functional” fragment of Java, in which many common Java idioms, such as use of enumerations, cannot be represented. Nonetheless, this fragment is computationally complete (it is easy to encode the lambda calculus into it), and is large enough to include many useful programs (many of the programs in Felleisen and Friedman’s Java text [12] use a purely functional style). Moreover, most of the tricky typing issues in both Java and GJ are independent of assignment. An important exception is that the type inference algorithm for generic method invocation in GJ has some twists imposed on it by the need to maintain soundness in the presence of assignment. This paper treats a simplified version of GJ without type inference.

The remainder of this paper is organized as follows. Section 2 introduces the main ideas of Featherweight Java, presents its syntax, type rules, and reduction rules, and sketches a type soundness proof. Section 3 extends Featherweight Java to Featherweight GJ, which includes generic classes and methods. Section 4 presents an erasure map from FGJ to FJ, modeling the techniques used to compile GJ into Java. Section 5 discusses related work, and Section 6 concludes.

2 Featherweight Java

In FJ, a program consists of a collection of class definitions plus an expression to be evaluated. (This expression corresponds to the body of the main method in Java.) Here are some typical class definitions in FJ.

     class Pair extends Object {
       Object fst;
       Object snd;
       Pair(Object fst, Object snd) {
         super(); this.fst=fst; this.snd=snd;
       }
       Pair setfst(Object newfst) {
         return new Pair(newfst, this.snd);
       }

                                                                }
                                                                class A extends Object {
                                                                  A() { super(); }
                                                                }
                                                                class B extends Object {
                                                                  B() { super(); }
                                                                }

For the sake of syntactic regularity, we always include the supertype (even when it is Object), we always write out the constructor (even for the trivial classes A and B), and we always write the receiver for a field access (as in this.snd) or a method invocation. Constructors always take the same stylized form: there is one parameter for each field, with the same name as the field; the super constructor is invoked on the fields of the supertype; and the remaining fields are initialized to the corresponding parameters. Here the supertype is always Object, which has no fields, so the invocations of super have no arguments. Constructors are the only place where super or = appears in an FJ program. Since FJ provides no side-effecting operations, a method body always consists of return followed by an expression, as in the body of setfst().

In the context of the above definitions, the expression

                                                                new Pair(new A(), new B()).setfst(new B())

evaluates to the expression

                                                                new Pair(new B(), new B()).

There are five forms of expression in FJ. Here, new A(), new B(), and new Pair(e1,e2) are object constructors, and e3.setfst(e4) is a method invocation. In the body of setfst, the expression this.snd is a field access, and the occurrences of newfst and this are variables. FJ differs from Java in that this is an ordinary variable rather than a special keyword.

The remaining form of expression is a cast. The expression

                                                                ((Pair)new Pair(new Pair(new A(), new B()),
                                                                                 new A()).fst).snd

evaluates to the expression

                                                                new B().
                                                    Here, ((Pair)e7), where e7 is new Pair(...).fst, is

a cast. The cast is required, because e7 is a field access to fst, which is declared to contain an Object, whereas the next field access, to snd, is only valid on a Pair. At run time, it is checked whether the Object stored in the fst field is a Pair (and in this case the check succeeds). In Java, one may prefix a field or parameter declaration with the keyword final to indicate that it may not be assigned to, and all parameters accessed from an inner class must be declared final. Since FJ contains no assignment and no inner classes, it matters little whether or not final appears, so we omit it for brevity. Dropping side effects has a pleasant side effect: evaluation can be easily formalized entirely within the syntax of FJ, with no additional mechanisms for modeling the heap. Moreover, in the absence of side effects, the order in which expressions are evaluated does not affect the final outcome, so we can define the operational semantics of FJ straightforwardly using a nondeterministic small-step reduction relation, following longstanding tradition in the lambda calculus. Of course, Java’s call-by-value evaluation strategy is subsumed by this more general relation, so the soundness properties we prove for reduction will hold for Java’s evaluation strategy as a special case.

There are three basic computation rules: one for field access, one for method invocation, and one for casts. Recall that, in the lambda calculus, the beta-reduction rule for applications assumes that the function is first simplified to a lambda abstraction. Similarly, in FJ the reduction rules assume the object operated upon is first simplified to a new expression. Thus, just as the slogan for the lambda calculus is “everything is a function,” here the slogan is “everything is an object.”

Here is the rule for field access in action:

new Pair(new A(), new B()).snd ⟶ new B()

Because of the stylized form for object constructors, we know that the constructor has one parameter for each field, in the same order that the fields are declared. Here the fields are fst and snd, and an access to the snd field selects the second parameter.

Here is the rule for method invocation in action (/ denotes substitution):

new Pair(new A(), new B()).setfst(new B())

⟶ [ \begin{matrix}new B()/newfst, \\ new Pair(new A(),new B())/this \end{matrix} ]

new Pair(newfst, this.snd)

i.e., new Pair(new B(),

new Pair(new A(), new B()).snd)

The receiver of the invocation is the object

new Pair(new A(), new B()), so we look up the

setfst method in the Pair class, where we find that it has formal parameter newfst and body

new Pair(newfst, this.snd). The invocation reduces

to the body with the formal parameter replaced by the actual, and the special variable this replaced by the receiver object. This is similar to the beta rule of the lambda calculus, (λx.e0)e1 ⟶ [e1/x]e0. The key differences are the fact that the class of the receiver determines where to look for the body (supporting method override), and the substitution of the receiver for this (supporting “recursion through self”). Readers familiar with Abadi and Cardelli’s Object Calculus will see a strong similarity to their ς reduction rule [1]. In FJ, as in the lambda calculus and the pure Abadi-Cardelli calculus, if a formal parameter appears more than once in the body this may lead duplication of the actual, but since there are no side effects this causes no problems.

Here is the rule for a cast in action:

(Pair)new Pair(new A(), new B())

⟶ new Pair(new A(), new B())

Once the subject of the cast is reduced to an object, it is easy to check that the class of the constructor is a subclass of the target of the cast. If so, as is the case here, then the reduction removes the cast. If not, as in the expression (A)new B(), then no rule applies and the computation is stuck, denoting a run-time error.

There are three ways in which a computation may get stuck: an attempt to access a field not declared for the class, an attempt to invoke a method not declared for the class (“message not understood”), or an attempt to cast to something other than a superclass of the class. We will prove that the first two of these never happen in well-typed programs, and the third never happens in well-typed programs that contain no downcasts (or “stupid casts”—a technicality explained below).

As usual, we allow reductions to apply to any subexpression of an expression. Here is a computation for the second example expression, where the next subexpression to be reduced is underlined at each step.

          ((Pair)new Pair(new Pair(new A(),
                  new B()), new A()).fst).snd

     ⟶ \underline{((Pair)new Pair(new A(),new B()))}.snd

⟶

          new Pair(new A(), new B()).snd

     ⟶ new B()

We will prove a type soundness result for FJ: if an expression e reduces to expression e′, and if e is well typed, then e′ is also well typed and its type is a subtype of the type of e.

With this informal introduction in mind, we may now proceed to a formal definition of FJ.

2.1 Syntax

The syntax, typing rules, and computation rules for FJ are given in Figure 1, with a few auxiliary functions in Figure 2.

The metavariables A, B, C, D, and E range over class names; f and g range over field names; m ranges over method names; x ranges over parameter names; d and e range over expressions; CL ranges over class declarations; K ranges over constructor declarations; and M ranges over method declarations. We write \overline{f} as shorthand for f_{1},…,f_{n} (and similarly for \overline{C}, \overline{x}, \overline{e}, etc.) and write \overline{M} as shorthand for M_{1}… M_{n} (with no commas). We write the empty sequence as • and denote concatenation of sequences using a comma. The length of a sequence \overline{x} is written #(\overline{x}). We abbreviate operations on pairs of sequences in the obvious way, writing “\overline{C} \overline{f}” as shorthand for “C_{1} f_{1},…,C_{n} f_{n}”, and similarly “\overline{C} \overline{f};” as shorthand for “C_{1} f_{1};… C_{n} f_{n};”, and “this.\overline{f}=\overline{f};” as shorthand for “this.f_{1}=f_{1};…;this.f_{n}=f_{n};”. Sequences of field declarations, parameter names, and method declarations are assumed to contain no duplicate names.

A class table CT is a mapping from class names C to class declarations CL. A program is a pair (CT , e) of a class table and an expression. To lighten the notation in what follows, we always assume a fixed class table CT .

The abstract syntax of FJ class declarations, constructor declarations, method declarations, and expressions is given at the top left of Figure 1. As in Java, we assume that casts bind less tightly than other forms of expression. We assume that the set of variables includes the special variable this, but that this is never used as the name of an argument to a method.

Every class has a superclass, declared with extends. This raises a question: what is the superclass of the Syntax:

CL ::= class C extends C \{\overline{C} \overline{f}; K \overline{M}\}
K ::= C(\overline{C} \overline{f}) \{super(\overline{f}); this.\overline{f} = \overline{f};\}
M ::= C m(\overline{C} \overline{x}) \{return e;\}

e ::= x

     | e.f
     | e.m(\overline{e})
     | new C(\overline{e})
     | (C)e

Subtyping:

             C<:C

        C<:D    D<:E C<:E
\frac{CT (C) = class C extends D \{...\}}{C<:D}

Computation:

\frac{fields(C) = \overline{C} \overline{f}}{(new C(\overline{e})).f_{i} ⟶ e_{i}}  (R-Field)

 \frac{mbody(m, C) = (\overline{x}, e_{0})}{(new C(\overline{e})).m(\overline{d}) ⟶ [\overline{x} ↦ \overline{d}, this ↦ new C(\overline{e})]e_{0}}  (R-Invk)
  C<:D ; (D)(new C(\overline{e})) ⟶ new C(\overline{e})  (R-Cast)

Expression typing:

Γ ⊢ x ∈ Γ(x)  (T-Var)
\frac{Γ ⊢ e_{0} ∈ C_{0}  fields(C_{0}) = \overline{C} \overline{f}}{Γ ⊢ e_{0}.f_{i} ∈ C_{i}}  (T-Field)
\frac{Γ ⊢ e_{0} ∈ C_{0} mtype(m, C_{0}) = \overline{D}→C Γ ⊢ \overline{e} ∈ \overline{C}    \overline{C} <: \overline{D}}{Γ ⊢ e_{0}.m(\overline{e}) ∈ C}  (T-Invk)
\frac{fields(C) = \overline{D} \overline{f} Γ ⊢ \overline{e} ∈ \overline{C}    \overline{C} <: \overline{D}}{Γ ⊢ new C(\overline{e}) ∈ C}  (T-New)
\frac{Γ ⊢ e_{0} ∈ D    D <: C}{Γ ⊢ (C)e_{0} ∈ C}  (T-UCast)
\frac{Γ ⊢ e_{0} ∈ D    C <: D    C ≠ D}{Γ ⊢ (C)e_{0} ∈ C}  (T-DCast)
\frac{Γ ⊢ e_{0} ∈ D    C≮:D    D≮:C stupid warning}{Γ ⊢ (C)e_{0} ∈ C}  (T-SCast)

Method typing:

                                                   \frac{\overline{x} : \overline{C}, this : C ⊢ e_{0} ∈ E_{0}  E_{0} <: C_{0} CT (C) = class C extends D \{...\} override(\overline{C}→C_{0}, m, D)}{C_{0} m (\overline{C} \overline{x}) \{return e_{0};\} OK IN C}

Class typing:

                                                \frac{K = C(\overline{D} \overline{g}, \overline{C} \overline{f}) \{super(\overline{g}); this.\overline{f} = \overline{f};\} fields(D) = \overline{D} \overline{g}    \overline{M} OK IN C}{class C extends D \{\overline{C} \overline{f}; K \overline{M}\} OK}

Figure 1: FJ: Main definitions Field lookup:

fields(Object) = •

\frac{CT (C) = class C extends D \{\overline{C} \overline{f}; K \overline{M}\} fields(D) = \overline{D} \overline{g}}{fields(C) = \overline{D} \overline{g}, \overline{C} \overline{f}}

Method type lookup:

\frac{CT (C) = class C extends D \{\overline{C} \overline{f}; K \overline{M}\} \overline{M}(m) = B m (\overline{B} \overline{x}) \{return e;\}}{mtype(m, C) = \overline{B}→B}

\frac{CT (C) = class C extends D \{\overline{C} \overline{f}; K \overline{M}\} m is not defined in \overline{M}}{mtype(m, C) = mtype(m, D)} Method body lookup:

 \frac{CT (C) = class C extends D \{\overline{C} \overline{f}; K \overline{M}\} \overline{M}(m) = B m (\overline{B} \overline{x}) \{return e;\}}{mbody(m, C) = (\overline{x}, e)}

\frac{CT (C) = class C extends D \{\overline{C} \overline{f}; K \overline{M}\} m is not defined in \overline{M}}{mbody(m, C) = mbody(m, D)}

Valid method overriding:

\frac{mtype(m, D) = \overline{D}→D_{0}, implies \overline{C} = \overline{D} and C_{0} = D_{0}}{override(\overline{C}→C_{0}, m, D)}

Figure 2: FJ: Auxiliary definitions

Object class? There are various ways to deal with this issue; the simplest one that we have found is to take Object as a distinguished class name whose definition does not appear in the class table. The auxiliary functions that look up fields and method declarations in the class table are equipped with special cases for Object that return the empty sequence of fields and the empty set of methods. (In full Java, the class Object does have several methods. We ignore these in FJ.)

By looking at the class table, we can read off the subtype relation between classes. We write C<:D when C is a subtype of D – i.e., subtyping is the reflexive and transitive closure of the immediate subclass relation given by the extends clauses in CT. Formally, it is defined in the middle of the left column of Figure 1.

The given class table is assumed to satisfy some sanity conditions: (1) CT (C) = class C... for every C ∈ dom(CT ); (2) Object ∉ dom(CT ); (3) for every class name C (except Object) appearing anywhere in CT , we have C ∈ dom(CT ); and (4) there are no cycles in the subtype relation induced by CT – that is, the <: relation is antisymmetric.

For the typing and reduction rules, we need a few auxiliary definitions, given in Figure 2. The fields of a class C, written fields(C), is a sequence \overline{C} \overline{f} pairing the class of a field with its name, for all the fields declared in class C and all of its superclasses. The type of the method m in class C, written mtype(m, C), is a pair, written \overline{B}→B, of a sequence of argument types \overline{B} and a result type B. Similarly, the body of the method m in class C, written mbody(m, C), is a pair, written (\overline{x},e), of a sequence of parameters \overline{x} and an expression e. The predicate override(C_{0}→\overline{C}, m, D) judges if a method m with argument types \overline{C} and a result type C_{0} may be defined in a subclass of D. In case of overriding, if a method with the same name is declared in the superclass then it must have the same type.

2.2 Typing

The typing rules for expressions, method declarations, and class declarations are in the right column of Figure 1. An environment Γ is a finite mapping from variables to types, written \overline{x}:\overline{C}.

The typing judgment for expressions has the form Γ ⊢ e ∈ C, read “in the environment Γ, expression e has type C.” The typing rules are syntax directed, with one rule for each form of expression, save that there are three rules for casts. The typing rules for constructors and method invocations check that each actual parameter has a type that is a subtype of the corresponding formal. We abbreviate typing judgments on sequences in the obvious way, writing Γ ⊢ \overline{e} ∈ \overline{C} as shorthand for Γ ⊢ e_{1} ∈ C_{1}, …, Γ ⊢ e_{n} ∈ C_{n} and writing \overline{C} <: \overline{D} as shorthand for C_{1} <: D_{1}, …, C_{n} <: D_{n}.

One technical innovation in FJ is the introduction of “stupid” casts. There are three rules for type casts: in an upcast the subject is a subclass of the target, in a downcast the target is a subclass of the subject, and in a stupid cast the target is unrelated to the subject. The Java compiler rejects as ill typed an expression containing a stupid cast, but we must allow stupid casts in FJ if we are to formulate type soundness as a subject reduction theorem for a small-step semantics. This is because a sensible expression may be reduced to one containing a stupid cast. For example, consider the following, which uses classes A and B as defined as in the previous section:

    (A)(Object)new B() ⟶ (A)new B()

We indicate the special nature of stupid casts by including the hypothesis stupid warning in the type rule for stupid casts (T-SCast); an FJ typing corresponds to a legal Java typing only if it does not contain this rule. (Stupid casts were omitted from Classic Java [14], causing its published proof of type soundness to be incorrect; this error was discovered independently by ourselves and the Classic Java authors.)

The typing judgment for method declarations has the form M OK IN C, read “method declaration M is ok if it occurs in class C.” It uses the expression typing judgment on the body of the method, where the free variables are the parameters of the method with their declared types, plus the special variable this with type

C.

The typing judgment for class declarations has the form CL OK, read “class declaration CL is ok.” It checks that the constructor applies super to the fields of the superclass and initializes the fields declared in this class, and that each method declaration in the class is ok.

The type of an expression may depend on the type of any methods it invokes, and the type of a method depends on the type of an expression (its body), so it behooves us to check that there is no ill-defined circularity here. Indeed there is none: the circle is broken because the type of each method is explicitly declared. It is possible to load and use the class table before all the classes in it are checked, so long as each class is eventually checked.

2.3 Computation

The reduction relation is of the form e ⟶ e′, read “expression e reduces to expression e′ in one step.” We write ⟶^{∗} for the reflexive and transitive closure of ⟶.

The reduction rules are given in the bottom left column of Figure 1. There are three reduction rules, one for field access, one for method invocation, and one for casting. These were already explained in the introduction to this section. We write [\overline{d}/\overline{x}, e/y]e_{0} for the result of replacing x_{1} by d_{1}, …, x_{n} by d_{n}, and y by e in expression e_{0}.

The reduction rules may be applied at any point in an expression, so we also need the obvious congruence rules (if e ⟶ e′ then e.f ⟶ e′.f, and the like), which we omit here.

2.4 Properties

Formal definitions are fun, but the proof of the pudding is in… well, the proof. If our definitions are sensible, we should be able to prove a type soundness result, which relates typing to computation. Indeed we can prove such a result: if a term is well typed and it reduces to a second term, then the second term is well typed, and furthermore its type is a subtype of the type of the first term.

2.4.1 Theorem [Subject Reduction]: If Γ ⊢ e ∈ C and e ⟶ e′, then Γ ⊢ e′ ∈ C′ for some C′ <:C.

Proof sketch: The main property required in the proof is the following term-substitution lemma:

If Γ, \overline{x} : \overline{E} ⊢ e ∈ D, and Γ ⊢ \overline{d} ∈ \overline{D} where \overline{D}<:\overline{E},
then Γ ⊢ [\overline{d}/\overline{x}]e ∈ C for some C<:D.

This is proved by induction on the derivation of Γ, \overline{x} : \overline{E} ⊢ e ∈ D. An interesting case is when e = (C)e_{0}, where the final rule used in the derivation is T-DCast. Suppose the type of e_{0} is C_{0} and C <: C_{0}. By the induction hypothesis, Γ ⊢ [\overline{d}/\overline{x}]e ∈ D_{0} for some D_{0} <: C_{0}. But, since D_{0} and C may or may not be in the subtype relation, the derivation of Γ ⊢ (C)[\overline{d}/\overline{x}]e ∈ C may involve a stupid warning. On the other hand, if (C)e_{0} is derived using T-UCast, then (C)[\overline{d}/\overline{x}]e will also be an upcast. The theorem itself is now proved by induction on the derivation of e ⟶ e′, with a case analysis on the last rule used. The case for R-Invk is easy, using the lemma above. Other base cases are also straightforward, as are most of the induction steps. The only interesting case is the congruence rule for casting—that is, the case where (C)e ⟶ (C)e′ is derived using e ⟶ e′. Using an argument similar to the term substitution lemma above, we see that a downcast expression may be reduced to a stupid cast and an upcast expression will be always reduced to an upcast. ■

We can also show that if a program is well typed, then the only way it can get stuck is if it reaches a point where it cannot perform a downcast.

2.4.2 Theorem [Progress]: Suppose e is a welltyped expression.

(1) If e includes new C_{0}(\overline{e}).f as a subexpression, then fields(C_{0}) = \overline{T} \overline{f} and f ∈ \overline{f}.

(2) If e includes new C_{0}(\overline{e}).m(\overline{d}) as a subexpression, then mbody(m, C_{0}) = (\overline{x}, e_{0}) and #(\overline{x}) = #(\overline{d}).

To state a similar property for casts, we say that an expression e is safe in Γ if the type derivations of the underlying CT and Γ ⊢ e ∈ C contain no downcasts or stupid casts (uses of rules T-DCast or T-SCast). In other words, a safe program includes only upcasts. Then we see that a safe expression always reduces to another safe expression, and, moreover, typecasts in a safe expression will never fail, as shown in the following pair of theorems.

2.4.3 Theorem: [Reduction preserves safety] If e is safe in Γ and e⟶e′, then e′ is safe in Γ.

2.4.4 Theorem [Progress of safe programs]:

Suppose e is safe in Γ. If e has (C)new C_{0}(\overline{e}) as a subexpression, then C_{0} <:C.

3 Featherweight GJ

Just as GJ adds generic types to Java, Featherweight GJ (or FGJ, for short) adds generic types to FJ. Here is the class definition for pairs in FJ, rewritten with generic type parameters in FGJ.

                                                                class Pair<X extends Object, Y extends Object>
                                                                        extends Object {
                                                                  X fst;
                                                                  Y snd;
                                                                  Pair(X fst, Y snd) {
                                                                    super(); this.fst=fst; this.snd=snd;
                                                                  }
                                                                  <Z extends Object>
                                                                        Pair<Z,Y> setfst(Z newfst) {
                                                                    return new Pair<Z,Y>(newfst, this.snd);
                                                                  }
                                                                }
                                                                class A extends Object {
                                                                  A { super(); }
                                                                }
                                                                class B extends Object {
                                                                  B { super(); }
                                                                }

Both classes and methods may have generic type parameters. Here X and Y are parameters of the class, and Z is a parameter of the setfst method. Each type parameter has a bound; here X, Y, and Z are each bounded

by Object.

In the context of the above definitions, the expression

     new Pair<A,B>(new A(), new B()).setfst<B>(new B())

evaluates to the expression

     new Pair<B,B>(new B(), new B())

If we were being extraordinarily pedantic, we would write A<> and B<> instead of A and B, but we allow the latter as an abbreviation for the former in order that FJ is a proper subset of FGJ.

In GJ, type parameters to generic method invocations are inferred. Thus, in GJ the expression above would be written

     new Pair<A,B>(new A(), new B()).setfst(new B())

with no <B> in the invocation of setfst. So while FJ is a subset of Java, FGJ is not quite a subset of GJ. We regard FGJ as an intermediate language – the form that would result after type parameters have been inferred. While parameter inference is an important aspect of GJ, we chose in FGJ to concentrate on modeling other aspects of GJ.

The bound of a type variable may not be a type variable, but may be a type expression involving type variables, and may be recursive (or even, if there are several bounds, mutually recursive). For example, if C<X> and D<Y> are classes with one parameter each, one may have bounds such as <X extends C<X>> or

even <X extends C<Y>, Y extends D<X>>. For more

on bounds, including examples of the utility of recursive bounds, see the GJ paper [7].

GJ and FGJ are intended to support either of two implementation styles. They may be implemented directly, augmenting the run-time system to carry information about type parameters, or they may be implemented by erasure, removing all information about type parameters at run-time. This section explores the first style, giving a direct semantics for FGJ that maintains type parameters, and proving a type soundness theorem. Section 4 explores the second style, giving an erasure mapping from FGJ into FJ and showing a correspondence between reductions on FGJ expressions and reductions on FJ expressions. The second style corresponds to the current implementation of GJ, which compiles GJ into the Java Virtual Machine (JVM), which of course maintains no information about type parameters at run-time; the first style would correspond to using an augmented JVM that maintains information about type parameters.

3.1 Syntax

In what follows, for the sake of conciseness we abbreviate the keyword extends to the symbol ◁.

The syntax, typing rules, and computation rules for FGJ are given in Figure 3, with a few auxiliary functions in Figure 4. The metavariables X, Y, and Z range over type variables; T, U, and V range over types; and N and O range over nonvariable types (types other than type variables). We write \overline{X} as shorthand for X_{1},…,X_{n} (and similarly for \overline{T}, \overline{N}, etc.), and assume sequences of type variables contain no duplicate names.

The abstract syntax of FGJ is given at the top left of Figure 3. We allow C<> and m<> to be abbreviated as C and m, respectively.

As before, we assume a fixed class table CT , which is a mapping from class names C to class declarations CL, obeying the same sanity conditions as given previously.

3.2 Typing

A type environment Δ is a finite mapping from type variables to nonvariable types, written \overline{X} <: \overline{N}, that takes each type variable to its bound.

Bounds of types

We write bound_{Δ}(T) for the upper bound of T in Δ, as defined in Figure 4. Unlike calculi such as F_{≤} [9], this promotion relation does not need to be defined recursively: the bound of a type variable is always a nonvariable type.

Subtyping

The subtyping relation is defined in the left column of Figure 3. As before, subtyping is the reflexive and transitive closure of the ◁ relation. Type parameters are invariant with regard to subtyping (for reasons explained in the GJ paper), so \overline{T}<:\overline{U} does not imply C<\overline{T}><:C<\overline{U}>.

Well-formed types

If the declaration of a class C begins class C<\overline{X} ◁ \overline{N}>, then a type like C<\overline{T}> is well formed only if substituting \overline{T} for \overline{X} respects the bounds \overline{N}, that is if \overline{T} <: [\overline{T}/\overline{X}]\overline{N}. We write Δ ⊢ T ok if type T is well-formed in context Δ. The rules for well-formed types appear in Figure 3. Note that we perform a simultaneous substitution, so any variable in \overline{X} may appear in \overline{N}, permitting recursion and mutual recursion between variables and bounds.

A type environment Δ is well formed if Δ ⊢ Δ(X) ok for all X in dom(Δ). We also say that an environment Γ is well formed with respect to Δ, written Δ ⊢ Γ ok, if Δ ⊢ Γ(x) ok for all x in dom(Γ).

Field and method lookup

For the typing and reduction rules, we need a few auxiliary definitions, given in Figure 4; these are fairly straightforward adaptations of the lookup rules given previously. The fields of a nonvariable type N, written fields(N), are a sequence of corresponding types and field names, \overline{T} \overline{f}. The type of the method invocation m at nonvariable type N, written mtype(m, N), is a type of the form <\overline{X} ◁ \overline{N}>\overline{U}→U. Similarly, the body of the method invocation m at nonvariable type N with type parameters \overline{V}, written mbody(m<\overline{V}>, N), is a pair, written (\overline{x},e), of a sequence of parameters \overline{x} and an expression e.

Syntax:

CL ::= class C<\overline{X} ◁ \overline{N}> ◁ N \{\overline{T} \overline{f}; K \overline{M}\}
K ::= C(\overline{T} \overline{f}) \{super(\overline{f}); this.\overline{f} = \overline{f};\}
M ::= <\overline{X} ◁ \overline{N}> T m (\overline{T} \overline{x}) \{↑e;\}

e ::= x

     | e.f
     | e.m<\overline{T}>(\overline{e})
     | new N(\overline{e})
     | (N)e

T ::= X

     | N
N ::= C<\overline{T}>

Subtyping:

           Δ ⊢ T<:T

    \frac{Δ ⊢ S<:T  Δ ⊢ T<:U}{Δ ⊢ S<:U}

Δ ⊢ X<: Δ(X)

\frac{CT (C) = class C<\overline{X} ◁ \overline{N}> ◁ N \{...\}}{Δ ⊢ C<\overline{T}><: [\overline{T}/\overline{X}]N}

Well-formed types:

         Δ ⊢ Object ok

\frac{X ∈ dom(Δ)}{Δ ⊢ X ok}

\frac{CT (C) = class C<\overline{X} ◁ \overline{N}> ◁ N \{...\} Δ ⊢ \overline{T} ok  Δ ⊢ \overline{T}<: [\overline{T}/\overline{X}]\overline{N}}{Δ ⊢ C<\overline{T}> ok}

Computation:

      \frac{fields(N) = \overline{T} \overline{f}}{(new N(\overline{e})).f_{i} ⟶ e_{i}}
   \frac{mbody(m<\overline{V}>, N) = (\overline{x}, e_{0})}{(new N(\overline{e})).m<\overline{V}>(\overline{d}) ⟶ [\overline{d}/\overline{x}, new N(\overline{e})/this]e_{0}}

  \frac{∅ ⊢ N<:O}{(O)(new N(\overline{e})) ⟶ new N(\overline{e})}

Expression typing:

Δ; Γ ⊢ x ∈ Γ(x)

\frac{Δ; Γ ⊢ e_{0} ∈ T_{0} fields(bound_{Δ}(T_{0})) = \overline{T} \overline{f}}{Δ; Γ ⊢ e_{0}.f_{i} ∈ T_{i}}

\frac{Δ; Γ ⊢ e_{0} ∈ T_{0} mtype(m, bound_{Δ}(T_{0})) = <\overline{Y} ◁ \overline{O}>\overline{U}→U Δ ⊢ \overline{V} ok  Δ ⊢ \overline{V}<: [\overline{V}/\overline{Y}]\overline{O} Δ; Γ ⊢ \overline{e} ∈ \overline{S}  Δ ⊢ \overline{S}<: [\overline{V}/\overline{Y}]\overline{U}}{Δ; Γ ⊢ e_{0}.m<\overline{V}>(\overline{e}) ∈ [\overline{V}/\overline{Y}]U}

\frac{Δ ⊢ N ok  fields(N) = \overline{T} \overline{f} Δ; Γ ⊢ \overline{e} ∈ \overline{S}  Δ ⊢ \overline{S}<:\overline{T}}{Δ; Γ ⊢ new N(\overline{e}) ∈ N}

\frac{Δ; Γ ⊢ e_{0} ∈ T_{0} Δ ⊢ T_{0} <:N}{Δ; Γ ⊢ (N)e_{0} ∈ N}

\frac{Δ; Γ ⊢ e_{0} ∈ T_{0}  Δ ⊢ N ok Δ ⊢ N<: bound_{Δ}(T_{0})  N ≠ bound_{Δ}(T_{0}) downcast(N, bound_{Δ}(T_{0}))}{Δ; Γ ⊢ (N)e_{0} ∈ N}

\frac{Δ; Γ ⊢ e_{0} ∈ T_{0}  Δ ⊢ N ok Δ ⊢ T_{0} ≮:N  Δ ⊢ N≮:T_{0} stupid warning}{Δ; Γ ⊢ (N)e_{0} ∈ N}

Method typing:

                                                \frac{Δ = \overline{X}<:\overline{N}, \overline{Y}<:\overline{O} Δ ⊢ \overline{T} ok  Δ ⊢ T ok  Δ ⊢ \overline{O} ok Δ; \overline{x} : \overline{T}, this : C<\overline{X}> ⊢ e_{0} ∈ S  Δ ⊢ S<:T CT (C) = class C<\overline{X} ◁ \overline{N}> ◁ N \{...\} override(m, N, <\overline{Z} ◁ \overline{P}>\overline{U}→U)}{<\overline{Y} ◁ \overline{O}> T m (\overline{T} \overline{x}) \{↑e_{0};\} OK IN C<\overline{X} ◁ \overline{N}>}

Class typing:

                                                \frac{\overline{X}<:\overline{N} ⊢ \overline{N} ok  \overline{X}<:\overline{N} ⊢ N ok  \overline{X}<:\overline{N} ⊢ \overline{T} ok fields(N) = \overline{U} \overline{g}    \overline{M} OK IN C<\overline{X} ◁ \overline{N}> K = C(\overline{U} \overline{g}, \overline{T} \overline{f}) \{super(\overline{g}); this.\overline{f} = \overline{f};\}}{class C<\overline{X} ◁ \overline{N}> ◁ N \{\overline{T} \overline{f}; K \overline{M}\} OK}

Figure 3: FGJ: Main definitions Bound of type:

bound_{Δ}(X) = Δ(X)
bound_{Δ}(N) = N.

Field lookup:

fields(Object) = •

\frac{CT (C) = class C<\overline{X} ◁ \overline{N}> ◁ N \{\overline{S} \overline{f}; K \overline{M}\} fields([\overline{T}/\overline{X}]N) = \overline{U} \overline{g}}{fields(C<\overline{T}>) = \overline{U} \overline{g}, [\overline{T}/\overline{X}]\overline{S} \overline{f}}

Method type lookup:

\frac{CT (C) = class C<\overline{X} ◁ \overline{N}> ◁ N \{\overline{S} \overline{f}; K \overline{M}\} <\overline{Y} ◁ \overline{O}> U m (\overline{U} \overline{x}) \{↑e;\} ∈ \overline{M}}{mtype(m, C<\overline{T}>) = [\overline{T}/\overline{X}](<\overline{Y} ◁ \overline{O}>\overline{U}→U)}

\frac{CT (C) = class C<\overline{X} ◁ \overline{N}> ◁ N \{\overline{S} \overline{f}; K \overline{M}\} m is not defined in \overline{M}}{mtype(m, C<\overline{T}>) = mtype(m, [\overline{T}/\overline{X}]N)} Method body lookup:

  \frac{CT (C) = class C<\overline{X} ◁ \overline{N}> ◁ N \{\overline{S} \overline{f}; K \overline{M}\} <\overline{Y} ◁ \overline{O}> U m (\overline{U} \overline{x}) \{↑e_{0};\} ∈ \overline{M}}{mbody(m<\overline{V}>, C<\overline{T}>) = (\overline{x}, [\overline{T}/\overline{X}, \overline{V}/\overline{Y}]e_{0})}

\frac{CT (C) = class C<\overline{X} ◁ \overline{N}> ◁ N \{\overline{S} \overline{f}; K \overline{M}\} m is not defined in \overline{M}}{mbody(m<\overline{V}>, C<\overline{T}>) = mbody(m<\overline{V}>, [\overline{T}/\overline{X}]N)}

Valid method overriding:

\frac{mtype(m, N) = <\overline{Z} ◁ \overline{P}>\overline{U}→U implies \overline{O},\overline{T} = [\overline{Y}/\overline{Z}](\overline{P},\overline{U}) and Δ ⊢ T<: [\overline{Y}/\overline{Z}]U}{override(m, N, <\overline{Z} ◁ \overline{P}>\overline{U}→U)}

Valid downcast:

\frac{Δ ⊢ C<\overline{S}><:T and Δ ⊢ C<\overline{S}> ok for all \overline{S} implies \overline{S} = \overline{T}}{downcast(C<\overline{T}>, T)}

Figure 4: FGJ: Auxiliary definitions

Typing rules

Typing rules for expressions, methods, and classes appear in Figure 3.

The typing judgment for expressions is of form Δ; Γ ⊢ e ∈ T, read as “in the type environment Δ and the environment Γ, e has type T.” Most of the subtleties are in the field and method lookup relations that we have already seen; the typing rules themselves are straightforward.

In the rule GT-DCast, the last premise ensures that the result of the cast will be the same at run time, no matter whether we use the high-level (type-passing) reduction rules defined later in this section or the erasure semantics considered in Section 4. For example, suppose we have defined:

class List<X ◁ Object> ◁ Object { ... }
class LinkedList<X ◁ Object> ◁ List<X> { ... }

Now, if o has type Object, then the cast (List<C>)o is not permitted. (If, at run time, o is bound to new List<D>(), then the cast would fail in the type-passing semantics but succeed in the erasure semantics, since (List<C>)o erases to (List)o while

both new List<C>() and new List<D>() erase to

new List().) On the other hand, if cl has type

List<C>, then the cast (LinkedList<C>)cl is permit-

ted, since the type-passing and erased versions of the cast are guaranteed to either both succeed or both fail.

The typing rule for methods contains one additional subtlety. In FGJ (and GJ), unlike in FJ (and Java), covariant subtyping of method results is allowed. That is, the result type of a method may be a subtype of the result type of the corresponding method in the superclass, although the bounds of type variables and the argument types must be identical (modulo renaming of type variables).

As before, a class table is ok if all its class definitions are ok.

3.3 Reduction

The operational semantics of FGJ programs is only a little more complicated than what we had in FJ. The rules appear in Figure 3.

3.4 Properties

FGJ programs enjoy subject reduction and progress properties exactly like programs in FJ (2.4.1 and 2.4.2). The basic structures of the proofs are similar to those of Theorem 2.4.1 and 2.4.2. For subject reduction, however, since we now have parametric polymorphism combined with subtyping, we need a few more lemmas. The main lemmas required are a term substitution lemma as before, plus similar lemmas about the preservation of subtyping and typing under type substitution. (Readers familiar with proofs of subject reduction for typed lambda-calculi like F_{≤} [9] will notice many similarities). We begin with the three substitution lemmas, which are proved by straightforward induction on a derivation of Δ ⊢ S<:T or Δ; Γ ⊢ e ∈ T.

3.4.1 Lemma: [Type substitution preserves subtyping] If Δ_{1}, \overline{X}<:\overline{N}, Δ_{2} ⊢ S <: T and Δ_{1} ⊢ \overline{U} <: [\overline{U}/\overline{X}]\overline{N} with Δ_{1} ⊢ \overline{U} ok, and none of \overline{X} appearing in Δ_{1}, then Δ_{1}, [\overline{U}/\overline{X}]Δ_{2} ⊢ [\overline{U}/\overline{X}]S<: [\overline{U}/\overline{X}]T.

3.4.2 Lemma: [Type substitution preserves typing] If Δ_{1}, \overline{X}<:\overline{N}, Δ_{2}; Γ ⊢ e ∈ T and Δ_{1} ⊢ \overline{U} <: [\overline{U}/\overline{X}]\overline{N} where Δ_{2} ⊢ \overline{U} ok and none of \overline{X} appears in Δ_{1}, then Δ_{1}, [\overline{U}/\overline{X}]Δ_{2}; [\overline{U}/\overline{X}]Γ ⊢ [\overline{U}/\overline{X}]e ∈ S for some S such that Δ_{1}, [\overline{U}/\overline{X}]Δ_{2} ⊢ S<: [\overline{U}/\overline{X}]T.

3.4.3 Lemma: [Term substitution preserves typing] If Δ; Γ, \overline{x} : \overline{T} ⊢ e ∈ T and, Δ; Γ ⊢ \overline{d} ∈ \overline{S} where Δ ⊢ \overline{S}<:\overline{T}, then Δ; Γ ⊢ [\overline{d}/\overline{x}]e ∈ S for some S such that

Δ ⊢ S<:T.

3.4.4 Theorem [Subject reduction]: If Δ; Γ ⊢ e ∈ T and e ⟶ e′, then Δ; Γ ⊢ e′ ∈ T′, for some T′ such that Δ ⊢ T′ <:T.

Proof sketch: By induction on the derivation of e ⟶ e′ with a case analysis on the reduction rule used. We show in detail just the base case where e is a method invocation. From the premises of the rule GR-Invk, we have

e = new N(\overline{e}).m<\overline{V}>(\overline{d})

mbody(m<\overline{V}>, N) = (\overline{x}, e_{0})

e′ = [\overline{d}/\overline{x}, new N(\overline{e})/this]e_{0}.

By the rule GT-Invk and GT-New, we also have

Δ; Γ ⊢ new N(\overline{e}) ∈ N

mtype(m, bound_{Δ}(N)) = <\overline{Y} ◁ \overline{O}>\overline{U}→U

Δ ⊢ \overline{V}<: [\overline{V}/\overline{Y}]\overline{O}

Δ ⊢ \overline{V} ok Δ; Γ ⊢ \overline{d} ∈ \overline{S}

Δ ⊢ \overline{S}<: [\overline{V}/\overline{Y}]\overline{U}

T = [\overline{V}/\overline{Y}]U.

By examining the derivation of mtype(m, bound_{Δ}(N)), we can find a supertype C<\overline{T}> of N where

\overline{Y}<:\overline{O}; \overline{x} : \overline{U}, this : C<\overline{T}> ⊢ e_{0} ∈ S
\overline{Y}<:\overline{O} ⊢ S<:U

and none of the \overline{Y} appear in \overline{T}. Now, by Lemma 3.4.2,

∅; \overline{x} : [\overline{V}/\overline{Y}]\overline{U}, this : C<\overline{T}> ⊢ e_{0} ∈ [\overline{V}/\overline{Y}]S.

From this, a straightforward weakening lemma (not shown here), plus Lemma 3.4.3 and Lemma 3.4.1, gives

Δ; Γ ⊢ e′ ∈ S′

Δ ⊢ S′ <: [\overline{V}/\overline{Y}]S

Δ ⊢ [\overline{V}/\overline{Y}]S<: [\overline{V}/\overline{Y}]U.

Letting T′ = S′ finishes the case, since Δ ⊢ S′ <: [\overline{V}/\overline{Y}]U by S-Trans. ■

3.4.5 Theorem [Progress]: Suppose e is a welltyped expression.

(1) If e includes new N_{0}(\overline{e}).f as a subexpression, then fields(N_{0}) = \overline{T} \overline{f} and f ∈ \overline{f}.

(2) If e includes new N_{0}(\overline{e}).m<\overline{V}>(\overline{d}) as a subexpression, then mbody(m<\overline{V}>, N_{0}) = (\overline{x}, e_{0}) and #(\overline{x}) = #(\overline{d}).

FGJ is backward compatible with FJ. Intuitively, this means that an implementation of FGJ can be used to typecheck and execute FJ programs without changing their meaning. We can show that a well-typed FJ program is always a well-typed FGJ program and that FJ and FGJ reduction correspond. (Note that it isn’t quite the case that the well-typedness of an FJ program under the FGJ rules implies its well-typedness in FJ, because FGJ allows covariant overriding and FJ does not.) In the statement of the theorem, we use ⟶_{FJ} and ⟶_{FGJ} to show which set of reduction rules is used.

3.4.6 Theorem [Backward compatibility]: If an FJ program (e, CT ) is well typed under the typing rules of FJ, then it is also well-typed under the rules of FGJ. Moreover, for all FJ programs e and e′ (whether well typed or not), e ⟶_{FJ} e′ iff e ⟶_{FGJ} e′.

Proof: The first half is shown by straightforward induction on the derivation of Γ ⊢ e ∈ C (using FJ typing rules), followed by an analysis of the rules GT-Method and GT-Class. In the second half, both directions are shown by induction on a derivation of the reduction relation, with a case analysis on the last rule used. ■

4 Compiling FGJ to FJ

We now explore the second implementation style for GJ and FGJ. The current GJ compiler works by translation into the standard JVM, which maintains no information about type parameters at run-time. We model this compilation in our framework by an erasure translation from FGJ into FJ. We show that this translation maps well-typed FGJ programs into well-typed FJ programs, and that the behavior of a program in FGJ matches (in a suitable sense) the behavior of its erasure under the FJ reduction rules.

A program is erased by replacing types with their erasures, inserting downcasts where required. A type is erased by removing type parameters, and replacing type variables with the erasure of their bounds. For example, the class Pair<X,Y> in the previous section erases to the following:

     class Pair extends Object {
       Object fst;
       Object snd;
       Pair(Object fst, Object snd) {
         super(); this.fst=fst; this.snd=snd;
       }
       Pair setfst(Object newfst) {
         return new Pair(newfst, this.snd);
       }
     }

Similarly, the field selection

     new Pair<A,B>(new A(), new B()).snd

erases to

     (B)new Pair(new A(), new B()).snd

where the added downcast (B) recovers type information of the original program. We call such downcasts inserted by erasure synthetic.

4.1 Erasure of Types

To erase a type, we remove any type parameters and replace type variables with the erasure of their bounds. Write |T|_{Δ} for the erasure of type T with respect to type environment Δ

|T|_{Δ} = C where bound_{Δ}(T) = C<\overline{T}>.

4.2 Field and Method Lookup

In FGJ (and GJ), a subclass may extend an instantiated superclass. This means that, unlike in FJ (and Java), the types of the fields and the methods in the subclass may not be identical to the types in the superclass. In order to specify a type-preserving erasure from FGJ to FJ, it is necessary to define additional auxiliary functions that look up the type of a field or method in the highest superclass in which it is defined.

For example, we previously defined the generic class Pair<X,Y>. We may declare a specialized subclass PairOfA as a subclass of the instantiation Pair<A,A>, which instantiates both X and Y to a given class A.

     class PairOfA extends Pair<A,A> {
       PairOfA(A fst, A snd) {
         super(fst, snd);
       }
       PairOfA setfst(A newfst) {
         return new PairOfA(newfst, this.fst);
       }
     }

Note that, in the setfst method, the argument type A matches the argument type of setfst in Pair<A,A>, while the result type PairOfA is a subtype of the result type in Pair<A,A>; this is permitted by FGJ’s covariant subtyping, as discussed in the previous section. Erasing the class PairOfA yields the following:

     class PairOfA extends Pair {
       PairOfA(Object fst, Object snd) {
         super(fst, snd);
       }
       Pair setfst(Object newfst) {
         return new PairOfA(newfst, this.fst);
       }
     }

Here arguments to the constructor and the method are given type Object, even though the erasure of A is itself; and the result of the method is given type Pair, even though the erasure of PairOfA is itself. In both cases, the types are chosen to correspond to types in Pair, the highest superclass in which the fields and method are defined.

We define variants of the auxiliary functions that find the types of fields and methods in the highest superclass in which they are defined. The maximum field types of a class C, written fieldsmax(C), is the sequence of pairs of a type and a field name defined as follows:

fieldsmax(Object) = •

\frac{CT (C) = class C<\overline{X} ◁ \overline{N}> ◁ D<\overline{U}> \{\overline{T} \overline{f}; ...  \} Δ = \overline{X}<:\overline{N}    \overline{C} \overline{g} = fieldsmax(D)}{fieldsmax(C) = \overline{C} \overline{g}, |\overline{T}|_{Δ} \overline{f}}

The maximum method type of m in C, written mtypemax(m, C), is defined as follows:

\frac{CT (C) = class C<\overline{X} ◁ \overline{N}> ◁ D<\overline{U}> \{...\} <\overline{Y} ◁ \overline{O}>\overline{T}→T = mtype(m, D<\overline{U}>)}{mtypemax(m, C) = mtypemax(m, D)}

\frac{CT (C) = class C<\overline{X} ◁ \overline{N}> ◁ D<\overline{U}> \{...\} mtype(m, D<\overline{U}>) undefined <\overline{Y} ◁ \overline{O}>\overline{T}→T = mtype(m, C<\overline{X}>) Δ = \overline{X}<:\overline{N}, \overline{Y}<:\overline{O}}{mtypemax(m, C) = |\overline{T}|_{Δ}→|T|_{Δ}}

We also need a way to look up the maximum type of a given field. If fieldsmax(C) = \overline{D} \overline{f} then we set fieldsmax(C)(f_{i}) = D_{i}.

4.3 Erasure of Expressions

The erasure of an expression depends on the typing of that expression, since the types are used to determine which downcasts to insert. The erasure rules are optimized to omit casts when it is trivially safe to do so; this happens when the maximum type is equal to the erased type.

Write |e|_{Δ,Γ} for the erasure of a well-typed expression e with respect to environment Γ and type environment Δ:

|x|_{Δ,Γ} = x

\frac{Δ; Γ ⊢ e_{0}.f ∈ T Δ; Γ ⊢ e_{0} ∈ T_{0} fieldsmax(|T_{0}|_{Δ})(f) = |T|_{Δ}}{|e_{0}.f|_{Δ,Γ} = |e_{0}|_{Δ,Γ}.f}

\frac{Δ; Γ ⊢ e_{0}.f ∈ T Δ; Γ ⊢ e_{0} ∈ T_{0} fieldsmax(|T_{0}|_{Δ})(f) ≠ |T|_{Δ}}{|e_{0}.f|_{Δ,Γ} = (|T|_{Δ}) |e_{0}|_{Δ,Γ}.f}

\frac{Δ; Γ ⊢ e_{0}.m<\overline{V}>(\overline{e}) ∈ T Δ; Γ ⊢ e_{0} ∈ T_{0} mtypemax(m, |T_{0}|_{Δ}) = \overline{C}→D D = |T|_{Δ}}{|e_{0}.m<\overline{V}>(\overline{e})|_{Δ,Γ} = |e_{0}|_{Δ,Γ}.m(|\overline{e}|_{Δ,Γ})}

\frac{Δ; Γ ⊢ e_{0}.m<\overline{V}>(\overline{e}) ∈ T Δ; Γ ⊢ e_{0} ∈ T_{0} mtypemax(m, |T_{0}|_{Δ}) = \overline{C}→D D ≠ |T|_{Δ}}{|e_{0}.m<\overline{V}>(\overline{e})|_{Δ,Γ} = (|T|_{Δ}) |e_{0}|_{Δ,Γ}.m(|\overline{e}|_{Δ,Γ})}

                                                         |new N(\overline{e})|_{Δ,Γ} = new |N|_{Δ}(|\overline{e}|_{Δ,Γ})

|(N)e_{0}|_{Δ,Γ} = (|N|_{Δ}) |e_{0}|_{Δ,Γ}

(Strictly speaking, one should think of the erasure operation as acting on typing derivations rather than expressions. Since well-typed expressions are in 1-1 correspondence with their typing derivations, the abuse of notation creates no confusion.)

4.4 Erasure of Methods and Classes

The erasure of a method m with respect to type environment Δ in class C, written |M|_{Δ,C}, is defined as follows:

\frac{Γ = \overline{x}:\overline{T} Δ′ = Δ, \overline{Y}<:\overline{O} e′ = [(|\overline{T}|_{Δ′})\overline{x}′/\overline{x}]|e|_{Δ′,Γ} mtypemax(m, C) = \overline{D}→D}{|<\overline{Y} ◁ \overline{O}> T m (\overline{T} \overline{x}) \{↑e;\}|_{Δ,C} = D m (\overline{D} \overline{x}′) \{↑e′;\}}

(In GJ, the actual erasure is somewhat more complex, involving the introduction of bridge methods, so that one ends up with two overloaded methods: one with the maximum type, and one with the instantiated type. We don’t model that extra complexity here, because it depends on overloading of method names, which is not modeled in FJ.)

The erasure of constructors and classes is:

    |C(\overline{U} \overline{g}, \overline{T} \overline{f}) \{super(\overline{g}); this.\overline{f} = \overline{f};\}|_{Δ,C}
  = C(fieldsmax(C)) \{super(\overline{g}); this.\overline{f} = \overline{f};\}

   \frac{Δ = \overline{X}<:\overline{N}}{|class C<\overline{X} ◁ \overline{N}> ◁ N \{\overline{T} \overline{f}; K \overline{M}\}| = class C ◁ |N|_{Δ}\{|\overline{T}|_{Δ} \overline{f}; |K|_{Δ} |\overline{M}|_{Δ,C}\}}

4.5 Properties of Erasure

Having defined erasure, we may investigate some of its properties. First, a well-typed FGJ program erases to a well-typed FJ program, as expected:

4.5.1 Theorem [Erasure preserves typing]: If an FGJ class table CT is ok and Δ; Γ ⊢ e ∈ T, then |Γ|_{Δ} ⊢ |e|_{Δ,Γ} ∈ |T|_{Δ} and |CT | is ok using FJ rules.

Proof sketch: By induction on the derivation of Δ; Γ ⊢_{FGJ} e ∈ T, using the following lemmas: (1) if Δ ⊢ N ok then |fields_{FGJ}(N)|_{Δ} <: fieldsmax(|N|_{Δ}); (2) if Δ ⊢ N ok and methodtype_{FGJ}(m, N) = <\overline{Y} ◁ \overline{O}>\overline{U}→U, then mtypemax(m, |N|_{Δ}) = \overline{C}→D and |[\overline{V}/\overline{Y}]\overline{U}|_{Δ} <: \overline{C} and |[\overline{V}/\overline{Y}]U|_{Δ} <:D; and (3) if Δ ⊢ Γ ok and Δ; Γ ⊢ e ∈ T for some well-formed type environment Δ, then Δ ⊢ T ok. ■

More interestingly, we would intuitively expect that erasure from FGJ to FJ should also preserve the reduction behavior of FGJ programs:

[figure: e; reduce (FGJ); erase; e′; erase; |e|; reduce (FJ); |e′|]

Unfortunately, this is not quite true. For example, consider the FGJ expression

    e = new Pair<A,B>(a,b).fst,

where a and b are expressions of type A and B, respectively, and its erasure:

    |e|_{Δ,Γ} = (A)new Pair(|a|_{Δ,Γ},|b|_{Δ,Γ}).fst

In FGJ, e reduces to |a|_{Δ,Γ}, while the erasure |e|_{Δ,Γ} reduces to (A)|a|_{Δ,Γ} in FJ; it does not reduce to |a|_{Δ,Γ} when a is not a new expression. (Note that it is not an artifact of our nondeterministic reduction strategy: it happens even if we adopt a call-by-value reduction strategy, since, after method invocation, we may obtain an expression like (A)e where e is not a new expression.) Thus, the above diagram does not commute even if one-step reduction (⟶) at the bottom is replaced with many-step reduction (⟶^{∗}). In general, synthetic casts can persist for a while in the FJ expression, although we expect those casts will eventually turn out to be upcasts when a reduces to a new expression.

In the example above, an FJ expression d reduced from |e|_{Δ,Γ} had more synthetic casts than |e′|_{Δ,Γ}. However, this is not always the case: d may have less casts than |e′|_{Δ,Γ} when the reduction step involves method invocation. Consider the following class and its erasure:

                                                                class C<X extends Object> extends Object {
                                                                  X f;
                                                                  C(X f) { this.f = f; }
                                                                  C<X> m() { return new C<X>(this.f); }
                                                                }
                                                                class C extends Object {
                                                                  Object f;
                                                                  C(Object f) { this.f = f; }
                                                                  C m() { return new C(this.f); }
                                                                }

Now consider the FGJ expression

                                                        e = new C<A>(new A()).m()

and its erasure

                                                        |e|_{Δ,Γ} = new C(new A()).m().

In FGJ,

                                                        e ⟶_{FGJ} new C<A>(new C<A>(new A()).f).

In FJ, on the other hand, |e|_{Δ,Γ} reduces to new C(new C(new A()).f), which has fewer synthetic

                                                    casts than new C((A)new C(new A()).f), which is the

erasure of the reduced expression in FGJ. The subtlety we observe here is that, when the erased term is reduced, synthetic casts may become “coarser” than the casts inserted when the reduced term is erased, or may be removed entirely as in this example. (Removal of downcasts can be considered as a combination of two operations: replacement of (A) with the coarser cast (Object) and removal of the upcast (Object), which does not affect the result of computation.)

To formalize both of these observations, we define an auxiliary relation that relates FJ expressions differing only by the addition and replacement of some synthetic casts. Let us call a well-typed expression d an expansion of a well-typed expression e, written e ⟹ d, if d is obtained from e by some combination of (1) addition of zero or more synthetic upcasts, (2) replacement of some synthetic casts (D) with (C), where C is a supertype of D, or (3) removal of some synthetic casts.

4.5.2 Theorem: [Erasure preserves reduction modulo expansion] If Δ; Γ ⊢ e ∈ T and e ⟶_{FGJ}^{∗} e′, then there exists some FJ expression d′ such that |e′|_{Δ,Γ} ⟹ d′ and |e|_{Δ,Γ} ⟶_{FJ} d′. In other words, the following diagram commutes.

[figure: e; reduce (FGJ); ∗; erase; e′; erase; |e′|; |e|; reduce (FJ); ∗; d′]

As easy corollaries of this theorem, it can be shown that, if an FGJ expression e reduces to a “fully-evaluated expression,” then the erasure of e reduces to exactly its erasure, and that if FGJ reduction gets stuck at a stupid cast, then FJ reduction also gets stuck because of the same typecast. We use the metavariable v for fully evaluated expressions, defined as follows:

    v ::= new N(\overline{v}).

4.5.3 Corollary: [Erasure preserves execution results] If Δ; Γ ⊢ e ∈ T and e ⟶_{FGJ}^{∗} v, then |e|_{Δ,Γ} ⟶_{FJ}^{∗} |v|_{Δ,Γ}.

4.5.4 Corollary: [Erasure preserves typecast errors] If Δ; Γ ⊢ e ∈ T and e ⟶_{FGJ}^{∗} e′, where e′ has a stuck subexpression (C<\overline{S}>)new D<\overline{T}>(\overline{e}), then |e|_{Δ,Γ} ⟶_{FJ}^{∗} d′ such that d′ has a stuck subexpression (C)new D(\overline{d}), where \overline{d} are expansions of the erasures of \overline{e}, in the same position (modulo synthetic casts) as the erasure of e′.

5 Related Work

Core calculi for Java. There are several known proofs in the literature of type soundness for subsets of Java. In the earliest, Drossopoulou and Eisenbach [11] (using a technique later mechanically checked by Syme [20]) prove soundness for a fairly large subset of sequential Java. Like us, they use a small-step operational semantics, but they avoid the subtleties of “stupid casts” by omitting casting entirely. Nipkow and Oheimb [17] give a mechanically checked proof of soundness for a somewhat larger core language. Their language does include casts, but it is formulated using a “bigstep” operational semantics, which sidesteps the stupid cast problem. Flatt, Krishnamurthi, and Felleisen [14] use a small-step semantics and formalize a language with both assignment and casting. Their system is somewhat larger than ours (the syntax, typing, and operational semantics rules take perhaps three times the space), and the soundness proof, though correspondingly longer, is of similar complexity. Their published proof of subject reduction is slightly flawed – the case that motivated our introduction of stupid casts is not handled properly – but the problem can be repaired by applying the same refinement we have used here.

Of these three studies, that of Flatt, Krishnamurthi, and Felleisen is closest to ours in an important sense: the goal there, as here, is to choose a core calculus that is as small as possible, capturing just the features of Java that are relevant to some particular task. In their case, the task is analyzing an extension of Java with Common Lisp style mixins – in ours, extensions of the core type system. The goal of the other two systems, on the other hand, is to include as large a subset of Java as possible, since their primary interest is proving the soundness of Java itself.

Other class-based object calculi. The literature on foundations of object-oriented languages contains many papers formalizing class-based object-oriented languages, either taking classes as primitive (e.g., [21, 8, 6, 5]) or translating classes into lower-level mechanisms (e.g., [13, 4, 1, 19]. Some of these systems (e.g. [19, 8]) include generic classes and methods, but only in fairly simple forms.

Generic extensions of Java. A number of extensions of Java with generic classes and methods have been proposed by various groups, including the language of Agesen, Freund, and Mitchell [2]; PolyJ, by Myers, Bank, and Liskov [16]; Pizza, by Odersky and Wadler [18]; GJ, by Bracha, Oderksy, Stoutamire, and Wadler [7]; and NextGen, by Cartwright and Steele [10]. While all these languages are believed to be typesafe, our study of FGJ is the first to give rigorous proof of soundness for a generic extension of Java. We have used GJ as the basis for our generic extension, but similar techniques should apply to the forms of genericity found in the rest of these languages.

6 Discussion

We have presented Featherweight Java, a core language for Java modeled closely on the lambda-calculus and embodying many of the key features of Java’s type system. FJ’s definition and proof of soundness are both concise and straightforward, making it a suitable arena for the study of ambitious extensions to the type system, such as the generic types of GJ. We have developed this extension in detail, stated some of its fundamental properties, and sketched their proofs.

FJ itself is not quite complete enough to model some of the interesting subtleties found in GJ. In particular, the full GJ language allows some parameters to be instantiated by a special “bottom type” *, using a slightly delicate rule to avoid unsoundness in the presence of assignment. Capturing the relevant issues in FGJ requires extending it with assignment and null values (both of these extensions seem straightforward, but cost us some of the pleasing compactness of FJ as it stands). The other somewhat subtle aspect of GJ that is not accurately modeled in FGJ is the use of bridge methods in the compilation from GJ to JVM bytecodes. To treat this compilation exactly as GJ does, we would need to extend FJ with overloading.

Our formalization of GJ also does not include raw types, a unique aspect of the GJ design that supports compatibility between old, unparameterized code and new, parameterized code. We are currently experimenting with an extension of FGJ with raw types.

Formalizing generics has proven to be a useful application domain for FJ, but there are other areas where its extreme simplicity may yield significant leverage. For example, work is under way on formalizing Java 1.1’s inner classes using FJ [15].

Acknowledgments

This work was supported by the University of Pennsylvania and the National Science Foundation under grant CCR-9701826, Principled Foundations for Programming with Objects. Igarashi is a research fellow of the Japan Society for the Promotion of Science.

References

[1] Martín Abadi and Luca Cardelli. A Theory of Objects. Springer-Verlag, 1996.

[2] Ole Agesen, Stephen N. Freund, and John C. Mitchell. Adding type parameterization to the Java language. In Object Oriented Programing: Systems, Languages, and Applications (OOPSLA), October 1997.

[3] H. P. Barendregt. The Lambda Calculus. North Holland, revised edition, 1984.

[4] Viviana Bono and Kathleen Fisher. An imperative first-order calculus with object extension. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP), 1998.

[5] Viviana Bono, Amit J. Patel, and Vitaly Shmatikov. A core calculus of classes and mixins. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP), volume 1628 of Lecture Notes in Computer Science, pages 43–66. Springer-Verlag, June 1999.

[6] Viviana Bono, Amit J. Patel, Vitaly Shmatikov, and John C. Mitchell. A core calculus of classes and objects. In Fifteenth Confertence on the Mathematical Foundations of Programming Semantics, April 1999.

[7] Gilad Bracha, Martin Odersky, David Stoutamire, and Philip Wadler. Making the future safe for the past: Adding genericity to the Java programming language. In Craig Chambers, editor, Object Oriented Programing: Systems, Languages, and Applications (OOPSLA), ACM SIGPLAN Notices volume 33 number 10, pages 183–200, Vancouver, BC, October 1998.

[8] Kim B. Bruce. A paradigmatic object-oriented programming language: Design, static typing and semantics. Journal of Functional Programming, 4(2), April 1994. Preliminary version in POPL 1993, under the title “Safe type checking in a statically typed object-oriented programming language”.

[9] Luca Cardelli, Simone Martini, John C. Mitchell, and Andre Scedrov. An extension of system F with subtyping. Information and Computation, 109(1– 2):4–56, 1994. Preliminary version in TACS ’91 (Sendai, Japan, pp. 750–770).

[10] Robert Cartwright and Guy L. Steele Jr. Compatible genericity with run-time types for the Java programming language. In Craig Chambers, editor, Object Oriented Programing: Systems, Languages, and Applications (OOPSLA), SIGPLAN Notices 33(10), pages 201–215, Vancouver, BC, Octover 1998. ACM.

[11] S. Drossopoulou, S. Eisenbach, and S. Khurshid. Is the Java Type System Sound? Theory and Practice of Object Systems, 7(1):3–24, 1999. Preliminary version in ECOOP ’97.

[12] Matthias Felleisen and Daniel P. Friedman. A little Java, A few Patterns. The MIT Press, Cambridge, Massachusetts, 1998.

[13] Kathleen Fisher and John C. Mitchell. On the relationship between classes, objects, and data abstraction. Theory and Practice of Object Systems, 4(1):3–25, 1998.

[14] Matthew Flatt, Shriram Krishnamurthi, and Matthias Felleisen. Classes and mixins. In ACM Symposium on Principles of Programming Languages (POPL), San Diego, January 1998. ACM.

[15] Atsushi Igarashi and Benjamin C. Pierce. On inner classes, July 1999. Submitted for publication.

[16] Andrew C. Myers, Joseph A. Bank, and Barbara Liskov. Parameterized types for Java. In ACM Symposium on Principles of Programming Languages (POPL), January 1997.

[17] Tobias Nipkow and David von Oheimb. Java_{light} is type-safe — definitely. In ACM Symposium on Principles of Programming Languages (POPL), pages 161–170, San Diego, January 1998. ACM.

[18] Martin Odersky and Philip Wadler. Pizza into Java: Translating theory into practice. In ACM Symposium on Principles of Programming Languages (POPL), 1997.

[19] Benjamin C. Pierce and David N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207–247, April 1994. Preliminary version in Principles of Programming Languages (POPL), 1993.

[20] Don Syme. Proving Java type soundness. Technical Report 427, Computer Laboratory, University of Cambridge, June 1997.

[21] Mitchell Wand. Type inference for objects with instance variables and inheritance. Technical Report NU-CCS-89-2, College of Computer Science, Northeastern University, February 1989. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design (MIT Press, 1994).