A Variation on Java Wildcards - Trading Expressiveness for Global Type Inference

Stadelmeier, Andreas; Plümicke, Martin; Thiemann, Peter

doi:10.4230/LIPIcs.ECOOP.2026.26

A Variation on Java Wildcards – Trading Expressiveness for Global Type Inference

Andreas Stadelmeier

DHBW Stuttgart, Campus Horb, Germany Martin Plümicke

DHBW Stuttgart, Campus Horb, Germany Peter Thiemann

Institut für Informatik, Universität Freiburg, Germany

Abstract

In standard Java, wildcards behave like existential types: they must be opened before use in a method invocation, a process the compiler performs implicitly via capture conversion. We present Java-TX, a dialect of Java that sidesteps this existential encoding and treats wildcards as placeholders for unknown types, used directly without prior opening. This choice simplifies the type system and makes it compatible with an existing global type inference algorithm. The trade-off is that some method calls valid in standard Java become unavailable in Java-TX. In effect, we trade some of Java’s wildcard expressiveness for global type inference.

We explore the metatheory of Java-TX through Featherweight Java-TX (FJ-TX), a functional core calculus for Java-TX that extends Featherweight Generic Java with our wildcard interpretation. We prove type soundness for FJ-TX. Finally, we evaluate the practical impact of omitting capture conversion by conducting a study on open-source Java projects by calculating an underapproximation of how much existing Java code is compatible with the Java-TX type system.

Keywords and phrases:

type inference, Java, subtyping, wildcards, capture conversion

Copyright and License:

2012 ACM Subject Classification:

Software and its engineering

\rightarrow

Syntax

DOI:

10.4230/LIPIcs.ECOOP.2026.26

Event:

40th European Conference on Object-Oriented Programming (ECOOP 2026)

Editors:

Robbert Krebbers and Alexandra Silva

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Global type inference is a natural goal for Java because explicit type annotations impose a real maintenance burden. Although Java has steadily moved toward inference¹¹1the diamond operator, the var keyword, and lambda type inference all reduce boilerplate, method and field types must still be annotated by hand, making certain refactorings unnecessarily painful (see Section 2.4 for concrete examples and evidence). A global type inference (GTI) algorithm that infers all type annotations would eliminate most of this overhead.

But global type inference for Java-style generics faces a fundamental obstacle with wildcard types. In Java, wildcard types such as Box<?> are treated as bounded existential types that must be opened before they can be used in a method call. This opening (capture conversion) replaces each wildcard with a fresh type variable and is performed eagerly at every method invocation. Attempts to extend constraint-based global type inference to support capture conversion have not succeeded: during constraint generation the types of subexpressions are not yet known, making it unclear whether and how capture conversion should be applied at a given call site (see Section 2.3).

Plümicke’s global type inference algorithm [13] resolves this impasse by adopting a different wildcard semantics: wildcards are treated as ordinary types that can serve directly as type arguments in method invocations, without any prior opening. The resulting language, Java-TX (Java Type eXtended), is a dialect of Java with global type inference that treats wildcards as ordinary types rather than existentials, foregoing capture conversion entirely. This design is not proposed as a superior alternative to Java’s wildcard treatment, but is rather a consequence of enabling global type inference: the wildcard semantics of Java-TX naturally arise from the limits of this global type inference algorithm.

The key technical difference concerns reflexivity. Wildcards denote unknown types, so subtyping is not reflexive on them. If wildcards are to be used directly as type arguments, the corresponding method type parameters must therefore also be treated as non-reflexive. Consequently, Java-TX does not assume reflexivity on method type parameters by default, and wildcards can be substituted for such parameters without capture conversion. However, if the method body requires the judgment ${\tt X}\mathbin{\texttt{<:}}{\tt X}$ , the parameter must be declared with an explicit reflexivity constraint ${\tt X}\ {\tt extends}\ {\tt X}$ , which wildcards cannot satisfy, ruling them out as type arguments at that position. Java-TX and Java are incomparable: each accepts some programs the other rejects (see Section 2 for a detailed comparison).

Up to now, Java-TX was defined only by its inference algorithm, with no semantic foundation for the language. In a technical report, Plümicke [15] made a first attempt at defining such a calculus, but without a soundness proof. The present paper completes this effort by establishing type soundness for FJ-TX, and assesses the practical impact of the different treatment of wildcards on real-world Java code.

1.1 Contributions of this work

$\blacksquare$

In depth comparison of the treatment of wildcards in Java and Java-TX.
$\blacksquare$

Definition of the core calculus Featherweight Java-TX (FJ-TX).
$\blacksquare$

Proof of type soundness for FJ-TX using the standard preservation/progress structure.
$\blacksquare$

An evaluation of the practical impact of the different treatment of wildcards.

1.2 Overview

Section 2 introduces the different approaches to wildcards taken by Java and Java-TX along with a detailed comparison based on practical examples. We conclude this section with a brief summary of further features of Java-TX in Section 2.4.

Section 3 defines the calculus Featherweight Java-TX (FJ-TX) by extending and adapting syntax, typing, and operational semantics of Featherweight Generic Java [7].

Section 4 contains the type soundness proof for FJ-TX.

Section 5 evaluates the differences between Java and Java-TX qualitatively on real world examples: the source code of the JDK and a selection of seven popular Java projects.

We close with related work (Section 6) and a brief outlook (Section 7).

2 Java vs. Java-TX

The sound interaction of subtyping and generics in an imperative programming language can be very simple. For instance, the initial proposals for generic Java, as well as the first Java version implementing generics, required generic types to be invariant. To illustrate the concept, we consider the class Box in Fig. 1(a). Invariance means that ${\tt{\tt Box}}\textrm{{<}}{\tt A}\textrm{{>}}$ is a subtype of ${\tt{\tt Box}}\textrm{{<}}{\tt B}\textrm{{>}}$ if and only if ${\tt A}={\tt B}$ . In Fig. 1(b) the assignment obox = ibox violates invariance. Java rejects it to prevent a value of type Object to be stored in a box of Integer.

⬇

class Box<T> {

T elem;

T get() { return elem; }

void set(T x) { elem = x; }

}

(a) Definition.

⬇

Box<Integer> ibox = new Box<>(42);

Box<Object> obox = ibox; // illegal

// because set() would put an Object

// into a Box of Integers:

obox.set(new Object());

(b) Erroneous Java program.

Figure 1: The class Box.

Subsequently, the design of Java’s collection classes showed that invariance is overly restrictive. If a method only reads from a generic type, then covariant subtyping is sound. If a method only writes to a generic type, then contravariant subtyping is sound. Only if a method both reads and writes from a generic type, invariant subtyping must be used. In consequence, Java introduced wildcard types to enable use-site variance for generic types. Use-site variance in programming allows us to specify variance (how subtypes relate) for a generic type where it is used, not where it is declared. Thus, the variance of a generic type can be different at each use (e.g., in Java and Kotlin). In contrast, with definition-site variance the definition of a generic type specifies its variance once and for all (e.g., in Eiffel, C#, OCaml). See Altidor et al. [1] for a in-depth treatment of both concepts.

Since version 5, Java [6] and the existing core calculi for wildcards [19, 18, 4, 3] employ bounded existential types and capture conversion to handle wildcard types.

2.1 Capture Conversion - The Java Approach

⬇

<T>void fg (Box<T> b1, Box<T> b2) {

b1.set(b2.get());

}

Box<?> b1 = new Box<Integer>(42);

Box<?> b2 = new Box<String>("foo");

fg (

b1,

b2); // Java type error here

Listing 1: Rejected Java program involving capture conversion

Wildcards enable variant subtyping in Java as in ${\tt Box}\textrm{{<}}{\tt String}\textrm{{>}}\mathbin{\texttt{<:}}{}$ Box<? extends Object>, where $\mathbin{\texttt{<:}}{}$ stands for the subtyping relation (cf. Figure 6) and the wildcard ? “forgets” the String type and only remembers that it is a subtype of Object. However, wildcards cannot be treated like regular types. In Listing 1 the method fg cannot be called with two arguments of type Box<?>. At first glance it seems like the method parameter T could be replaced with a wildcard resulting in a method type (Box<?>, Box<?>) $\to$ void. But Java rejects this idea as it would lead to unsoundness: In this example the contents of ${\tt Box}\textrm{{<}}{\tt String}\textrm{{>}}$ would end up in ${\tt Box}\textrm{{<}}{\tt Integer}\textrm{{>}}$ .

What Java actually does for every method call involving wildcards is to replace every wildcard type with a fresh capture variable. This process is called capture conversion [18, 4, 3] and is hidden from the programmer. In Listing 1, the first argument has the type Box<?>, which is transformed to ${\tt Box}\textrm{{<}}\texttt{CAP\#1}\textrm{{>}}$ . Argument gets the type ${\tt Box}\textrm{{<}}\texttt{CAP\#2}\textrm{{>}}$ . Now the method call is subject to a regular type check treating CAP#1 and CAP#2 as normal types. The method call is rejected, because there is no substitution for T in the method type ${\tt}\textrm{{<}}{\tt T}\textrm{{>}}$ (Box<T>, Box<T>) $\to$ void to fit the argument types $({\tt Box}\textrm{{<}}\texttt{CAP\#1}\textrm{{>}},{\tt Box}\textrm{{<}}\texttt% {CAP\#2}\textrm{{>}})$ .

Capture conversion does not require any participation of the programmer and enables many method calls involving wildcards.

2.2 Method-Site Variance - The Java-TX Approach

Java-TXis a dialect of Java with global type inference [12], which includes support for wildcards. This system has been developed and used for a number of years (see Section 2.4). It does not rely on an encoding of wildcards as existentials, but rather supports a notion of wildcard types (different from Java) directly. It basically supports declaration-site variance for method parameters combined with wildcards treated like regular types. In particular, there is no capture conversion and one can substitute wildcards for certain Java-TX type parameters. Whether a type parameter is eligible for instantiation by a wildcard depends on how the corresponding argument is used inside the method body.

The key to this approach is to assume that subtyping is not reflexive on type variables in general. If the reflexivity is required on a type variable ${\tt X}$ , it must be declared explicitly by the constraint ” ${\tt X}\textrm{$\,\mathbin{\texttt{<:}}\,$}{\tt X}$ ”. This constraint forbids the instantiation of ${\tt X}$ with a wildcard.

Note: The Java-TX approach works best in combination with global type inference. The constraints generated during inference indicate whether a method type parameter requires the reflexivity constraint. For readability, all the Java-TX examples shown in this chapter are fully annotated with their inferred types.

Listing 2 shows an example where the method type parameter X can be instantiated with a wildcard type, because X does not have to be reflexive inside the assign method. Therefore the call at is valid. It is possible to instantiate X with a wildcard resulting in the method type instance (Box<?>, Box<?>) $\to$ void.

⬇

<X> void assign(Box<X> b1, Box<X> b2) {

b1 = b2;

}

Box<?> b1 = ...

Box<?> b2 = ...

assign(b1, b2);

Listing 2: Non-reflexive method type parameters

On the other hand, Java rejects the call to assign, because Java applies capture conversion separately to the method parameters b1 and b2. As their capture types are different, there is no instantiation for X to accept the call.

The Java-TX approach comes with some restrictions, too. The next example is a legal Java program fragment which is accepted via capture conversion, but rejected by Java-TX.

⬇

<T> void m(Box<T> b) {

b.set(b.get());

}

Box<?> bb = ...;

m(bb);

⬇

// Java-TX

<T extends T> void repack(Box<T> b) {

b.set(b.get());

}

Box<?> b = ...;

repack(b); // Illegal in Java-TX

Listing 3: Reflexive type parameter Note: Java-TX source code highlighted in yellow

Java uses capture conversion in the call to m. The wildcard in Box<?> is replaced by a fresh capture type CAP#1. In contrast, Java-TX does not accept this method definition. The return type of get() is ${\tt T}$ and set() expects an argument of type ${\tt T}$ . For b.set(b.get()) to be accepted the type variable ${\tt T}$ must be reflexive ( ${\tt T}\mathbin{\texttt{<:}}{}{\tt T}$ ). Thus, the method m requires a reflexive constraint ${\tt T}\ {\tt extends}\ {\tt T}$ as shown in Listing 3. In Java-TX this method cannot be called with a type ${\tt Box}\textrm{{<}}{\tt?}\textrm{{>}}$ like in line because subtyping is not reflexive on wildcards.

The next example we discuss is a variation of a method shown in Listing 1.

⬇

<W, R extends W>

void overwrite(Box<W> x, Box<R> y){

x.set(y.get());

}

This program is accepted by both Java and by Java-TX and type inference infers the same typing. Let’s try to use it with wildcard types.

⬇

Box<? extends Object> b1 = new Box<Integer>(42);

Box<? extends Object> b2 = new Box<String>("foo");

overwrite(b1, b2);

Java rejects this program. In the call to overwrite, the wildcards in the types of b1 and b2 get instantiated to different capture variables, say CAP#1 and CAP#2, which are not in a subtype relation. Hence, the constraint ${\tt R}\textrm{$\,\mathbin{\texttt{<:}}\,$}{\tt W}$ is not satisfied and the method call is rejected.

Type inference in Java-TX obtains the instantiation

[\textrm{?\,extends}\linebreak[0]\,\mathtt{Object}/\mathtt{W},\ \textrm{?\,% extends}\linebreak[0]\,\mathtt{Object}/\mathtt{R}]

for the method call and has to check

\mathtt{\textrm{?\,extends}\linebreak[0]\,Object\ \textrm{$\,\mathbin{\texttt{% <:}}\,$}\ \textrm{?\,extends}\linebreak[0]\,Object}

which leads to a type error as subtyping is not reflexive on wildcard types.

So the method definition is accepted in both languages and the call is rejected in both languages.

We conclude with a somewhat contrived example that is accepted by both, Java and Java-TX, but cannot be expressed in the core calculi based on existential types (e.g., [3]).

⬇

<X,Y> void equalize(Pair<X,Y> a, Pair<X,Y> b) {}

<Y> Pair<?, Y> left() { return null; }

<X> Pair<X, ?> right() { return null; }

equalize(left(), right());

The difficulty in typing the method call to equalize with capture conversion is that the capture variable introduced for left instantiates the generic variable of right and vice versa. This mutual instantiation pattern cannot be expressed in (e.g.) Bierhoff’s calculus [3], but recent Java compilers support it.

The example presents no difficulty for Java-TX: both X and Y can be instantiated to a wildcard because equalize() does not require a reflexivity constraint.

2.3 Capture Conversion and Global Type Inference

Capture conversion turns out to be incompatible with global type inference, where the goal is to reconstruct missing type annotations in partially untyped Java programs. Recent work [17] has shown that type inference works well for Java with generics, but without wildcards. When trying to extend type inference to Java-style wildcards, we find that capture conversion is not compatible with constraint-based global type inference, as it is based on first generating type constraints and solving them afterwards. However, during constraint generation it is impossible to determine if a capture conversion is required because the argument types to a method call are not yet known.

In the following example untypedMethod, the types of b1 and b2 only emerge during the constraint solving process. (See Listing 2 for the definition of assign.)

⬇

untypedMethod(b1, b2){

return assign(b1, b2);

}

Constraints

\implies

	$\displaystyle\textit{b1}\mathbin{\texttt{<:}}{}{\tt Box}\textrm{{<}}\textit{a}% \textrm{{>}}$
	$\displaystyle\textit{b2}\mathbin{\texttt{<:}}{}{\tt Box}\textrm{{<}}\textit{a}% \textrm{{>}}$

The variables b1 and b2 on the right side are type placeholders for the types of b1 and b2, respectively. A constraint solver has to find a substitution for those type placeholders that satisfies all constraints. A satisfying substitution can afterwards be translated into a well-typed Java program by adding the type calculated for b1 (b2) to the variable definition of b1 (b2) in the input program.

In Java, ${\tt Box}\textrm{{<}}{\tt?}\textrm{{>}}$ is treated as an existential type $\exists{\tt X}.{\tt Box}\textrm{{<}}{\tt X}\textrm{{>}}$ which is implicitly opened for this method call. To answer the question if the variable b1 can have the type Box<?> in Java, we would have to find a solution for the constraints in Figure 3. In this case, a solution is a substitution for the type placeholders b1 and b2 in compliance with the given constraints. But the constraints shown in Figure 3 have no solution.

	$\displaystyle\exists{\tt X}.{\tt Box}\textrm{{<}}{\tt X}\textrm{{>}}\mathbin{% \texttt{<:}}{}{\tt Box}\textrm{{<}}\textit{a}\textrm{{>}}$
	$\displaystyle\textit{b2}\mathbin{\texttt{<:}}{}{\tt Box}\textrm{{<}}\textit{a}% \textrm{{>}}$

Figure 2: Java’s subtype constraints.

	$\displaystyle{\tt Box}\textrm{{<}}{\tt?}\textrm{{>}}\mathbin{\texttt{<:}}{}{% \tt Box}\textrm{{<}}\textit{a}\textrm{{>}}$
	$\displaystyle\textit{b2}\mathbin{\texttt{<:}}{}{\tt Box}\textrm{{<}}\textit{a}% \textrm{{>}}$

Figure 3: Java-TX subtype constraints.

On the other hand, Java-TX can handle the example easily. In the resulting constraint set in Figure 3, Java-TX treats the wildcard ${\tt?}$ like any other type. The substitution $\textit{a}\to{\tt?}$ and $\textit{b1}\to{\tt Box}\textrm{{<}}{\tt?}\textrm{{>}}$ and $\textit{b2}\to{\tt Box}\textrm{{<}}{\tt?}\textrm{{>}}$ leads to ${\tt Box}\textrm{{<}}{\tt?}\textrm{{>}}\mathbin{\texttt{<:}}{}{\tt Box}\textrm% {{<}}{\tt?}\textrm{{>}}$ , ${\tt Box}\textrm{{<}}{\tt?}\textrm{{>}}\mathbin{\texttt{<:}}{}{\tt Box}\textrm% {{<}}{\tt?}\textrm{{>}}$ and is a valid solution.

2.4 Java-TXUse Cases

A static type system helps programmers in many ways. Coupled with an IDE [10] it can identify errors on the spot, show additional information, and even propose code completions. But at times it can generate considerable overhead, if type annotations are required in (too) many places as in Java. If one annotation is changed, for example a ${\tt List}\textrm{{<}}String\textrm{{>}}$ to a ${\tt Set}\textrm{{<}}String\textrm{{>}}$ , this change can ensue a cascade of type changes throughout the program. A study that checked the git logs of 129 Java projects [9] found that type changes are even more frequent than renamings. In a survey presented by Negara et al. [11] 86.4% of the 420 participants demanded automated IDE support for type changes in Java.

Consider the Change Field Type example in Figure 4. After changing ${\tt int}\to{\tt long}$ of the field mileage the programmer has to manually change the types at and . A global type inference (GTI) algorithm would render manual type changes obsolete. With full GTI, no type annotations are needed and it is sufficient to change the field types in the class definition.

⬇

class TypeChangeExample {

int mileage;

int getMileage(){

return mileage;

}

void update(int m){

mileage += m;

}

(a) Before.

⬇

class TypeChangeExample {

long mileage;

long getMileage(){

return mileage;

}

void update(

long m){

mileage += m;

}

(b) After long

\to

int.

Figure 4: Change Field Type. Example from Negara et al [11].

Java-TXprovides a global type inference algorithm and adds some further convenience features. For example, Java-TX comes with a predefined bundle of function types of the form Fun $N$ $$< $T_{1},\ldots,T_{N}$ , $R$ > (where $N$ is the number of arguments) with contravariant argument types and covariant return types [16]. Function types are assigned to lambda expressions.

In the following we give some examples of programming with Java-TX.

Example 1.

Consider a lambda-expression that takes three arguments (two values and a function) where the function is applied to the two arguments.

⬇

x -> y -> f -> f.apply(x,y);

In Java, using the package java.util.function the principal type would be

⬇

Function<? super A,

? extends Function<? super B,

? extends Function<

? super BiFunction<? super A,

? super B,

? extends C>>,

? extends C>>>

As Function is an ordinary Java interface, covariance and contravariance have to be expressed by wildcards. The equivalent Java-TX type is much simpler:

⬇

Fun1$$<A, Fun1$$<B, Fun2$$<A, B, C>, C>>

⬇

class OL {

m(x) { return x + x; }

m(x) { return x || x; }

}

class OLMain {

main(x) {

var ol = new OL();

return ol.m(x);

}

Listing 4: Overloading

Example 2.

The example in Listing 4 illustrates the extended overloading mechanism of Java-TX. In the class OL, the method name m is overloaded by two different method declarations. If the types Integer, Double, String, and Boolean are visible the type inference algorithm infers intersection types

\begin{array}[t]{rcl}{\mathtt{m}}&{:}&{\mathtt{Integer}\rightarrow\mathtt{% Integer}}\\ &{\wedge}&{\texttt{Double}\rightarrow\mathtt{Double}}\\ &{\wedge}&{\texttt{String}\rightarrow\texttt{String}}\\ \\ {\mathtt{m}}&{:}&{\mathtt{Boolean}\rightarrow\mathtt{Boolean}}\end{array}\ \ % \ \ \ \ \ \ \ \ \begin{array}[t]{rcl}{\mathtt{main}}&{:}&{\mathtt{Integer}% \rightarrow\mathtt{Integer}}\\ &{\wedge}&{\texttt{Double}\rightarrow\mathtt{Double}}\\ &{\wedge}&{\texttt{String}\rightarrow\texttt{String}}\\ &{\wedge}&{\mathtt{Boolean}\rightarrow\mathtt{Boolean}}\end{array}

which are resolved in bytecode by overloaded methods. While function types are covered by our soundness proof, intersection types are not.

To obtain this result from global type inference, the programmer has to include the following import declarations

⬇

import java.lang.Integer

import java.lang.Double

import java.lang.String

import java.lang.Boolean

A less restrictive import declaration like java.lang.* would extend the visibility to Float, Long, and so on. This declaration would lead to additional conjuncts in the intersection type, but their presence severely affects the performance of type inference. The use of visibility in Java-TX is comparable to the way that Haskell manages type classes: type class instances are only considered by the type checker if the modules containing them are imported.

Example 3.

Listing 5 shows the matrix multiplication in Java-TX.

⬇

class Matrix extends Vector<Vector<Integer>> {

mul(m) {

var ret = new Matrix();

for(v1 : this) {

for(j ...) {

var erg = 0;

for(k ...) {

erg = erg + v1.get(k) * m.get(k).get(j);

} ...

}

return ret;}

}

Listing 5: Matrix multiplication

The class Matrix is implemented as an extension of $\mathtt{Vector}$ < $\mathtt{Vector}$ < $\mathtt{Integer}$ >>. The method mul implements the multiplication of two matrices this and m. An obvious typing of mul would be Matrix mul(Matrix m). However, this typing is not the only possible typing. In fact, it is easy to see that there are further typings. Here are some alternatives:

$\blacksquare$

⬇

Matrix mul(Vector<Vector<Integer>> m)
$\blacksquare$

⬇

Vector<Vector<Integer>> mul(Vector<Vector<Integer>> m)
$\blacksquare$

⬇

Matrix mul(Vector<? extends Vector<? extends Integer>> m)

Java-TXinfers a maximal type for the method wrt. the subtyping ordering of function types where argument types are contravariant and return types are covariant. For this example, type inference determines the maximal type as

⬇

Matrix mul(Vector<? extends Vector<? extends Integer>> m)

Global type inference for Java-TX does not come cheap. The underlying type unification algorithm is NP-hard [17], but there are some heuristics that improve the running time significantly [14].

3 Featherweight Java-TX

In this section, we define FJ-TX, a core calculus for Java-TX in the style of Featherweight Java [8].

3.1 Syntax

$\displaystyle{\tt N}$ $\displaystyle::={\tt C}\textrm{{<}}{\overline{{\tt E}}}\textrm{{>}}$ $\displaystyle{\tt T},{\tt U},{\tt L}$ $\displaystyle::={\tt N}\mid{\tt X}$ $\displaystyle{\tt E},{\tt F},{\tt G}$ $\displaystyle::={\tt T}\mid{\tt W}$ $\displaystyle{\tt W}$ $\displaystyle::={\text{{\tt?}}^{{\tt U}}_{{\tt L}}}$ $\displaystyle{\tt P}$ $\displaystyle::={\tt class}\ {\tt C}\textrm{{<}}\overline{{\tt X}}% \triangleleft\overline{{\tt T}}\textrm{{>}}\triangleleft\ {\tt N}\ \{\overline% {{\tt T}}\ \overline{{\tt f}};\,\overline{{\tt M}}\}$ $\displaystyle{\tt M}$ $\displaystyle::={\tt}\textrm{{<}}\overline{{\tt X}}\triangleleft\overline{{\tt T% }}\textrm{{>}}\ {\tt T}\ {\tt m}(\overline{{\tt T}}\ \overline{{\tt x}})\ \{{% \tt return}\ {\tt e};\}$ $\displaystyle{\tt e}$ $\displaystyle::={\tt x}\mid{{\tt e}}.{\tt f}\mid{{\tt e}}.{\tt m}(\overline{{% \tt e}})\mid{\tt new}\ {\tt N}(\overline{{\tt e}})\mid({\tt T}){\tt e}\mid{\tt null}$

Figure 5: Syntax of FJ-TX.

Fig. 5 defines the syntax of FJ-TX. It extends Featherweight Generic Java (FGJ) [8] with wildcards. We let ${\tt C}$ range over class names including the predefined names ${\tt Object}$ and $\bot$ (the empty type), which do not take parameters. As wildcards are not allowed in all positions of the syntax, we distinguish several syntactic categories of types:

X: type variables.
N: ranges over class types.
T, U, L: range over all FJ-TX types, except top-level wildcards.
E, F, G: range over all types including wildcards.
W: ranges over wildcard types. The notation $\text{{\tt?}}^{{\tt U}}_{{\tt L}}$ denotes a wildcard with lower bound ${\tt L}$ and upper bound ${\tt U}$ . For example, we write $\text{{\tt?}}^{\texttt{Integer}}_{\bot}$ for ? extends Integer, where $\bot$ stands for the lower bound of all types. Analogously, $\text{{\tt?}}^{\texttt{Object}}_{\texttt{Number}}$ stands for ? super Number.

3.2 Typing

A context $\Gamma$ is a finite mapping from variables to types, written $\overline{{\tt x}}:\overline{{\tt E}}$ . A type context $\Delta$ is a finite relation between type variables and types. Each type variable ${\tt X}$ can be related to at most two types, some type ${\tt T}\neq{\tt X}$ and ${\tt X}$ itself (reflexive subtyping constraint). We write $\overline{\mathtt{X}}\mathbin{\texttt{<:}}\overline{\mathtt{T}}$ for the non-reflexive part, which associates each type variable to its declared bound, and treat the reflexive constraints $(\mathtt{X}\mathbin{\texttt{<:}}\mathtt{X})$ separately.

A class definition has its type arguments split in two parts, ${\tt class}\ {\tt C}\textrm{{<}}\overline{{\tt X}}\triangleleft\overline{{\tt N% }},\overline{{\tt Y}}\triangleleft\overline{{\tt Y}}\textrm{{>}}$ , but during class instantiation we write just ${\tt new}\ {\tt C}\textrm{{<}}\overline{{\tt E}}\textrm{{>}}$ . The list of type arguments $\overline{{\tt E}}$ has the length of the first part $\overline{{\tt X}}$ from the class definition. For example an instance of the class definition ${\tt class}\ {\tt Example}\textrm{{<}}{\tt X}\triangleleft{\tt String},{\tt X}% \triangleleft{\tt X}\textrm{{>}}$ looks like ${\tt Example}\textrm{{<}}{\tt String}\textrm{{>}}$ .

Fig. 6 defines the well-formedness judgment for types $\Delta\vdash\mathtt{E}\ \texttt{OK}$ and two subtyping relations: $\Delta\vdash\mathtt{{E}\mathbin{\texttt{<:}}{E}}$ for top-level subtyping and $\Delta\vdash{\tt W}\textrm{$\,\lessdot_{?}\,$}{\tt W}$ for use-site variance subtyping, which is invoked by the former inside of type parameters.

Well-formed types:

Subtyping:

Use-site variance subtyping:

Figure 6: Well-formedness and subtyping.

We discuss the subtyping rules emphasizing the differences between FJ-TX and FGJ.

The rules for well-formed types are mostly unchanged. The new rule WF-Wildcard guarantees that the lower bound of a wildcard is a subtype of its upper bound.

The rule S-Refl is restricted to types of the form N. This change enforces that reflexivity does not apply to type variables and wildcards.

Subtyping is transitive as usual (S-Trans). The rules S-Var and S-Class are similar to FGJ.

There are three new rules that manage wildcards.

The rules S-WC-Super and S-WC-Extends relate a wildcard type to its lower and upper bound, respectively.

The rule S-WC-Class introduces use-site variance by invoking a subsidiary relation, use-site variance subtyping $\,\lessdot_{?}\,$ . This relation checks if the types in argument position induce covariant, contravariant, or invariant subtyping.

That is, $\mathtt{List}$ < $\mathtt{Integer}$ > is a subtype of $\mathtt{List}$ < $\mathtt{\textrm{?\,extends}\linebreak[0]\,Object}$ > due to use-site variance subtyping of the type arguments $\mathtt{Integer}\textrm{$\,\lessdot_{?}\,$}\text{{\tt?}}^{\mathtt{Object}}_{\bot}$ .

For example, in combination with S-Trans we can conclude from $\mathtt{T}\mathbin{\texttt{<:}}\mathtt{T}^{\prime}$ that $\text{{\tt?}}^{\mathtt{T}}_{\mathtt{T}^{\prime\prime}}\mathbin{\texttt{<:}}% \text{{\tt?}}^{\mathtt{T}^{\prime\prime\prime}}_{\mathtt{T}^{\prime}}$ .

There are two rules for use-site variance subtyping. The rule USV-Extends enables covariance and contravariance for wildcards. The rules USV-Equals enforces invariant subtyping in all cases where the right-hand side is not a wildcard.

Field lookup:

Method lookup:

Method Overriding:

Expression typing:

Figure 7: Expression Typing rules.

Method typing:

Field typing:

Class typing:

Figure 8: Class Typing rules.

Finally, we consider the rules for typing classes, methods, fields, and expressions. Fig. 7 defines the judgments for expression typing $\mbox{$\Delta;\Gamma$}\vdash{\tt e}:{\tt W}$ . Fig. 8 contains method typing, field typing, and class typing. The rules are similar to those of FGJ although there are two differences. First, the rule T-Field is added. This rule is needed to guarantee the soundness of top-level wildcard instantiation. If the subtyping $\mathtt{C}$ < $\mathtt{\overline{E}^{\prime}}$ > $\,\mathbin{\texttt{<:}}\,$ $\mathtt{C}$ < $\mathtt{\overline{E}}$ > holds for a class type, its field types F must satisfy $\mathtt{[\overline{E}^{\prime}/\overline{X}]F}\textrm{$\,\mathbin{\texttt{<:}}% \,$}\mathtt{[\overline{E}/\overline{X}]F}$ . We discuss the rationale for this typing rule in Example 5. Furthermore, we need an extension of the type variable instance, where we distinguish instantiations of type without top-level wildcards T and wildcard type W.

3.3 Examples

The following examples demonstrate the intuition of the calculus. The first example shows the idea of wildcards in the argument position of generic types.

The first example illustrates why the S-Refl rule in FJ-TX is restricted to ground types N (types without top-level type variables), rather than arbitrary types T (including generic type variables), and what consequences this has for methods whose type variables require a reflexive bound.

Example 4.

Consider the following method shuffle:

⬇

<X extends Object> List<List<X>> shuffle(List<List<X>> l){

l.addElement(addElement(l.get(0).get(0)));

}

This method is not accepted. As l.get(0).get(0) has type X and addElement takes a value of type X, we need $\texttt{X}\mathbin{\texttt{<:}}\texttt{X}$ . However, subtyping is not reflexive on type variables!

To make the method acceptable, we have to change the bound of X from Object to X (a reflexive bound).

⬇

<X extends X> List<List<X>> shuffle(List<List<X>> l){

l.addElement(addElement(l.get(0).get(0)));

}

Now the S-VAR rule enables us to conclude $\texttt{X}\mathbin{\texttt{<:}}\texttt{X}$ , such that the type checker accepts this method.

Due to the reflexive constraint, we cannot use shuffle with wildcards. Consider:

⬇

void error(List<List<?>> anyL){

shuffle<?>(anyL);

}

The method error is not typeable, because the GT-Invk rule requires $\Delta\vdash{\tt?}\mathbin{\texttt{<:}}[{\tt?}/{\tt X}]{\tt X}$ , which is not given. Any non wildcard instantiation of X would be accepted.

Example 5.

The T-Field rule declares that if ${\tt A}$ is a subtype of ${\tt B}$ ( ${\tt A}\mathbin{\texttt{<:}}{}{\tt B}$ ) then any field of ${\tt A}$ must be a subtype of the respective field in ${\tt B}$ . The example in Fig. 9 demonstrates why this property is needed to ensure soundness. Variable ${\tt b}$ of type ${\tt Box}\textrm{{<}}{\tt?}\textrm{{>}}$ contains an instance of ${\tt Box}\textrm{{<}}{\tt String}\textrm{{>}}$ , which is possible because ${\tt Box}\textrm{{<}}{\tt String}\textrm{{>}}\mathbin{\texttt{<:}}{}{\tt Box}% \textrm{{<}}{\tt?}\textrm{{>}}$ . The field access expression ${\tt b}.{\tt boxed}$ has type ${\tt Box}\textrm{{<}}{\tt Box}\textrm{{<}}{\tt?}\textrm{{>}}\textrm{{>}}$ , because ${\tt b}$ is of type ${\tt Box}\textrm{{<}}{\tt?}\textrm{{>}}$ . But as we know, the type behind ${\tt b}$ is actually an instance of ${\tt Box}\textrm{{<}}{\tt String}\textrm{{>}}$ meaning that the field ${\tt boxed}$ is an instance of ${\tt Box}\textrm{{<}}{\tt Box}\textrm{{<}}{\tt String}\textrm{{>}}\textrm{{>}}$ . The resulting problem is that ${\tt Box}\textrm{{<}}{\tt Box}\textrm{{<}}{\tt String}\textrm{{>}}\textrm{{>}}$ is not a subtype of ${\tt Box}\textrm{{<}}{\tt Box}\textrm{{<}}{\tt?}\textrm{{>}}\textrm{{>}}$ , leading to an unsound program. In this example, a Box<Integer> would be added to a ${\tt Box}\textrm{{<}}{\tt Box}\textrm{{<}}{\tt String}\textrm{{>}}\textrm{{>}}$ . We address this issue with the new T-Field rule. It forces us to add the reflexive constraint in the class definition of Box in Fig. 9 as in class Box<X extends X>, which prevents a type like ${\tt Box}\textrm{{<}}{\tt?}\textrm{{>}}$ to exist.

⬇

class Box<X> {

Box<Box<X>> boxed;

void set(X value){ .. }

}

Box<?> b = new Box<String>(new Box<Box<String>>(null));

b.boxed.set(new Box<Integer>(1)); // error!

Figure 9: Unsound Field Access Example.

Computation:

Errors:

Figure 10: FJ-TX: Reduction Rules.

3.4 Operational semantics

Fig. 10 defines small-step operational semantics of FJ-TX. They include null pointer and cast exceptions ( ${\tt e}\ {\tt err}$ ).

4 Soundness

In this section, we prove the type soundness theorem for FJ-TX.

Theorem 6 (Soundness).

Suppose that $\emptyset;\emptyset\vdash\mathtt{e:{\color[rgb]{0,0,0}E}}$ and $\mathtt{e}\longrightarrow^{*}{\mathtt{e}^{\prime}}$ , then either:

$\blacksquare$

$\mathtt{{e^{\prime}}}$ is a value,
$\blacksquare$

there exists $\mathtt{e}^{\prime}\longrightarrow{\mathtt{e}^{\prime\prime}}$ where $\emptyset;\emptyset\vdash\mathtt{e^{\prime\prime}:{\color[rgb]{0,0,0}E^{\prime% }}}$ with ${\tt E^{\prime}}={\tt E}$ or $\emptyset\vdash{\tt E^{\prime}}\mathbin{\texttt{<:}}{}{\tt E}$ , or
$\blacksquare$

$\mathtt{{e^{\prime}}}$ runs into an Exception ${\tt e^{\prime}}\ {\tt err}$ .

We define values as a subset of irreducible expressions by the following grammar.

\displaystyle{\tt v}

\displaystyle::=({\tt new}\ {\tt N}(\overline{{\tt v}}))\mid{\tt null}

We prove this theorem in the usual way by induction on the reduction sequence from type preservation (Thm. 12) and progress (Thm. 13).

We start with some lemmas about substitution. Their proofs are similar to the ones for other Featherweight Java calculi using existential types (e.g. [4], [3]).

Note that in our type system not all types are reflexive. Therefore saying $\emptyset\vdash{\tt E^{\prime}}\mathbin{\texttt{<:}}{}{\tt E}$ in the Soundness and the preservation theorem does not necessarily include the case where ${\tt E^{\prime}}={\tt E}$ and we have to state both possibilities. This is the biggest difference between this proof and proofs for similar calculi.

Bierhoff suspected in [3] that requiring wildcards to have a lower bound that is a subtype of their upper bound allows ${\tt null}$ values to be typed with the bottom type $\bot$ without any complications. Our calculus requires this property to achieve soundness regardless of whether a ${\tt null}$ expression is involved, and we can affirm that ${\tt null}$ caused no complications in our soundness proof.

Lemma 7 (Type substitution preserves subtyping).

If $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}}\vdash{\tt E}% \mathbin{\texttt{<:}}{}{\tt F}$ and $\vdash[\overline{{\tt G}}/\overline{{\tt X}}](\overline{{\tt X}}\mathbin{% \texttt{<:}}{}\overline{{\tt U}})$ then $\vdash[\overline{{\tt G}}/\overline{{\tt X}}]{\tt E}\mathbin{\texttt{<:}}{}[% \overline{{\tt G}}/\overline{{\tt X}}]{\tt F}$

Proof.

By induction on the derivation $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}}\vdash{\tt E}% \mathbin{\texttt{<:}}{}{\tt F}$ :

Case

S-Var. By inversion we obtain ${\tt E}={\tt X_{i}}$ and ${\tt F}={\tt U_{i}}$ . From the assumption $\vdash[\overline{{\tt G}}/\overline{{\tt X}}](\overline{{\tt X}}\mathbin{% \texttt{<:}}{}\overline{{\tt U}})$ , we have ${\tt G_{i}}\mathbin{\texttt{<:}}{}[\overline{{\tt G}}/\overline{{\tt X}}]{\tt U% _{i}}$ , which is the same as $\vdash[\overline{{\tt G}}/\overline{{\tt X}}]{\tt X_{i}}\mathbin{\texttt{<:}}{% }[\overline{{\tt G}}/\overline{{\tt X}}]{\tt U_{i}}$ .

Case

S-Refl is immediate.

Case

For S-WC-Super and S-WC-Extends we obtain $\vdash[\overline{{\tt G}}/\overline{{\tt X}}]{\tt T}\mathbin{\texttt{<:}}{}[% \overline{{\tt G}}/\overline{{\tt X}}]{\tt T^{\prime}}$ by induction, so the conclusion is immediate.

Case

S-Trans $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}}\vdash{\tt E}% \mathbin{\texttt{<:}}{}{\tt F}$ with $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}}\vdash{\tt E}% \mathbin{\texttt{<:}}{}{\tt E^{\prime}}$ and $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}}\vdash{\tt E^{% \prime}}\mathbin{\texttt{<:}}{}{\tt F}$ . By induction we have $\vdash[\overline{{\tt G}}/\overline{{\tt X}}]{\tt E}\mathbin{\texttt{<:}}{}[% \overline{{\tt G}}/\overline{{\tt X}}]{\tt E^{\prime}}$ and $\vdash[\overline{{\tt G}}/\overline{{\tt X}}]{\tt E^{\prime}}\mathbin{\texttt{% <:}}{}[\overline{{\tt G}}/\overline{{\tt X}}]{\tt F}$ . Then $\vdash[\overline{{\tt G}}/\overline{{\tt X}}]{\tt E}\mathbin{\texttt{<:}}{}[% \overline{{\tt G}}/\overline{{\tt X}}]{\tt F}$ by S-Trans.

Case

S-Class. We have $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}}\vdash{\tt C}% \textrm{{<}}\overline{{\tt E}}\textrm{{>}}\mathbin{\texttt{<:}}{}[\overline{{% \tt E}}/\overline{{\tt Y}}]{\tt N}$ and $\texttt{class}\ {\tt C}\textrm{{<}}\overline{{\tt Y}}\triangleleft\overline{{% \tt T}}\textrm{{>}}\triangleleft{\tt N}$ . By T-Class we know $\textit{fv}({\tt N})\subseteq\overline{{\tt Y}}$ leading to $\textit{fv}([\overline{{\tt E}}/\overline{{\tt Y}}]{\tt N})\subseteq\{% \overline{{\tt X}}\}$ and from well-formedness $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}}\vdash\overline{{% \tt E}}\mathbin{\texttt{<:}}{}[\overline{{\tt E}}/\overline{{\tt Y}}]\overline% {{\tt T}}$ .

We have to show well-formedness $[\overline{{\tt G}}/\overline{{\tt X}}]\overline{{\tt E}}\mathbin{\texttt{<:}}% {}[\overline{{\tt G}}/\overline{{\tt X}}][\overline{{\tt E}}/\overline{{\tt Y}% }]\overline{{\tt T}}$ , that is, $[\overline{{\tt G}}/\overline{{\tt X}}]\overline{{\tt E}}\mathbin{\texttt{<:}}% {}[[\overline{{\tt G}}/\overline{{\tt X}}]\overline{{\tt E}}/\overline{{\tt Y}% }]\overline{{\tt T}}$ , to conclude ${\tt C}\textrm{{<}}[\overline{{\tt G}}/\overline{{\tt X}}]\overline{{\tt E}}% \textrm{{>}}\mathbin{\texttt{<:}}{}[[\overline{{\tt G}}/\overline{{\tt X}}]% \overline{{\tt E}}/\overline{{\tt Y}}]{\tt N}$ by S-Class. The latter is the same as $[\overline{{\tt G}}/\overline{{\tt X}}]{\tt C}\textrm{{<}}\overline{{\tt E}}% \textrm{{>}}\mathbin{\texttt{<:}}{}[\overline{{\tt G}}/\overline{{\tt X}}][% \overline{{\tt E}}/\overline{{\tt Y}}]{\tt N}$ .

Case

S-WC-Class. Suppose that $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}}\vdash{\tt C}% \textrm{{<}}\overline{{\tt E}}\textrm{{>}}\mathbin{\texttt{<:}}{}{\tt C}% \textrm{{<}}\overline{{\tt E^{\prime}}}\textrm{{>}}$ and $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}}\vdash\overline{{% \tt E}}\textrm{$\,\lessdot_{?}\,$}\overline{{\tt E^{\prime}}}$ . We have to show for every ${\tt E_{i}}\in\overline{{\tt E}}$ and ${\tt E^{\prime}_{i}}\in\overline{{\tt E^{\prime}}}$ that $[\overline{{\tt G}}/\overline{{\tt X}}]{\tt E_{i}}\textrm{$\,\lessdot_{?}\,$}[% \overline{{\tt G}}/\overline{{\tt X}}]{\tt E^{\prime}_{i}}$ . There are two subcases:

Case: USV-Extends. Inversion applied to $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}}\vdash{\tt E}% \textrm{$\,\lessdot_{?}\,$}\text{{\tt?}}^{U}_{L}$ yields $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}}\vdash{\tt L}% \mathbin{\texttt{<:}}{}{\tt E}$ and $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}}\vdash{\tt E}% \mathbin{\texttt{<:}}{}{\tt U}$ . Then $\vdash[\overline{{\tt G}}/\overline{{\tt X}}]{\tt L}\mathbin{\texttt{<:}}{}[% \overline{{\tt G}}/\overline{{\tt X}}]{\tt E}$ and $\vdash[\overline{{\tt G}}/\overline{{\tt X}}]{\tt E}\mathbin{\texttt{<:}}{}[% \overline{{\tt G}}/\overline{{\tt X}}]{\tt U}$ by induction hypothesis. Applying USV-Extends yields $\vdash[\overline{{\tt G}}/\overline{{\tt X}}]{\tt E}\textrm{$\,\lessdot_{?}\,$% }[\overline{{\tt G}}/\overline{{\tt X}}]\text{{\tt?}}^{U}_{L}$ .
Case: USV-Equals is immediate by induction.

$\hfill\blacktriangleleft$

Lemma 8 (Type substitution preserves typing).

If $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}};\Gamma\vdash{\tt e% }:{\tt E}$ and $\vdash[\overline{{\tt G}}/\overline{{\tt X}}](\overline{{\tt X}}\mathbin{% \texttt{<:}}{}\overline{{\tt U}})$ then $\emptyset;[\overline{{\tt G}}/\overline{{\tt X}}]\Gamma\vdash[\overline{{\tt G% }}/\overline{{\tt X}}]{\tt e}:[\overline{{\tt G}}/\overline{{\tt X}}]{\tt E}$

Proof.

We write $\Delta=\overline{{\tt X}\mathbin{\texttt{<:}}{}{\tt U}}$ and proceed by induction over the derivation $\Delta;\Gamma\vdash{\tt e}:{\tt T}$ .

Case: T-Var. Assuming $\overline{{\tt X}\mathbin{\texttt{<:}}{}{\tt U}};\Gamma\cup\{\,{\tt x}:{\tt T}% \,\}\vdash{\tt x}:{\tt T}$ we get after substitution $\emptyset;[\overline{{\tt G}}/\overline{{\tt X}}]\Gamma\cup\{\,{\tt x}:[% \overline{{\tt G}}/\overline{{\tt X}}]{\tt T}\,\}\vdash x:[\overline{{\tt G}}/% \overline{{\tt X}}]{\tt T}$ and we finish this case by T-Var.
Case: T-Null. Immediate.
Case: T-Access. We have $\overline{{\tt X}\mathbin{\texttt{<:}}{}{\tt U}};\Gamma\vdash{\tt e}.{\tt f}:{% \tt E}$ where $\overline{{\tt X}\mathbin{\texttt{<:}}{}{\tt U}};\Gamma\vdash{\tt e}:{\tt E_{0}}$ , $\overline{{\tt X}\mathbin{\texttt{<:}}{}{\tt U}}\vdash{\tt E}\mathbin{\texttt{% <:}}{}{\tt N}$ and $\textit{fields}({\tt N})=\overline{{\tt T}}\ \overline{{\tt f}}$ by assumption. $\emptyset,[\overline{{\tt G}}{}/\overline{{\tt X}}]\Gamma\vdash[\overline{{\tt G% }}{}/\overline{{\tt X}}]{\tt e}:[\overline{{\tt G}}{}/\overline{{\tt X}}]{\tt E% ^{\prime}_{0}}$ by induction hypothesis. $[\overline{{\tt G}}{}/\overline{{\tt X}}]{\tt E}\mathbin{\texttt{<:}}{}[% \overline{{\tt G}}{}/\overline{{\tt X}}]{\tt N}$ by lemma 8 and $\textit{fields}([\overline{{\tt G}}{}/\overline{{\tt X}}]{\tt N})=[\overline{{% \tt G}}{}/\overline{{\tt X}}]\overline{{\tt T}}\ \overline{f}$ by definition of fields finishing the case.
Case: T-New. By premise of T-New and induction hypothesis we get $\emptyset;[\overline{{\tt G}}{}/\overline{{\tt X}}]\Gamma\vdash\overline{{\tt e% }}:[\overline{{\tt G}}{}/\overline{{\tt X}}]\overline{{\tt E}}$ . By the definition of fields we get $\textit{fields}({\tt C}\textrm{{<}}[\overline{{\tt G}}{}/\overline{{\tt X}}]% \overline{{\tt F}}\textrm{{>}})=[\overline{{\tt G}}{}/\overline{{\tt X}}]% \overline{{\tt T}}\ \overline{{\tt f}}$ . By lemma 7 we get $\emptyset\vdash[\overline{{\tt G}}{}/\overline{{\tt X}}]\overline{{\tt E}}% \mathbin{\texttt{<:}}{}[\overline{{\tt G}}{}/\overline{{\tt X}}]\overline{{\tt T}}$ , and $\emptyset\vdash[\overline{{\tt G}}{}/\overline{{\tt X}}][\overline{{\tt F}}/% \overline{{\tt X}}](\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}})$ . Therefore $\emptyset;[\overline{{\tt G}}{}/\overline{{\tt X}}]\Gamma\vdash{\tt new}\ {\tt C% }\textrm{{<}}[\overline{{\tt G}}{}/\overline{{\tt X}}]\overline{{\tt F}}% \textrm{{>}}(\overline{{\tt e}}):{\tt C}\textrm{{<}}[\overline{{\tt G}}{}/% \overline{{\tt X}}]\overline{{\tt F}}\textrm{{>}}$ finishing the case.
Case: T-Invk. By premise of T-Invk we have ${\tt e}={\tt e_{0}}.{\tt}\textrm{{<}}\overline{{\tt F}}\textrm{{>}}{\tt m}(% \overline{{\tt e}})$ and $\textit{mtype}({\tt m},{\tt C}\textrm{{<}}\overline{{\tt S}}\textrm{{>}})={\tt% }\textrm{{<}}\overline{{\tt Y}}\triangleleft\overline{{\tt P}}\textrm{{>}}% \overline{{\tt T}}\to{\tt T}$ and $\Delta;\Gamma\vdash{\tt e}:{\tt E}$ and $\Delta\vdash{\tt E}\mathbin{\texttt{<:}}{}{\tt C}\textrm{{<}}\overline{{\tt S}% }\textrm{{>}}$ and $\Delta;\Gamma\vdash\overline{{\tt e}}:\overline{{\tt E}}$ and $\Delta\vdash\overline{{\tt E}}\mathbin{\texttt{<:}}{}[\overline{{\tt F}}/% \overline{{\tt Y}}]\overline{{\tt T}}$ and $\Delta\vdash\overline{{\tt F}}\mathbin{\texttt{<:}}{}[\overline{{\tt F}}/% \overline{{\tt Y}}]\overline{{\tt P}}$ . By the inductive hypothesis we have $\emptyset;[\overline{{\tt G}}/\overline{{\tt X}}]\Gamma\vdash[\overline{{\tt G% }}/\overline{{\tt X}}]{\tt e}:[\overline{{\tt G}}/\overline{{\tt X}}]{\tt E}$ and $\emptyset;[\overline{{\tt G}}/\overline{{\tt X}}]\Gamma\vdash[\overline{{\tt G% }}/\overline{{\tt X}}]\overline{{\tt e}}:[\overline{{\tt G}}/\overline{{\tt X}% }]\overline{{\tt E}}$ .

By definition of mtype we have $\textit{mtype}({\tt m},[\overline{{\tt G}}/\overline{{\tt X}}]{\tt C}\textrm{{% <}}\overline{{\tt S}}\textrm{{>}})=[\overline{{\tt G}}/\overline{{\tt X}}]({% \tt}\textrm{{<}}\overline{{\tt Y}}\triangleleft\overline{{\tt U}}\textrm{{>}}% \overline{{\tt T}}\to{\tt T})$ . By lemma 7 we obtain $\vdash[\overline{{\tt G}}/\overline{{\tt X}}]{\tt E}\mathbin{\texttt{<:}}{}[% \overline{{\tt G}}/\overline{{\tt X}}]{\tt C}\textrm{{<}}\overline{{\tt S}}% \textrm{{>}}$ , $\vdash[\overline{{\tt G}}/\overline{{\tt X}}]\overline{{\tt E}}\mathbin{% \texttt{<:}}{}[\overline{{\tt G}}/\overline{{\tt X}}][\overline{{\tt F}}/% \overline{{\tt Y}}]\overline{{\tt T}}$ and $\vdash[\overline{{\tt G}}/\overline{{\tt X}}]\overline{{\tt F}}\mathbin{% \texttt{<:}}{}[\overline{{\tt G}}/\overline{{\tt X}}][\overline{{\tt F}}/% \overline{{\tt Y}}]\overline{{\tt P}}$ finishing the case by application of T-Invk.
Case: T-UCast. We have $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}};\Gamma\vdash({\tt U% }){\tt e}:{\tt U}$ with $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}};\Gamma\vdash{\tt e% }:{\tt T}$ and $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}}\vdash{\tt T}% \mathbin{\texttt{<:}}{}{\tt U}$ . $\emptyset;\Gamma\vdash[\overline{{\tt G}}/\overline{{\tt X}}]{\tt e}:[% \overline{{\tt G}}/\overline{{\tt X}}]{\tt T}$ by induction hypothesis and $\vdash[\overline{{\tt G}}/\overline{{\tt X}}]{\tt T}\mathbin{\texttt{<:}}{}[% \overline{{\tt G}}/\overline{{\tt X}}]{\tt U}$ by lemma 7. Leading to $\emptyset;[\overline{{\tt G}}/\overline{{\tt X}}]\Gamma\vdash([\overline{{\tt G% }}/\overline{{\tt X}}]{\tt U})[\overline{{\tt G}}/\overline{{\tt X}}]{\tt e}:[% \overline{{\tt G}}/\overline{{\tt X}}]{\tt U}$ by T-UCast.
Case: T-AnyCast. We have $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}};\Gamma\vdash({\tt U% }){\tt e}:{\tt U}$ with $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt U}};\Gamma\vdash{\tt e% }:{\tt T}$ . $\emptyset;\Gamma\vdash[\overline{{\tt G}}/\overline{{\tt X}}]{\tt e}:[% \overline{{\tt G}}/\overline{{\tt X}}]{\tt T}$ by induction hypothesis Leading to $\emptyset;[\overline{{\tt G}}/\overline{{\tt X}}]\Gamma\vdash([\overline{{\tt G% }}/\overline{{\tt X}}]{\tt U})[\overline{{\tt G}}/\overline{{\tt X}}]{\tt e}:[% \overline{{\tt G}}/\overline{{\tt X}}]{\tt U}$ by T-AnyCast.

$\hfill\blacktriangleleft$

We can substitute wildcard types, which are not reflexive, for free type variables because type variables are not reflexive either. Lemma 7 works as expected.

Lemma 9 (Term substitution preserves typing).

If $\emptyset;\overline{{\tt x}}:\overline{{\tt E}}\vdash e:{\tt E}$ and $\emptyset;\emptyset\vdash\overline{{\tt e}}:\overline{{\tt G}}$ where $\vdash\overline{{\tt G}}\mathbin{\texttt{<:}}{}\overline{{\tt E}}$ then $\emptyset;\emptyset\vdash[\overline{{\tt e}}/\overline{{\tt x}}]{\tt e}:{\tt F}$ with $\vdash{\tt F}\mathbin{\texttt{<:}}{}{\tt E}$

Proof.

By induction over the derivation of $\emptyset;\overline{{\tt x}}:\overline{{\tt E}}\vdash{\tt e}:{\tt E}$ .

Case: T-Var. By inversion $\emptyset;\overline{{\tt x}}:\overline{{\tt E}}\vdash{\tt x_{i}}:{\tt E_{i}}$ . From assumption $\vdash\overline{{\tt G}}\mathbin{\texttt{<:}}{}\overline{{\tt E}}$ we have $\vdash{\tt S_{i}}\mathbin{\texttt{<:}}{}{\tt E_{i}}$ and $[\overline{{\tt e}}/\overline{{\tt x}}]{\tt x_{i}}={\tt e_{i}}$ . Therefore $\emptyset;\emptyset\vdash[\overline{{\tt e}}/\overline{{\tt x}}]{\tt x_{i}}:{% \tt S_{i}}$ and $\vdash{\tt S_{i}}\mathbin{\texttt{<:}}{}{\tt E_{i}}$ .
Case: T-Null. Immediate.
Case: T-New. We have ${\tt e}={\tt new}\ {\tt N}(\overline{{\tt e^{\prime}}})$ and ${\tt E}={\tt N}$ with $\emptyset;\overline{{\tt x}}:\overline{{\tt E}}\vdash\overline{{\tt e^{\prime}% }}:\overline{{\tt E^{\prime}}}$ , $\textit{fields}({\tt N})=\overline{{\tt T}}\ \overline{{\tt f}}$ , $\vdash\overline{{\tt E^{\prime}}}\mathbin{\texttt{<:}}{}\overline{{\tt T}}$ . Induction yields $\vdash[\overline{{\tt e}}/\overline{{\tt x}}]\overline{{\tt e^{\prime}}}:% \overline{{\tt F^{\prime}}}$ where $\vdash\overline{{\tt F^{\prime}}}\mathbin{\texttt{<:}}{}\overline{{\tt T}}$ by S-Trans and $\vdash{\tt new}\ {\tt N}([\overline{{\tt e}}/\overline{{\tt x}}]\overline{{\tt e% ^{\prime}}}):{\tt N}$ by T-New and induction hypothesis.
Case: T-Access is similar to T-New. $\vdash{\tt e}:{\tt F}$ by induction where $\vdash{\tt F}\mathbin{\texttt{<:}}{}{\tt N}$ by S-Trans and $\vdash{\tt e}.{\tt f}_{i}:{\tt T_{i}}$ by T-Access as desired.
Case: T-Invk is similar to T-New and T-Access.
Case: T-UCast. We have $\emptyset;\overline{{\tt x}}:\overline{{\tt E}}\vdash({\tt U}){\tt e}:{\tt U}$ with $\emptyset;\overline{{\tt x}}:\overline{{\tt E}}\vdash{\tt e}:{\tt T}$ and $\vdash{\tt T}\mathbin{\texttt{<:}}{}{\tt U}$ . $\emptyset;\emptyset\vdash[\overline{{\tt e}}/\overline{{\tt x}}]{\tt e}:{\tt F}$ with $\vdash{\tt F}\mathbin{\texttt{<:}}{}{\tt E}$ by induction hypothesis following $\vdash{\tt F}\mathbin{\texttt{<:}}{}{\tt U}$ by S-Trans and finally $\emptyset;\emptyset\vdash({\tt U})[\overline{{\tt e}}/\overline{{\tt x}}]{\tt e% }:{\tt U}$ by T-UCast.
Case: T-AnyCast. Immediate.

$\hfill\blacktriangleleft$

The following lemma 10 shows that fields can change their types to a subtype when occurring in a subtype. Example:

⬇

class Test<X>{

Box<X> f;

}

Test<?> t = new Test<String>(); // t.f has type Box<?>

t.f = new Box<Integer>(); // because Box<Integer> \subeq{} Box<?>

The T-Field rule is necessary to address the problem illustrated in Fig. 9. When a new instance of the class ${\tt Box}\textrm{{<}}{\tt String}\textrm{{>}}$ is created the field boxed is of type ${\tt Box}\textrm{{<}}{\tt Box}\textrm{{<}}{\tt String}\textrm{{>}}\textrm{{>}}$ . Later when treating this Box as a ${\tt Box}\textrm{{<}}{\tt?}\textrm{{>}}$ its boxed field changes to ${\tt Box}\textrm{{<}}{\tt Box}\textrm{{<}}{\tt?}\textrm{{>}}\textrm{{>}}$ as well, but the actual value of boxed is still a ${\tt Box}\textrm{{<}}{\tt String}\textrm{{>}}$ . This would violate the preservation of subtyping by substitution.

Interestingly, there is no corresponding problem for method calls. This sounds counterintuitive, because a field access can also be seen as a method call with no parameters. So let us rewrite the Box example in Fig. 9 to use a method instead of a field:

⬇

class Box<X extends X>{

X value;

Box<Box<X>> boxed(){

return new Box<Box<X>>(new Box<X>(this.value));

}

The method boxed() creates the boxed value on demand. Here the reflexivity constraint X extends X is enforced by the expression new Box<X>(this.value), which demands value to have a subtype of X.

Lemma 10.

If $\vdash{\tt C}\textrm{{<}}\overline{{\tt E}}\textrm{{>}}\mathbin{\texttt{<:}}{}% {\tt N}$ and $\textit{fields}({\tt N})=\overline{{\tt T}}\ \overline{f}$ and ${\tt class}\ {\tt C}\textrm{{<}}\overline{{\tt X}}\triangleleft\overline{{\tt U% }}\textrm{{>}}$ and $\vdash[\overline{{\tt E}}/\overline{{\tt X}}](\overline{{\tt X}}\mathbin{% \texttt{<:}}{}\overline{{\tt U}})$ then $\textit{fields}({\tt C}\textrm{{<}}\overline{{\tt E}}\textrm{{>}})=\overline{{% \tt T^{\prime}}}\ \overline{f},\overline{{\tt S}}\ \overline{g}$ where ${\tt T^{\prime}_{i}}={\tt T_{i}}$ or $\vdash{\tt T^{\prime}_{i}}\mathbin{\texttt{<:}}{}{\tt T_{i}}$

Proof.

By induction over the subtype relation $\vdash{\tt C}\textrm{{<}}\overline{{\tt E}}\textrm{{>}}\mathbin{\texttt{<:}}{}% {\tt N}$ .

Case

S-Var, S-WC-Super and S-WC-Extends cannot occur, because there are no type variables in this context.

Case

S-Refl immediate.

Case

S-Bot cannot occur.

Case

S-Trans $\vdash{\tt C}\textrm{{<}}\overline{{\tt E}}\textrm{{>}}\mathbin{\texttt{<:}}{}% {\tt E}$ , $\vdash{\tt E}\mathbin{\texttt{<:}}{}{\tt N}$ . ${\tt E}$ can have one of the forms ${\tt N^{\prime}}$ or $\text{{\tt?}}^{{\tt U}}_{{\tt L}}$ .

Case: ${\tt E}={\tt N^{\prime}}$ . This case is immediate by induction.
Case: ${\tt E}=\text{{\tt?}}^{{\tt U}}_{{\tt L}}$ . Then $\vdash{\tt C}\textrm{{<}}\overline{{\tt E}}\textrm{{>}}\mathbin{\texttt{<:}}{}% \text{{\tt?}}^{{\tt U}}_{{\tt L}}$ and $\vdash\text{{\tt?}}^{{\tt U}}_{{\tt L}}\mathbin{\texttt{<:}}{}{\tt N}$ . Additionally ${\tt U}={\tt N_{U}}$ and ${\tt L}={\tt N_{L}}$ , because there are no free variables. Only the rules S-WC-Super and S-WC-Extends are applicable and therefore we know $\vdash{\tt N_{L}}\mathbin{\texttt{<:}}{}{\tt N_{U}}$ , ${\tt C}\textrm{{<}}\overline{{\tt E}}\textrm{{>}}\mathbin{\texttt{<:}}{}{\tt N% _{L}}$ and $\vdash{\tt N_{U}}\mathbin{\texttt{<:}}{}{\tt N}$ . Now induction hypothesis finishes this case.

Case

S-Class immediate by definition of fields.

Case

S-WC-Class $\vdash{\tt C}\textrm{{<}}\overline{{\tt E}}\textrm{{>}}\mathbin{\texttt{<:}}{}% {\tt C}\textrm{{<}}\overline{{\tt E^{\prime}}}\textrm{{>}}$ . This case is immediate by T-Field.

$\hfill\blacktriangleleft$

Lemma 11.

If $\textit{mtype}({\tt m},{\tt C}\textrm{{<}}\overline{{\tt G}}\textrm{{>}})=[% \overline{{\tt G}}/\overline{{\tt X}}]{\tt}\textrm{{<}}\overline{{\tt Y}}% \triangleleft\overline{{\tt U}}\textrm{{>}}\overline{{\tt T}}\to{\tt T}$ , $\overline{{\tt Y}}\triangleleft\overline{{\tt U}},\overline{{\tt X}}% \triangleleft\overline{{\tt U^{\prime}}};\overline{{\tt x}}:\overline{{\tt T}}% ,{\tt this}:{\tt C}\textrm{{<}}\overline{{\tt X}}\textrm{{>}}\vdash{\tt e_{0}}% :{\tt S}$ ${\tt class}\ {\tt C}\textrm{{<}}\overline{{\tt X}}\triangleleft\overline{{\tt U% ^{\prime}}}\textrm{{>}}\triangleleft{\tt D}\textrm{{<}}\overline{{\tt E^{% \prime}}}\textrm{{>}}\{\,\ldots\,\}$ , $\vdash{\tt e}:{\tt E}$ , $\vdash{\tt E}\mathbin{\texttt{<:}}{}{\tt C}\textrm{{<}}\overline{{\tt G}}% \textrm{{>}}$ , $\vdash[\overline{{\tt G}}/\overline{{\tt X}}](\overline{{\tt X}}\mathbin{% \texttt{<:}}{}\overline{{\tt U^{\prime}}})$ , and $\vdash\overline{{\tt e}}:\overline{{\tt E}}$ with $\vdash\overline{{\tt F}}\mathbin{\texttt{<:}}{}[\overline{{\tt F}}/\overline{{% \tt Y}}]\overline{{\tt U}}$ and $\vdash\overline{{\tt E}}\mathbin{\texttt{<:}}{}[\overline{{\tt G}}/\overline{{% \tt X}}][\overline{{\tt F}}/\overline{{\tt Y}}]\overline{{\tt T}}$ , then $\vdash[{\tt e^{\prime}}/{\tt this}][\overline{{\tt e}}/\overline{{\tt x}}]{\tt e% }:{\tt S}$ with $\vdash{\tt S}\mathbin{\texttt{<:}}{}[\overline{{\tt G}}/\overline{{\tt X}}][% \overline{{\tt F}}/\overline{{\tt Y}}]{\tt T}$

Proof.

By induction over the mtype function.

Case: M-Class: By premise of M-Class the method ${\tt m}$ is in a class ${\tt C}\textrm{{<}}\overline{{\tt X}}\triangleleft\overline{{\tt N}}\textrm{{>}}$ and by T-Method we have $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt N}},\overline{{\tt Y}}% \mathbin{\texttt{<:}}{}\overline{{\tt U}};\overline{{\tt x}}:\overline{{\tt T}% },{\tt this}:{\tt C}\textrm{{<}}\overline{{\tt X}}\textrm{{>}}\vdash{\tt e}:{% \tt E}$ , $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt N}},\overline{{\tt Y}}% \mathbin{\texttt{<:}}{}\overline{{\tt U}}\vdash{\tt E}\mathbin{\texttt{<:}}{}{% \tt T}$ .

By lemma 8 we get $\emptyset;\overline{{\tt x}}:[\overline{{\tt G}}/\overline{{\tt X}}][\overline% {{\tt F}}/\overline{{\tt Y}}]\overline{{\tt T}},{\tt this}:[\overline{{\tt G}}% /\overline{{\tt X}}][\overline{{\tt F}}/\overline{{\tt Y}}]{\tt C}\textrm{{<}}% \overline{{\tt X}}\textrm{{>}}\vdash{\tt e}:[\overline{{\tt G}}/\overline{{\tt X% }}][\overline{{\tt F}}/\overline{{\tt Y}}]{\tt E}$ . Then by lemma 9 we get $\vdash[{\tt C}\textrm{{<}}\overline{{\tt G}}\textrm{{>}}/{\tt this}][\overline% {{\tt e}}/\overline{{\tt x}}]{\tt e}:[\overline{{\tt G}}/\overline{{\tt X}}][% \overline{{\tt F}}/\overline{{\tt Y}}]{\tt E}$ . $\vdash[\overline{{\tt G}}/\overline{{\tt X}}][\overline{{\tt F}}/\overline{{% \tt Y}}]{\tt E}\mathbin{\texttt{<:}}{}[\overline{{\tt G}}/\overline{{\tt X}}][% \overline{{\tt F}}/\overline{{\tt Y}}]{\tt T}$ by lemma 7 finishing the case.
Case: M-Super $\textit{mtype}({\tt m},{\tt C}\textrm{{<}}\overline{{\tt G}}\textrm{{>}})=% \textit{mtype}({\tt m},[\overline{{\tt G}}/\overline{{\tt X}}]{\tt D}\textrm{{% <}}\overline{{\tt E^{\prime}}}\textrm{{>}})$ . ${\tt class}\ {\tt D}\textrm{{<}}\overline{{\tt X^{\prime}}}\triangleleft% \overline{{\tt S^{\prime}}}\textrm{{>}}\triangleleft{\tt N}$ by T-Class. By S-Class ${\tt C}\textrm{{<}}\overline{{\tt G}}\textrm{{>}}\mathbin{\texttt{<:}}{}[% \overline{{\tt G}}/\overline{{\tt X}}]{\tt D}\textrm{{<}}\overline{{\tt E}}% \textrm{{>}}$ and ${\tt E}\mathbin{\texttt{<:}}{}[\overline{{\tt G}}/\overline{{\tt X}}]{\tt D}% \textrm{{<}}\overline{{\tt E}}\textrm{{>}}$ by S-Trans. $\vdash[\overline{{\tt G}}/\overline{{\tt X}}][\overline{{\tt E^{\prime}}}/% \overline{{\tt X^{\prime}}}](\overline{{\tt X^{\prime}}}\mathbin{\texttt{<:}}{% }\overline{{\tt S^{\prime}}})$ by lemma 7 using $\overline{{\tt X}}\mathbin{\texttt{<:}}{}\overline{{\tt S}}\vdash[\overline{{% \tt E^{\prime}}}/\overline{{\tt X^{\prime}}}](\overline{{\tt X^{\prime}}}% \mathbin{\texttt{<:}}{}\overline{{\tt S^{\prime}}})$ by T-Class. Then induction hypothesis finishes the case.

$\hfill\blacktriangleleft$

Subtyping is not reflexive on type variables in our calculus, but it is on named types $\Delta\vdash{\tt N}\mathbin{\texttt{<:}}{}{\tt N}$ . This is because wildcard types are represented as interval types that can stand for any type inside of their bounds. When applying a computation step to an expression ${\tt e}$ the resulting expression ${\tt e^{\prime}}$ does not necessarily have a subtype of the previous expression’s type. For example a method call can have a wildcard type as its return type and an intermediate state during computation might look like this: $\{\,{\tt x}:{\tt List}\textrm{{<}}\text{{\tt?}}^{{\tt Object}}_{\bot}\textrm{{% >}}\,\}\vdash{\tt x}.{\tt get}():\text{{\tt?}}^{{\tt Object}}_{\bot}$ . After a term substitution we get $\vdash{\tt new}\ {\tt List}\textrm{{<}}{\tt String}\textrm{{>}}.{\tt get}():% \text{{\tt?}}^{{\tt Object}}_{\bot}$ , but the return type remains the wildcard $\text{{\tt?}}^{{\tt Object}}_{\bot}$ , which is not a subtype of itself. Therefore, the preservation theorem says that the result either has the same type or a subtype of the previous type.

Theorem 12 (Preservation).

If $\vdash{\tt e}:{\tt E}$ and ${\tt e}\longrightarrow{\tt e^{\prime}}$ then there exists some ${\tt E^{\prime}}$ with $\vdash{\tt e^{\prime}}:{\tt E^{\prime}}$ where either ${\tt E^{\prime}}={\tt E}$ or $\vdash{\tt E^{\prime}}\mathbin{\texttt{<:}}{}{\tt E}$ .

Proof.

By structural induction over the ${\tt e}\longrightarrow{\tt e^{\prime}}$ relation.

Case: R-Field. ${\tt e}=(\texttt{new}\ {\tt C}\textrm{{<}}\overline{{\tt S}}\textrm{{>}}(% \overline{{\tt e}})).f_{i}$ , ${\tt e^{\prime}}={\tt e}_{i}$ and $\textit{fields}({\tt N})=\overline{{\tt T}}\ \overline{{\tt f}}$ . We get by T-New $\vdash\texttt{new}\ {\tt C}\textrm{{<}}\overline{{\tt S}}\textrm{{>}}(% \overline{{\tt e}}):{\tt N}$ $\vdash\overline{{\tt e}}:\overline{{\tt E}}$ and $\vdash\overline{{\tt E}}\mathbin{\texttt{<:}}{}\overline{{\tt T}}$ , ${\tt class}\ {\tt C}\textrm{{<}}\overline{{\tt X}}\triangleleft\overline{{\tt T% ^{\prime}}}\textrm{{>}}$ , $\vdash\overline{{\tt S}}\mathbin{\texttt{<:}}{}[\overline{{\tt S}}/\overline{{% \tt X}}]\overline{{\tt T^{\prime}}}$ .

We get by T-Access $\vdash{\tt N}\mathbin{\texttt{<:}}{}{\tt N^{\prime}}$ and $\textit{fields}({\tt N^{\prime}})=\overline{{\tt U}}\ \overline{{\tt g}}$ and ${\tt E}={\tt U_{i}}$ . By lemma 10 either $\vdash{\tt T_{i}}\mathbin{\texttt{<:}}{}{\tt U_{i}}$ or ${\tt T_{i}}={\tt U_{i}}$ and in both cases $\vdash{\tt E_{i}}\mathbin{\texttt{<:}}{}{\tt U_{i}}$ (using S-Trans and $\vdash\overline{{\tt E}}\mathbin{\texttt{<:}}{}\overline{{\tt T}}$ ). Letting ${\tt E^{\prime}}={\tt E_{i}}$ finishes the case.
Case: C-Field: Given ${\tt e}={\tt e_{0}}.{\tt f}\longrightarrow{\tt e^{\prime}_{0}}.{\tt f}$ we get by T-Field $\vdash{\tt e}:{\tt E}$ , $\vdash{\tt E}\mathbin{\texttt{<:}}{}{\tt N}$ and $\textit{fields}({\tt N})=\overline{{\tt T}}\ \overline{{\tt f}}$ . By hypothesis and S-Trans we get $\vdash{\tt e}^{\prime}:{\tt T}^{\prime}$ with $\vdash{\tt T}^{\prime}\mathbin{\texttt{<:}}{}{\tt N}$ . Then letting ${\tt E^{\prime}}={\tt T_{i}}$ by lemma 10 finishing the case.
Case: R-Invk: ${\tt e}=({\tt new}\ {\tt C}\textrm{{<}}\overline{{\tt G}}\textrm{{>}}(% \overline{{\tt d}})).\texttt{m}{\tt}\textrm{{<}}\overline{{\tt F}}\textrm{{>}}% (\overline{{\tt e}})$ reduces to $[{\tt new}\ {\tt C}\textrm{{<}}\overline{{\tt G}}\textrm{{>}}(\overline{{\tt e% }})/{\tt this},\overline{{\tt d}}/\overline{{\tt x}}]{\tt e_{0}}$ with $mbody(\,\textrm{$\mathtt{m}$<$\mathtt{\overline{G}}$>},N\,)=\overline{{\tt x}}% .{\tt e}$ . We have by T-Invk and T-New: $\vdash\texttt{new}\ {\tt C}\textrm{{<}}\overline{{\tt G}}\textrm{{>}}(% \overline{{\tt e}}):{\tt N}$ , ${\tt class}\ {\tt C}\textrm{{<}}\overline{{\tt X}}\triangleleft\overline{{\tt N% }}\textrm{{>}}\{\,\ldots\,\}$ , $\vdash\overline{{\tt G}}\mathbin{\texttt{<:}}{}[\overline{{\tt G}}/\overline{{% \tt X}}]\overline{{\tt N}}$ , $\vdash{\tt N}\mathbin{\texttt{<:}}{}{\tt N}^{\prime}$ , $\textit{mtype}(m,{\tt N}^{\prime})={\tt}\textrm{{<}}\overline{{\tt Y}}% \triangleleft\overline{{\tt U}}\textrm{{>}}\overline{{\tt T}}\to{\tt T}$ , $\vdash\overline{{\tt e}}:\overline{{\tt E}}$ , $\vdash\overline{{\tt E}}\mathbin{\texttt{<:}}{}[\overline{{\tt F}}/\overline{{% \tt Y}}]\overline{{\tt T}}$ and $\vdash{\tt e}:[\overline{{\tt F}}/\overline{{\tt Y}}]{\tt T}$ . Additionally $\textit{mbody}({\tt C}\textrm{{<}}\overline{{\tt G}}\textrm{{>}},m{\tt}\textrm% {{<}}\overline{{\tt E}}\textrm{{>}})=\overline{{\tt x}}.{\tt e_{0}}$ by T-Method and override. By lemma 11 we get $\vdash[{\tt new}\ {\tt C}\textrm{{<}}\overline{{\tt G}}\textrm{{>}}(\overline{% {\tt e}})/{\tt this},\overline{{\tt d}}/\overline{{\tt x}}]{\tt e_{0}}:{\tt S}$ with $\vdash{\tt S}\mathbin{\texttt{<:}}{}{\tt[\overline{{\tt F}}/\overline{{\tt Y}}% ]{\tt T}}$ as desired.
Case: C-Invk: ${\tt e}.{\tt}\textrm{{<}}\overline{{\tt F}}\textrm{{>}}{\tt m}(\overline{{\tt e% }})$ reduces to ${\tt e^{\prime}}.{\tt}\textrm{{<}}\overline{{\tt F}}\textrm{{>}}{\tt m}(% \overline{{\tt e}})$ , where ${\tt e}\longrightarrow{\tt e^{\prime}}$ . $\vdash{\tt e}.{\tt}\textrm{{<}}\overline{{\tt F}}\textrm{{>}}{\tt m}(\overline% {{\tt e}}):[\overline{{\tt F}}/\overline{{\tt Y}}]{\tt T}$ with $\textit{mtype}({\tt m},{\tt C}\textrm{{<}}\overline{{\tt S}}\textrm{{>}})={\tt% }\textrm{{<}}\overline{{\tt Y}}\triangleleft\overline{{\tt U}}\textrm{{>}}% \overline{{\tt T}}\to{\tt T}$ , $\texttt{class}\ {\tt C}\textrm{{<}}\overline{{\tt X}}\triangleleft\overline{{% \tt T^{\prime}}}\textrm{{>}}\{\,\ldots\,\}$ , $\vdash{\tt e}:{\tt E_{0}}$ , $\vdash{\tt E_{0}}\mathbin{\texttt{<:}}{}{\tt C}\textrm{{<}}\overline{{\tt S}}% \textrm{{>}}$ , $\vdash\overline{{\tt S}}\mathbin{\texttt{<:}}{}[\overline{{\tt S}}/\overline{{% \tt X}}]\overline{{\tt T^{\prime}}}$ , $\vdash\overline{{\tt e}}:\overline{{\tt E}}$ , $\vdash\overline{{\tt E}}\mathbin{\texttt{<:}}{}[\overline{{\tt F}}/\overline{{% \tt Y}}]\overline{{\tt T}}$ , $\vdash\overline{{\tt F}}\mathbin{\texttt{<:}}{}[\overline{{\tt F}}/\overline{{% \tt Y}}]\overline{{\tt U}}$ by T-Invk. $\vdash{\tt e^{\prime}}:{\tt E^{\prime}_{0}}$ with $\vdash{\tt E^{\prime}_{0}}\mathbin{\texttt{<:}}{}{\tt E_{0}}$ by induction hypothesis and $\vdash{\tt E^{\prime}_{0}}\mathbin{\texttt{<:}}{}{\tt C}\textrm{{<}}\overline{% {\tt S}}\textrm{{>}}$ by S-Trans. By T-Invk we get $\vdash{\tt e^{\prime}}.{\tt}\textrm{{<}}\overline{{\tt F}}\textrm{{>}}{\tt m}(% \overline{{\tt e}}):[\overline{{\tt F}}/\overline{{\tt Y}}]{\tt T}$ as desired.
Case: C-Invk-Param ${\tt v}.{\tt}\textrm{{<}}\overline{{\tt F}}\textrm{{>}}{\tt m}(\overline{{\tt v% }},{\tt e},\overline{{\tt e}})\longrightarrow{\tt v}.{\tt}\textrm{{<}}% \overline{{\tt F}}\textrm{{>}}{\tt m}(\overline{{\tt v}},{\tt e^{\prime}},% \overline{{\tt e}})$ . This case is similar to C-Invk: We have ${\tt v}.{\tt}\textrm{{<}}\overline{{\tt F}}\textrm{{>}}{\tt m}(\overline{{\tt v% }},{\tt e},\overline{{\tt e}})$ by T-Invk and $\vdash{\tt e^{\prime}}:{\tt E^{\prime}_{0}}$ with $\vdash{\tt E^{\prime}_{0}}\mathbin{\texttt{<:}}{}{\tt E_{0}}$ or $\vdash{\tt E^{\prime}_{0}}={\tt E_{0}}$ by induction hypothesis. In both cases ${\tt v}.{\tt}\textrm{{<}}\overline{{\tt F}}\textrm{{>}}{\tt m}(\overline{{\tt v% }},{\tt e^{\prime}},\overline{{\tt e}})$ by T-Invk finishing the case.
Case: C-New: Analogous to C-Invk-Param.
Case: R-Null-Field. No reduction.
Case: R-Null-Invk. No reduction.
Case: C-Cast $({\tt T}){\tt e}\longrightarrow({\tt T}){\tt e^{\prime}}$ . $\vdash{\tt e}:{\tt E}$ by T-AnyCast. We know ${\tt e^{\prime}}:{\tt E^{\prime}}$ by i.h. where either ${\tt E^{\prime}}={\tt E}$ or ${\tt E^{\prime}}\mathbin{\texttt{<:}}{}{\tt E}$ . In both cases $\vdash({\tt T}){\tt e^{\prime}}:{\tt T}$ by T-AnyCast finishing the case.
Case: R-Upcast $({\tt T})({\tt new}\ {\tt N}(\overline{{\tt v}}))\longrightarrow({\tt new}\ {% \tt N}(\overline{{\tt v}}))$ with $\vdash({\tt T})({\tt new}\ {\tt N}(\overline{{\tt v}})):{\tt T}$ . We know $\vdash{\tt new}\ {\tt N}(\overline{{\tt v}}):{\tt N}$ by T-New and we get $\vdash{\tt N}\mathbin{\texttt{<:}}{}{\tt T}$ by the premise of R-Upcast finishing the case.
Case: R-Cast-Exception. No reduction.
Case: Err-Field, Err-New, Err-Invk, Err-Invk-Param, Err-Cast. No reduction.

$\hfill\blacktriangleleft$

Theorem 13 (Progress).

If $\vdash{\tt e}:{\tt E}$ then either ${\tt e}$ is a value or ${\tt e}\longrightarrow{\tt e^{\prime}}$ , for some ${\tt e^{\prime}}$ , or ${\tt e}\ {\tt err}$ .

Proof.

By induction over the typing derivation.

Case: T-Var cannot occur ( $\Gamma=\emptyset$ )
Case: T-New: By premise of T-New we have $\vdash\overline{{\tt e}}:\overline{{\tt E}}$ and either every ${\tt e}$ in $\overline{{\tt e}}$ is a value or we can apply C-New or Err-New by induction hypothesis.
Case: T-Field ${\tt e}={\tt e_{0}}.{\tt f}_{i}$ : Either ${\tt e_{0}}$ is a value ${\tt e_{0}}={\tt new}\ {\tt N^{\prime}}(\overline{{\tt v}})$ with $\vdash{\tt N^{\prime}}\mathbin{\texttt{<:}}{}{\tt N}$ and $\textit{fields}({\tt N^{\prime}})=\overline{{\tt T}}\ \overline{{\tt f}},% \overline{{\tt T^{\prime}}}\ \overline{{\tt g}}$ by lemma 10 then we can apply R-Field. Otherwise we have $\vdash{\tt e_{0}}:{\tt E}$ by premise of T-Field and therefore either a reduction ${\tt e_{0}}\longrightarrow{\tt e^{\prime}_{0}}$ or we can apply Err-Field and get ${\tt e_{0}}\ {\tt err}$ by induction hypothesis.
Case: T-Invk ${\tt e}={\tt e_{0}}.{\tt}\textrm{{<}}\overline{{\tt F}}\textrm{{>}}{\tt m}(% \overline{{\tt v}},{\tt e_{p}},\overline{{\tt e}})$ : Either ${\tt e_{0}}\longrightarrow{\tt e^{\prime}_{0}}$ because of $\vdash{\tt e_{0}}:{\tt E}$ and induction hypothesis and we can apply C-Invk. Or the same for ${\tt e_{p}}\longrightarrow{\tt e^{\prime}_{p}}$ and we can apply C-Invk-Param. If ${\tt e_{0}}={\tt e^{\prime}_{0}}\ {\tt err}$ we can apply Err-Invk and if ${\tt e_{p}}={\tt e^{\prime}_{p}}\ {\tt err}$ we can apply Err-Invk-Param. Otherwise ${\tt e}=({\tt new}\ {\tt N}(\overline{{\tt e^{\prime}}})).{\tt}\textrm{{<}}% \overline{{\tt F}}\textrm{{>}}{\tt m}(\overline{{\tt v}})$ : By T-Invk we get $\textit{mtype}({\tt m},{\tt N^{\prime}})={\tt}\textrm{{<}}\overline{{\tt Y}}% \triangleleft\overline{{\tt U}^{\prime}}\textrm{{>}}\overline{{\tt T}}\to{\tt T}$ with $\vdash{\tt N}\mathbin{\texttt{<:}}{}{\tt N^{\prime}}$ . By definition of override $\textit{mtype}({\tt m},{\tt N})=\textit{mtype}({\tt m},{\tt N^{\prime}})$ and therefore $\textit{mbody}({\tt m}{\tt}\textrm{{<}}\overline{{\tt F}}\textrm{{>}},{\tt N})% =\overline{{\tt x}}.\overline{{\tt e^{\prime}}}$ where $\overline{{\tt x}}$ has the same length as $\overline{{\tt e}}$ and we can apply R-Invk.
Case: T-UCast $\vdash({\tt T}){\tt e}:{\tt T}$ . Either we have $\vdash{\tt e}:{\tt E}$ then C-Cast can be applied or we have $\vdash{\tt v}:{\tt E}$ and we can apply R-Upcast, because we have ${\tt E}\mathbin{\texttt{<:}}{}{\tt T}$ by T-UCast. For the error case ${\tt e}={\tt e^{\prime}}\ {\tt err}$ we can apply Err-Cast.
Case: T-AnyCast $\vdash({\tt T}){\tt e}:{\tt T}$ . Same as for T-UCast except that for the case that we have $\vdash{\tt v}:{\tt E}$ with $\vdash{\tt E}\nless:{\tt T}$ we have to apply R-Cast-Exception and end up with ${\tt v}\ {\tt err}$ .
Case: R-Null-Field, R-Null-Invk, R-Cast-Exception, Err-Field, Err-New, Err-Invk, Err-Invk-Param, Err-Cast all lead to ${\tt e}\ {\tt err}$ .

$\hfill\blacktriangleleft$

5 Practical Evaluation

As discussed earlier, the Java-TX type system deliberately supports only a subset of Java, because certain method calls can only be type-checked using Java’s specific implementation of wildcards with capture conversion. Thus we consider the following research question for our evaluation: if we take an existing, well-typed Java program and remove all type annotations, can the Java-TX global type inference algorithm find a typing derivation? And if not, how often does it fail in real-world projects?

As no full-fledged compiler for Java-TX is available, yet, we cannot hope for a precise answer, but perform an experiment that provides an approximate answer. To this end, we compare Java-TX to existing formal models of Java with wildcards (e.g., [3, 18, 4]) and identify two principal points of divergence: (1) generic method invocations involving wildcard types, and (2) field declarations that include doubly nested generic type variables (like ${\tt Box}\textrm{{<}}{\tt Box}\textrm{{<}}\,\underline{{\tt X}}\,\textrm{{>}}% \textrm{{>}}$ in Figure 12). We will illustrate both points with concrete examples:

⬇

<X> List<List<X>> make2DList(List<X> from){ ... }

<X> List<List<X>> shuffle2DList(List<List<X>> l){ ... }

List<?> input = ...;

shuffle2DList(make2DList(input));

Figure 11: Code snippet incompatible with Java-TX, but accepted by Java.

⬇

class NestedFields<X extends X> {

Box<Box<X>> f; // X nested two levels deep -> X must be reflexive

}

NestedFields<?> nf = ...; // Not possible in Java-TX

Figure 12: Illicit type annotation, due to nested generics inside class body.

1.

Figure 11 shows a method call which is rejected by Java-TX. In Java, the method call to shuffle2DList(make2DList(input)) is made possible by utilizing Capture Conversion. Although the variable input has type List<?>, the Java compiler implicitly introduces a fresh type variable Cap#1 to capture the wildcard at the call site of make2DList. This process replaces the wildcard type List<?> with the concrete but locally bound type List<Cap#1>. The method make2DList then returns a value of type List<List<Cap#1>>. When this return value is passed as an argument to shuffle2DList, the type parameter X of the method can be instantiated with the captured type variable Cap#1, rendering the composed call typeable.
2.

Java-TX’s type system requires some class parameters to be reflexive as discussed in Section 3.3 example 5. For instance, the field declaration f in the class NestedFields, shown in Figure 12, demands a reflexive type parameter X. In consequence, a type annotation like ${\tt NestedFields}\textrm{{<}}{\tt?}\textrm{{>}}$ is invalid in Java-TX.

To estimate how applicable Java-TX would be in practice, we investigate how often these two situations occur in existing Java code. For this purpose, we conduct an empirical study using a modified OpenJDK compiler that logs 1. capture-conversion events and 2. nested field types as explained. To obtain a safe approximation, we assume that every method call involving capture conversion cannot be handled by Java-TX and we assume the same for every occurrence of nested fields. In consequence, our measurements may overestimate the number of cases that actually cause problems for Java-TX. The details of this approximation are described in Section 5.1, the instrumentation and experimental setup are outlined in Section 5.2, and the quantitative findings are presented in Section 5.3.

5.1 The Good, the Bad, and the Ugly

The Java projects we studied contain three types of wildcard use cases: those that are compatible with the Java-TX type system, those that are certainly not, and those we cannot classify.

Calls to methods that are not generic, such as the one in Figure 13, are fully compatible with Java-TX. On the other hand, method calls like the one in Figure 14 are not possible in Java-TX, because the generic type variable X is used in a reflexive way within the method body. The third variant is the call shown in Figure 15, which is in fact valid in Java-TX, since the method’s type parameter X is not reflexive. Unfortunately, our evaluation cannot distinguish between the second and the third case, which is why we conservatively treat all uncertain cases as incompatible with Java-TX. E.g. both method calls shown in Figure 14 and Figure 15 are counted as invalid even though the last one is supported by Java-TX.

Determining whether a generic type variable in a given Java method must be reflexive would require a full implementation of the Java-TX type checker for the entire Java language. This implementation is not yet available, hence we approximate this behavior by logging all method invocations that use capture conversion. We then conservatively classify only method calls to non-generic methods as valid and all others as invalid.

⬇

List<?> m(List<?> l){ // non-generic method

return l;

}

List<?> l = ...;

m(l); // accepted in Java and Java-TX

Figure 13: Method call accepted by Java and Java-TX.

⬇

// <X extends X> would be required by Java-TX:

<X> List<X> sort(List<X> l){

return l.add(l.get(0));

}

List<?> l = ...;

sort(l); //type-error!

Figure 14: Method call rejected by Java-TX, but accepted by Java’s type system.

⬇

1<X> // X is not reflexive

2List<X> sort(List<X> l){

3 return l;

4}

5

6List<?> l = ...;

7sort(l); // accepted!

Figure 15: Method call accepted by Java-TX, but counted as invalid.

Similar to the approximation for method calls, we also approximate Java-TX’s restrictions on field declarations. We check class definitions for nested type variables and mark those fields as incompatible with Java-TX. Every type variable that appears anywhere other than in the topmost parameter list of a field type is counted as unsupported. Thus, a field like f in Figure 12 would be considered illegal by our evaluation. This provides a pessimistic, upper-bound approximation of the T-Field rule, formalized by Lemma 14, which states that every field type with no doubly nested generic type parameters poses no problem for the Java-TX type system.

Lemma 14.

A field with type ${\tt C}\textrm{{<}}\overline{{\tt E}}\textrm{{>}}$ containing type variables only in $\overline{{\tt E}}$ but not in any nested type parameter lists is a valid field type according to the rule T-Field.

If: ${\tt D}\textrm{{<}}\overline{{\tt E}}\textrm{{>}}$ where $\forall{\tt E}\in\overline{{\tt E}}:$ ${\tt E}$ either is ${\tt X}$ or a wildcard ${\tt W}$ or a type ${\tt N}$ with $\textit{fv}({\tt W})=\emptyset$ , $\textit{fv}({\tt N})=\emptyset$
Then: $\forall\overline{{\tt E_{1}}}\ \forall\overline{{\tt E_{2}}}\in\{\,\overline{{% \tt E_{1}}}\mid\ \emptyset\vdash{\tt C}\textrm{{<}}\overline{{\tt E_{1}}}% \textrm{{>}}\mathbin{\texttt{<:}}{}{\tt C}\textrm{{<}}\overline{{\tt E_{2}}}% \textrm{{>}}\,\}:[\overline{{\tt E}_{1}}/\overline{{\tt X}}]{\tt D}\textrm{{<}% }\overline{{\tt E}}\textrm{{>}}\mathbin{\texttt{<:}}[\overline{{\tt E}_{2}}/% \overline{{\tt X}}]{\tt D}\textrm{{<}}\overline{{\tt E}}\textrm{{>}}$

Proof.

We will show $\forall\overline{{\tt E_{1}}}\ \forall\overline{{\tt E_{2}}}\in\{\,\overline{{% \tt E_{1}}}\mid\ \emptyset\vdash{\tt C}\textrm{{<}}\overline{{\tt E_{1}}}% \textrm{{>}}\mathbin{\texttt{<:}}{}{\tt C}\textrm{{<}}\overline{{\tt E_{2}}}% \textrm{{>}}\,\}:\forall{\tt E}\in\overline{{\tt E}}:\ \emptyset\vdash[% \overline{{\tt E}_{1}}/\overline{{\tt X}}]{\tt E}\textrm{$\,\lessdot_{?}\,$}[% \overline{{\tt E}_{2}}/\overline{{\tt X}}]{\tt E}$ which implies $\forall\overline{{\tt E_{1}}}\ \forall\overline{{\tt E_{2}}}\in\{\,\overline{{% \tt E_{1}}}\mid\ \emptyset\vdash{\tt C}\textrm{{<}}\overline{{\tt E_{1}}}% \textrm{{>}}\mathbin{\texttt{<:}}{}{\tt C}\textrm{{<}}\overline{{\tt E_{2}}}% \textrm{{>}}\,\}:[\overline{{\tt E}_{1}}/\overline{{\tt X}}]{\tt N}\mathbin{% \texttt{<:}}[\overline{{\tt E}_{2}}/\overline{{\tt X}}]{\tt N}$ by S-WC-Class.

Case: ${\tt E}={\tt X}$ then $[\overline{{\tt E}_{1}}/\overline{{\tt X}}]{\tt X}\textrm{$\,\lessdot_{?}\,$}[% \overline{{\tt E}_{2}}/\overline{{\tt X}}]{\tt X}$ is the same as $\emptyset\vdash{\tt E_{1}}\textrm{$\,\lessdot_{?}\,$}{\tt E_{2}}$ . We have $\emptyset\vdash{\tt C}\textrm{{<}}\overline{{\tt E_{1}}}\textrm{{>}}\mathbin{% \texttt{<:}}{}{\tt C}\textrm{{<}}\overline{{\tt E_{2}}}\textrm{{>}}$ by hypothesis which requires $\emptyset\vdash\overline{{\tt E_{1}}}\textrm{$\,\lessdot_{?}\,$}\overline{{\tt E% _{2}}}$ by S-WC-Class finishing the case.
Case: ${\tt E}=\text{{\tt?}}^{{\tt U}}_{{\tt L}}$ and $[\overline{{\tt E}_{1}}/\overline{{\tt X}}]\text{{\tt?}}^{{\tt U}}_{{\tt L}}=[% \overline{{\tt E}_{2}}/\overline{{\tt X}}]\text{{\tt?}}^{{\tt U}}_{{\tt L}}$ , because $\textit{fv}(\text{{\tt?}}^{{\tt U}}_{{\tt L}})=\emptyset$ . USV-Extends and S-Refl finishing the case.
Case: ${\tt E}={\tt D^{\prime}}\textrm{{<}}\overline{{\tt E^{\prime}}}\textrm{{>}}$ and $[\overline{{\tt E}_{1}}/\overline{{\tt X}}]{\tt D^{\prime}}\textrm{{<}}% \overline{{\tt E^{\prime}}}\textrm{{>}}=[\overline{{\tt E}_{2}}/\overline{{\tt X% }}]{\tt D^{\prime}}\textrm{{<}}\overline{{\tt E^{\prime}}}\textrm{{>}}$ , because $\textit{fv}({\tt D^{\prime}}\textrm{{<}}\overline{{\tt E^{\prime}}}\textrm{{>}% })=\emptyset$ . USV-Equals and S-Refl finishing the case.

$\hfill\blacktriangleleft$

5.2 Method

To perform this evaluation, we modify the Java Compiler to output information about every capture conversion that occurs during compilation. We take the compiler from the current Java implementation (JDK 24) of the OpenJDK project (https://openjdk.org/) and use it to compile open-source software from GitHub (https://github.com/).

We applied the modified compiler to the JDK itself and to a selection of trending Java projects on GitHub²²2https://github.com/trending/java in the time period from September to December 2024. The main criterion for choosing a project is that it compiles with the modified version of the OpenJDK, which means, the project has to be compatible with Java version 24. With this criterion, we ended up with seven open source Java projects compatible with our test setup:³³3Each project name is linked to its GitHub page. graphhopper, nacos, commons-collections, DependencyCheck, maven, Algorithms-Java, commons-lang.

The biggest code base was OpenJDK’s Java Development Kit⁴⁴4https://github.com/openjdk/jdk with over six million lines of Java code. The seven open source projects gathered from GitHub amount to a total of around seven hundred thousand lines of Java source code (measured with cloc⁵⁵5https://github.com/AlDanial/cloc).

5.3 Result

Table 1 shows the number of method calls and the number of calls involving capture conversion in the code base. The invalid column shows the number of method calls that involve capture conversion and call a generic method.

Table 1: Method calls involving capture conversion.

Project	Method Calls	with CC	invalid in Java-TX
Java Development Kit	778339	8943	2109 (0.27%)
GitHub Projects	107899	1795	903 (0.84%)

Table 2 shows the breakdown in terms of classes: A class that contains at least one (potentially) invalid method call or field declaration is counted as invalid. The idea is that those classes may not be accepted by a type inference algorithm based on Java-TX.

Table 2: Classes that may not type check in Java-TX.

Project	Classes	invalid in Java-TX
Java Development Kit	31831	542 (1.70%)
GitHub Projects	5147	328 (6.37%)

Table 3: Classes with deeply nested field types.

Project	Fields	nested generics	affected classes
Java Development Kit	116717	81 (0.07%)	57 (0.18%)
GitHub Projects	13891	45 (0.32%)	28 (0.54%)

Additionally we looked for field declarations that contain a type variable nested inside multiple layers. For example, the type ${\tt Box}\textrm{{<}}{\tt X}\textrm{{>}}$ contains a type variable X nested inside Box. The nested generics column in Table 3 counts field declarations that contain type variables nested at least two levels deep (e.g. ${\tt Box}\textrm{{<}}{\tt Box}\textrm{{<}}{\tt X}\textrm{{>}}\textrm{{>}}$ ). This is used as the approximation for the T-Field rule (see lemma 14). The affected classes are classes that contain at least one such field declaration.

5.4 Evaluation

The results support our claim that giving up capture conversion for our approach has only a small impact on existing Java code. In the real world projects we considered, around six percent of all classes may be not be compatible with Java-TX. However, we determined an upper limit of method calls which may pose problems for our calculus. Even if a class is counted as invalid, the Java-TX type inference algorithm may still find a typing! Thus, invalid just means that Java-TX may not find the exact same type annotations as the Java compiler. An alternative typing may not involve wildcards or the target method may not use its generic type variables in a reflexive way (cf. Fig. 15), in which case there is no problem.

We also scrutinized the unsupported method calls and found that many of those calls are targeting methods with isolated type variables. The next section 5.6 discusses them further and proposes a practical solution for those methods.

Our evaluation shows that Java-TX type inference is useful in real world source code. In fact, it could be used as an IDE plugin [10] enabling automated type completions and improvements, enabling the programmer to concentrate on providing explicit types for difficult cases involving capture conversion.

5.5 Directions for a More Thorough Evaluation

There are two principal ways to extend our evaluation.

Wider coverage.

Our current approach requires manually running a modified javac compiler on each project. The advantage is that we count actual capture conversion events during the type-checking phase, which gives a precise (if conservative) measure. The downside is that it does not scale easily to a large number of projects. One alternative is to use the Boa infrastructure [5], which provides a query language over the ASTs of millions of open-source Java projects. While Boa cannot count capture conversions directly, it can count user-defined wildcard type annotations and methods with isolated type variables – the latter being a class of method calls that Java-TX can handle as described in Section 5.6. Another alternative is to adapt existing empirical studies on Java wildcards and generics to our use case. For instance, Altidor et al. [1] find that 32% of generic classes have single-variance type parameters and that 37% of existing wildcard uses are rendered unnecessary by their inference algorithm. Single-variance type parameters are compatible with Java-TX, since they do not require reflexivity and can therefore be instantiated with a wildcard. The problematic cases are invariant wildcards, which require use-site variance and depend on capture conversion – precisely the feature that Java-TX does not support.

Finer-grained classification.

Our current approximation counts all method calls involving capture conversion on a generic method as incompatible with Java-TX, without distinguishing where the wildcard types and the called methods originate. Section 5.6 already shows one refinement: pre-typed library methods with isolated type variables can be handled by Java-TX and should not be counted as incompatible. A further refinement is to distinguish between user-defined and library methods, and between wildcard types originating in user code and those returned by library APIs. This distinction matters because the typical use case for Java-TX global type inference is to infer types for user-written code; library code is already fully type-annotated. The incompatibility between capture conversion and Java-TX type inference only arises when neither the types of the method parameters nor the types of the arguments are known to the inference algorithm. Concretely, three categories of call sites are worth distinguishing:

1.

Calls where neither the called method nor the argument types are known – these are the genuinely problematic cases for Java-TX type inference.
2.

Calls where all types are already known (e.g., both method and arguments are from library code) – here the Java type checker resolves the call directly and no type inference is needed.
3.

Calls to user-defined methods where the argument type originates from a library function returning a wildcard – here it may be possible to support the call by applying capture conversion selectively at the boundary between library and user code.

5.6 Calls to Pre-typed Methods with Isolated Type Variables

A type inference algorithm can leverage the fact that external Java code included in a project (e.g., the Java standard library) is already type checked. Generally those methods could be converted to Java-TX by making their type parameters reflexive: <X extends Object> becomes <X extends Object, X extends X>.

⬇

// Pre-Typed Java Libraray

<X> void shuffle(List<X> list){ ... }

⬇

// Typeless Java-TX code:

List<?> anyList = ...;

shuffle(anyList); // accepted

Figure 16: Pre-Typed Method with Isolated Type Variable X, called from Java-TX program.

If a type parameter appears only once in a method header, this conversion can be safely omitted without compromising soundness. For instance, the shuffle method shown in Figure 16 has a type parameter ${\tt X}$ that occurs only once in the method header, namely in the parameter type ${\tt List}\textrm{{<}}{\tt X}\textrm{{>}}$ . In Java this method can be invoked with an argument of type ${\tt List}\textrm{{<}}{\tt?}\textrm{{>}}$ . Therefore we can treat ${\tt X}$ as a non-reflexive type argument in our Java-TX type system while still preserving soundness.

Furthermore we now can look for methods in the Java standard library with a similar pattern and treat their isolated type arguments also as non-reflexive. This allows our approximation to count more method calls as possible in Java-TX. One prominent example is the collect method of the Java Stream API:

class Stream<T> { <R,A> R collect(Collector<? super T,A,R> collector) }

The type parameter A is used only once in the method header. therefore fits our requirements to be eligible for wildcards. The calls to collect using Collectors.toList() as a parameter instantiate A with a wildcard type and were counted as invalid by our evaluation as explained in Section 5.1. But these calls would all be sound under Java-TX’s interpretation of wildcards, due the fact that those calls are invoking a pre-typed method with an isolated type variable.

In total (including JDK source code) we found 10785 uses of capture conversion in method calls of which 3012 are used to call a polymorphic method. So over 70% of method calls utilizing capture conversion are compatible with Java-TX anyway. Using the method proposed in this section we could additionally support 948 of those 3012 incompatible method calls pushing this number to 80% support for method calls using capture conversion.

6 Related Work

Igarashi et al [8] define Featherweight Java and its generic sibling, Featherweight Generic Java. This language is a functional core calculus that embodies the essential ingredients of Java. They develop the full metatheory for FJ and FGJ and study the type erasure transformation used by the Java compiler.

Wildcards are first described in a research paper by Torgersen et al [19]. Subsequently, they propose Wild FJ as an extension of FGJ with wildcards [18], but without any proofs of their formal system. The Java Language Specification [6] refers to Wild FJ for the introduction of wildcards. Cameron et al [4] propose a refined formal model of wildcards based on explicit existential types. They give a soundness proof and a translation of a subset of Java to the formal model. Bierhoff [3] gives a subtly different core calculus with a soundness proof. The motivation for this paper is to show that the unsoundness of Java which was discovered by Amin and Tate [2] is avoidable, even in the absence of a nullness-aware type system.

Altidor et al [1] present a framework which combines use-site variance (wildcards as in Java) and definition-site variance (as in Scala). For instance, it can be used to add use-site variance to Scala and extend the Java type system to infer the definition-site variance.

All these approaches rely on capture conversion to process arguments of wildcard type in calls to generic methods. As in our proposal, subtyping is not reflexive on wildcards in the systems of Cameron et al [4] and Bierhoff [3]. As our calculus instantiates type variables with wildcards, our subtyping relation is not reflexive on type variables. This restriction can be amended with reflexivity constraints, which in turn rule out instantiation with wildcards to retain soundness.

The type inference algorithm of Java-TX [13] treats wildcards similar to our approach. In particular, the subtyping relation is similar to ours. Their main contribution is the algorithm for type inference along with its soundness and completeness proof. Furthermore, Plümicke [15] proposes a similar calculus than considered here, but its soundness is not considered.

7 Summary and Outlook

This paper introduced the calculus FJ-TX, a core calculus for the language Java-TX. The calculus is based on a novel approach to deal with wildcards. Contrary to the mainstream approach, which is implemented in the Java compiler, our calculus avoids the notion of capture conversion. This design choice enables us to treat wildcards like any other type, instantiate type variables with wildcards, and thus support global type inference. Our approach is implemented in the Java-TX compiler.

Both approaches guarantee soundness of using wildcards in combination with generic types. As we have shown in Section 2.3, our approach accepts some programs that are rejected by capture conversion and vice versa. Further research and experimentation is needed to investigate which approach is more manageable and intuitive in practice. For some programmers the restriction that subtyping is not reflexive on type variables might not be intuitive. However, type inference of Java-TX will silently insert the additional reflexivity constraints without programmer interaction. For others the concept of capture conversion with its complex error messages may be confusing.

References

[1] John Altidor, Shan Shan Huang, and Yannis Smaragdakis. Taming the wildcards: combining definition- and use-site variance. In Mary W. Hall and David A. Padua, editors, Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011, pages 602–613. ACM, 2011. doi:10.1145/1993498.1993569.
[2] Nada Amin and Ross Tate. Java and Scala’s type systems are unsound: the existential crisis of null pointers. In Eelco Visser and Yannis Smaragdakis, editors, OOPSLA 2016, pages 838–848. ACM, 2016. doi:10.1145/2983990.2984004.
[3] Kevin Bierhoff. Wildcards need witness protection. Proc. ACM Program. Lang., 6(OOPSLA2), 2022. doi:10.1145/3563301.
[4] Nicholas Cameron, Sophia Drossopoulou, and Erik Ernst. A model for Java with wildcards. ECOOP 2008 - Object-Oriented Programming, 22nd European Conference, Paphos, Cyprus, July 7-11, 2008, Proceedings, 5142:2–26, 2008. doi:10.1007/978-3-540-70592-5_2.
[5] Robert Dyer, Hridesh Rajan, Hoan Anh Nguyen, and Tien N. Nguyen. Mining billions of AST nodes to study actual and potential usage of Java language features. In Proceedings of the 36th International Conference on Software Engineering, ICSE 2014, Hyderabad, India, May 31 – June 7, 2014, pages 779–790. ACM, 2014. doi:10.1145/2568225.2568295.
[6] James Gosling, Bill Joy, Guy Steele, Gilad Bracha, Alex Buckley, and Daniel Smith. The Java^® Language Specification. Addison-Wesley, Java SE 21 edition, 2023. URL: https://docs.oracle.com/javase/specs/jls/se21/jls21.pdf.
[7] Atsushi Igarashi, Benjamin Pierce, and Philip Wadler. Featherweight Java: A minimal core calculus for Java and GJ. Proceedings of the ACM SIGPLAN Conference OOPSLA, 1999.
[8] Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: a minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems (TOPLAS), 23(3):396–450, 2001. doi:10.1145/503502.503505.
[9] Ameya Ketkar, Nikolaos Tsantalis, and Danny Dig. Understanding type changes in Java. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2020, pages 629–641, New York, NY, USA, 2020. Association for Computing Machinery. doi:10.1145/3368089.3409725.
[10] Ruben Kraft and Martin Plümicke. Ein Language-Server für Java-TX. In Stefan Brunthaler, editor, 23. Kolloquium Programmiersprachen und Grundlagen der Programmierung – Vorläufiger Tagungsband. Universität der Bundeswehr München, September 2025. (in german).
[11] Stas Negara, Mihai Codoban, Danny Dig, and Ralph E. Johnson. Mining fine-grained code changes to detect unknown change patterns. In Proceedings of the 36th International Conference on Software Engineering, ICSE 2014, pages 803–813, New York, NY, USA, 2014. Association for Computing Machinery. doi:10.1145/2568225.2568317.
[12] Martin Pluemicke. Completing the functional approach in object-oriented languages. In A Second Soul: Celebrating the Many Languages of Programming - Festschrift in Honor of Peter Thiemann’s Sixtieth Birthday, Freiburg, Germany, 30th August 2024, volume 413 of Electronic Proceedings in Theoretical Computer Science, pages 43–56. Open Publishing Association, 2024. doi:10.4204/EPTCS.413.4.
[13] Martin Plümicke. Java type unification with wildcards. In Applications of Declarative Programming and Knowledge Management, 17th International Conference, INAP 2007, and 21st Workshop on Logic Programming, WLP 2007, Würzburg, Germany, October 4-6, 2007, Revised Selected Papers, volume 5437 of Lecture Notes in Computer Science, pages 223–240. Springer, 2007. doi:10.1007/978-3-642-00675-3_15.
[14] Martin Plümicke. Optimization of the Java Type Unification. In Sibylle Schwarz and Mario Wenzel, editors, Proceedings of the 37th Workshop on (Constraint) Logic Programming (WLP 2023), 2023. URL: https://dbs.informatik.uni-halle.de/wlp2023/WLP2023_Pl%C3%BCmicke_Optimization%20of%20the%20Java%20Type%20Unification.pdf.
[15] Martin Plümicke. Featherweight-Java-TX: A Minimal Core Calculus for Java-TX (FJ-TX). In Daniel Holle, Jens Knoop, Martin Plümicke, Peter Thiemann, and Baltasar Trancón y Widemann, editors, 40. Workshop der GI-Fachgruppe "Programmiersprachen und Rechenkonzepte", number 02/2024 in INSIGHTS – Schriftenreihe der Fakultät Technik, pages 93–101, Bad Honnef, Germany, April 2024. URL: https://www.dhbw-stuttgart.de/forschung-transfer/technik/schriftenreihe-insights.
[16] Martin Plümicke and Andreas Stadelmeier. Introducing Scala-like function types into Java-TX. In Proceedings of the 14th International Conference on Managed Languages and Runtimes, ManLang 2017, pages 23–34, New York, NY, USA, 2017. ACM. doi:10.1145/3132190.3132203.
[17] Andreas Stadelmeier, Martin Plümicke, and Peter Thiemann. Global Type Inference for Featherweight Generic Java. 36th European Conference on Object-Oriented Programming (ECOOP 2022), 222:28:1–28:27, 2022. doi:10.4230/LIPIcs.ECOOP.2022.28.
[18] Mads Torgersen, Erik Ernst, and Christian Plesner Hansen. Wild FJ. In Philip Wadler, editor, Proceedings of FOOL 12, Long Beach, California, USA, 2012. ACM, School of Informatics, University of Edinburgh. URL: http://homepages.inf.ed.ac.uk/wadler/fool/.
[19] Mads Torgersen, Erik Ernst, Christian Plesner Hansen, Peter von der Ahé, Gilad Bracha, and Neal Gafter. Adding wildcards to the Java programming language. Journal of Object Technology, 3(11):97–116, December 2004. doi:10.5381/jot.2004.3.11.a5.

[bib.bib1] [1] John Altidor, Shan Shan Huang, and Yannis Smaragdakis. Taming the wildcards: combining definition- and use-site variance. In Mary W. Hall and David A. Padua, editors, Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011, pages 602–613. ACM, 2011. doi:10.1145/1993498.1993569.

[bib.bib2] [2] Nada Amin and Ross Tate. Java and Scala’s type systems are unsound: the existential crisis of null pointers. In Eelco Visser and Yannis Smaragdakis, editors, OOPSLA 2016, pages 838–848. ACM, 2016. doi:10.1145/2983990.2984004.

[bib.bib3] [3] Kevin Bierhoff. Wildcards need witness protection. Proc. ACM Program. Lang., 6(OOPSLA2), 2022. doi:10.1145/3563301.

[bib.bib4] [4] Nicholas Cameron, Sophia Drossopoulou, and Erik Ernst. A model for Java with wildcards. ECOOP 2008 - Object-Oriented Programming, 22nd European Conference, Paphos, Cyprus, July 7-11, 2008, Proceedings, 5142:2–26, 2008. doi:10.1007/978-3-540-70592-5_2.

[bib.bib5] [5] Robert Dyer, Hridesh Rajan, Hoan Anh Nguyen, and Tien N. Nguyen. Mining billions of AST nodes to study actual and potential usage of Java language features. In Proceedings of the 36th International Conference on Software Engineering, ICSE 2014, Hyderabad, India, May 31 – June 7, 2014, pages 779–790. ACM, 2014. doi:10.1145/2568225.2568295.

[bib.bib6] [6] James Gosling, Bill Joy, Guy Steele, Gilad Bracha, Alex Buckley, and Daniel Smith. The Java^® Language Specification. Addison-Wesley, Java SE 21 edition, 2023. URL: https://docs.oracle.com/javase/specs/jls/se21/jls21.pdf.

[bib.bib7] [7] Atsushi Igarashi, Benjamin Pierce, and Philip Wadler. Featherweight Java: A minimal core calculus for Java and GJ. Proceedings of the ACM SIGPLAN Conference OOPSLA, 1999.

[bib.bib8] [8] Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: a minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems (TOPLAS), 23(3):396–450, 2001. doi:10.1145/503502.503505.

[bib.bib9] [9] Ameya Ketkar, Nikolaos Tsantalis, and Danny Dig. Understanding type changes in Java. In Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2020, pages 629–641, New York, NY, USA, 2020. Association for Computing Machinery. doi:10.1145/3368089.3409725.

[bib.bib10] [10] Ruben Kraft and Martin Plümicke. Ein Language-Server für Java-TX. In Stefan Brunthaler, editor, 23. Kolloquium Programmiersprachen und Grundlagen der Programmierung – Vorläufiger Tagungsband. Universität der Bundeswehr München, September 2025. (in german).

[bib.bib11] [11] Stas Negara, Mihai Codoban, Danny Dig, and Ralph E. Johnson. Mining fine-grained code changes to detect unknown change patterns. In Proceedings of the 36th International Conference on Software Engineering, ICSE 2014, pages 803–813, New York, NY, USA, 2014. Association for Computing Machinery. doi:10.1145/2568225.2568317.

[bib.bib12] [12] Martin Pluemicke. Completing the functional approach in object-oriented languages. In A Second Soul: Celebrating the Many Languages of Programming - Festschrift in Honor of Peter Thiemann’s Sixtieth Birthday, Freiburg, Germany, 30th August 2024, volume 413 of Electronic Proceedings in Theoretical Computer Science, pages 43–56. Open Publishing Association, 2024. doi:10.4204/EPTCS.413.4.

[bib.bib13] [13] Martin Plümicke. Java type unification with wildcards. In Applications of Declarative Programming and Knowledge Management, 17th International Conference, INAP 2007, and 21st Workshop on Logic Programming, WLP 2007, Würzburg, Germany, October 4-6, 2007, Revised Selected Papers, volume 5437 of Lecture Notes in Computer Science, pages 223–240. Springer, 2007. doi:10.1007/978-3-642-00675-3_15.

[bib.bib14] [14] Martin Plümicke. Optimization of the Java Type Unification. In Sibylle Schwarz and Mario Wenzel, editors, Proceedings of the 37th Workshop on (Constraint) Logic Programming (WLP 2023), 2023. URL: https://dbs.informatik.uni-halle.de/wlp2023/WLP2023_Pl%C3%BCmicke_Optimization%20of%20the%20Java%20Type%20Unification.pdf.

[bib.bib15] [15] Martin Plümicke. Featherweight-Java-TX: A Minimal Core Calculus for Java-TX (FJ-TX). In Daniel Holle, Jens Knoop, Martin Plümicke, Peter Thiemann, and Baltasar Trancón y Widemann, editors, 40. Workshop der GI-Fachgruppe "Programmiersprachen und Rechenkonzepte", number 02/2024 in INSIGHTS – Schriftenreihe der Fakultät Technik, pages 93–101, Bad Honnef, Germany, April 2024. URL: https://www.dhbw-stuttgart.de/forschung-transfer/technik/schriftenreihe-insights.

[bib.bib16] [16] Martin Plümicke and Andreas Stadelmeier. Introducing Scala-like function types into Java-TX. In Proceedings of the 14th International Conference on Managed Languages and Runtimes, ManLang 2017, pages 23–34, New York, NY, USA, 2017. ACM. doi:10.1145/3132190.3132203.

[bib.bib17] [17] Andreas Stadelmeier, Martin Plümicke, and Peter Thiemann. Global Type Inference for Featherweight Generic Java. 36th European Conference on Object-Oriented Programming (ECOOP 2022), 222:28:1–28:27, 2022. doi:10.4230/LIPIcs.ECOOP.2022.28.

[bib.bib18] [18] Mads Torgersen, Erik Ernst, and Christian Plesner Hansen. Wild FJ. In Philip Wadler, editor, Proceedings of FOOL 12, Long Beach, California, USA, 2012. ACM, School of Informatics, University of Edinburgh. URL: http://homepages.inf.ed.ac.uk/wadler/fool/.

[bib.bib19] [19] Mads Torgersen, Erik Ernst, Christian Plesner Hansen, Peter von der Ahé, Gilad Bracha, and Neal Gafter. Adding wildcards to the Java programming language. Journal of Object Technology, 3(11):97–116, December 2004. doi:10.5381/jot.2004.3.11.a5.