Section 32.1 describes support for Java generics (also known as “parametric polymorphism”). Section 32.2 describes polymorphism over type qualifiers for methods. Section 32.3 describes polymorphism over type qualifiers for classes.
The Checker Framework fully supports type-qualified Java generic types and methods (also known as “parametric polymorphism”). When instantiating a generic type, clients supply the qualifier along with the type argument, as in List<@NonNull String>. When using a type variable
T within the implementation of a generic type, typically no type qualifier is written (see Section 32.1.3); rather, the instantiation of the type parameter is restricted (see Section 32.1.2).
Before running any pluggable type-checker, we recommend that you eliminate raw types from your code (e.g., your code should use List<...> as opposed to List). Your code should compile without warnings when using the standard Java compiler and the
-Xlint:unchecked -Xlint:rawtypes command-line options. Using generics helps prevent type errors just as using a pluggable type-checker does, and makes the Checker Framework’s warnings easier to understand.
If your code uses raw types, then the Checker Framework will do its best to infer the Java type arguments and the type qualifiers. By default, these inferred types are ignored in subtyping checks. If you supply the command-line option -AignoreRawTypeArguments=false, you will see errors from raw
types.
When you define a generic class in Java, the extends clause of the generic type parameter (known as the “upper bound”) requires that the corresponding type argument must be a subtype of the bound. For example, given the definition class G<T extends Number> {...}, the upper bound is Number and a client can instantiate it as G<Number> or G<Integer> but not G<Date>.
You can write a type qualifier on the extends clause to make the upper bound a qualified type. For example, you can declare that a generic list class can hold only non-null values:
class MyList<T extends @NonNull Object> {...}
MyList<@NonNull String> m1; // OK
MyList<@Nullable String> m2; // error
That is, in the above example, all arguments that replace T in MyList<T> must be subtypes of @NonNull Object.
Conceptually, each generic type parameter has two bounds — a lower bound and an upper bound — and at instantiation, the type argument must be within the bounds. Java only allows you to specify the upper bound; the lower bound is implicitly the bottom type void. The Checker Framework gives
you more power: you can specify both an upper and lower bound for type parameters. Write the upper bound on the extends clause, and write the lower bound on the type variable.
class MyList<@LowerBound T extends @UpperBound Object> { ... }
You may omit either the upper or the lower bound, and the Checker Framework will use a default.
For a discussion of wildcards, see Section 32.1.4.
For a concrete example, consider the type system of the Regex Checker (see Figure 14.1) in which @Regex(0) :> @Regex(1) :> @Regex(2) :>
@Regex(3) :> ….
class MyRegexes<@Regex(5) T extends @Regex(1) String> { ... }
MyRegexes<@Regex(0) String> mu; // error - @Regex(0) is not a subtype of @Regex(1)
MyRegexes<@Regex(1) String> m1; // OK
MyRegexes<@Regex(3) String> m3; // OK
MyRegexes<@Regex(5) String> m5; // OK
MyRegexes<@Regex(6) String> m6; // error - @Regex(6) is not a supertype of @Regex(5)
The above declaration states that the upper bound of the type variable is @Regex(1) String and the lower bound is @Regex(5) void. That is, arguments that replace T in MyRegexes<T> must be subtypes of @Regex(1) String and
supertypes of @Regex(5) void. Since void cannot be used to instantiate a generic class, MyRegexes may be instantiated with @Regex(1) String through @Regex(5) String.
To specify an exact bound, place the same annotation on both bounds. For example:
class MyListOfNonNulls<@NonNull T extends @NonNull Object> { ... }
class MyListOfNullables<@Nullable T extends @Nullable Object> { ... }
MyListOfNonNulls<@NonNull Number> v1; // OK
MyListOfNonNulls<@Nullable Number> v2; // error
MyListOfNullables<@NonNull Number> v4; // error
MyListOfNullables<@Nullable Number> v3; // OK
It is an error if the lower bound is not a subtype of the upper bound.
class MyClass<@Nullable T extends @NonNull Object> // error: @Nullable is not a subtype of @NonNull
A generic type parameter or wildcard is written as class MyClass<@LowerBound T extends @UpperBound JavaUpperBound> or as MyClass<@UpperBound ? super @LowerBound JavaLowerBound>, where
“@LowerBound” and “@UpperBound” are type qualifiers.
For lower bounds: If no type annotation is written in front of ?, then the lower bound defaults to @BottomType void.
For upper bounds:
• If the extends clause is omitted, then the upper bound defaults to @TopType Object.
• If the extends clause is written but contains no type qualifier, then the normal defaulting rules apply to the type in the extends clause (see Section 33.5.3).
The upper-bound rules mean that even though in Java the following two declarations are equivalent:
class MyClass<T>
class MyClass<T extends Object>
they specify different type qualifiers on the upper bound, if the type system’s default annotation is not its top annotation.
The Nullness type system is an example.
class MyClass<T> == class MyClass<T extends @Nullable Object>
class MyClass<T extends Object> == class MyClass<T extends @NonNull Object>
The rationale for this choice is:
• The “<T>” in MyClass<T> means “fully unconstrained”, and the rules maintain that, without the need for a programmer to change existing code.
• The “Object” in MyClass<T extends Object> is treated exactly like every other occurrence of Object in the program — it would be confusing for different occurrences of Object to mean different annotated types.
Here are some style guidelines:
• Use “<T>” when there are no constraints on the type qualifiers. This is short and is what already appears in source code.
• Whenever you write an extends clause, write an explicit type annotation on it. For example, for the Nullness Checker, write class MyClass<T> rather than class MyClass<T extends @Nullable Object>, and write class MyClass<T extends
@NonNull Object> rather than class MyClass<T extends Object>.
For further discussion, see Section 40.7.2.
A type annotation on a use of a generic type variable overrides/ignores any type qualifier (in the same type hierarchy) on the corresponding actual type argument. For example, suppose that T is a formal type parameter. Then using @Nullable T within the scope of T applies
the type qualifier @Nullable to the (unqualified) Java type of T. This feature is sometimes useful, but more often the implementation of a generic type just uses the type variable T, whose instantiation is restricted (see Section 32.1.2).
Here is an example of applying a type annotation to a generic type variable:
class MyClass2<T> {
...
@Nullable T myField = null;
...
}
The type annotation does not restrict how MyClass2 may be instantiated. In other words, both MyClass2<@NonNull String> and MyClass2<@Nullable String> are legal, and in both cases @Nullable T means @Nullable String. In
MyClass2<@Interned String>, @Nullable T means @Nullable @Interned String.
Defaulting never affects a use of a type variable, even if the type variable use has no explicit annotation. Defaulting helps to choose a single type qualifier for a concrete Java class or interface. By contrast, a type variable use represents a set of possible types.
At an instantiation of a generic type, a Java wildcard indicates that some constraints are known on the type argument, but the type argument is not known exactly. For example, you can indicate that the type parameter for variable ls is some unknown subtype of CharSequence:
List<? extends CharSequence> ls;
ls = new ArrayList<String>(); // OK
ls = new ArrayList<Integer>(); // error: Integer is not a subtype of CharSequence
For more details about wildcards, see the Java tutorial on wildcards or JLS §4.5.1.
You can write a type annotation on the bound of a wildcard:
List<? extends @NonNull CharSequence> ls;
ls = new ArrayList<@NonNull String>(); // OK
ls = new ArrayList<@Nullable String>(); // error: @Nullable is not a subtype of @NonNull
Conceptually, every wildcard has two bounds — an upper bound and a lower bound. Java only permits you to write one bound. You can specify the upper bound with <? extends SomeType>, in which case the lower bound is implicitly the bottom type void. You can specify the
lower bound with <? super OtherType>, in which case the upper bound is implicitly the top type Object. The Checker Framework is more flexible: it lets you similarly write annotations on both the upper and lower bound.
To annotate the implicit bound, write the type annotation before the ?. For example:
List<@LowerBound ? extends @UpperBound CharSequence> lo;
List<@UpperBound ? super @NonNull Number> ls;
For an unbounded wildcard (<?>, with neither bound specified), the annotation in front of a wildcard applies to both bounds. The following three declarations are equivalent (except that you cannot write the bottom type void; note that Void does not denote the bottom type):
List<@NonNull ?> lnn;
List<@NonNull ? extends @NonNull Object> lnn;
List<@NonNull ? super @NonNull void> lnn;
Note that the annotation in front of a type parameter always applies to its lower bound, because type parameters can only be written with extends and never super.
The defaulting rules for wildcards also differ from those of type parameters (see Section 33.5.5).
Recall that @Nullable X is a supertype of @NonNull X, for any X. Most of the following types mean different things:
class MyList1<@Nullable T> { ... }
class MyList1a<@Nullable T extends @Nullable Object> { ... } // same as MyList1
class MyList2<@NonNull T extends @NonNull Object> { ... }
class MyList2a<T extends @NonNull Object> { ... } // same as MyList2
class MyList3<T extends @Nullable Object> { ... }
MyList1 and MyList1a must be instantiated with a nullable type. The implementation of MyList1 must be able to consume (store) a null value and produce (retrieve) a null value.
MyList2 and MyList2a must be instantiated with a non-null type. The implementation of MyList2 has to account for only non-null values — it does not have to account for consuming or producing null.
MyList3 may be instantiated either way: with a nullable type or a non-null type. The implementation of MyList3 must consider that it may be instantiated either way — flexible enough to support either instantiation, yet rigorous enough to impose the correct constraints of the specific
instantiation. It must also itself comply with the constraints of the potential instantiations.
One way to express the difference among MyList1, MyList2, and MyList3 is by comparing what expressions are legal in the implementation of the list — that is, what expressions may appear in the ellipsis in the declarations above, such as inside a method’s body. Suppose
each class has, in the ellipsis, these declarations:
T t;
@Nullable T nble; // Section "Type annotations on a use of a generic type variable", above,
@NonNull T nn; // further explains the meaning of "@Nullable T" and "@NonNull T".
void add(T arg) {}
T get(int i) {}
Then the following expressions would be legal, inside a given implementation — that is, also within the ellipses. (Compilable source code appears as file checker-framework/checker/tests/nullness/generics/GenericsExample.java.)
| MyList1 | MyList2 | MyList3 | |
| t = null; | OK | error | error |
| t = nble; | OK | error | error |
| nble = null; | OK | OK | OK |
| nn = null; | error | error | error |
| t = this.get(0); | OK | OK | OK |
| nble = this.get(0); | OK | OK | OK |
| nn = this.get(0); | error | OK | error |
| this.add(t); | OK | OK | OK |
| this.add(nble); | OK | error | error |
| this.add(nn); | OK | OK | OK |
The differences are more significant when the qualifier hierarchy is more complicated than just @Nullable and @NonNull.
Java types are invariant in their type parameter. This means that A<X> is a subtype of B<Y> only if X is identical to Y. For example, ArrayList<Number> is a subtype of List<Number>, but neither
ArrayList<Integer> nor List<Integer> is a subtype of List<Number>. (If they were, there would be a loophole in the Java type system.) For the same reason, type parameter annotations are treated invariantly. For example, List<@Nullable
String> is not a subtype of List<String>.
When a type parameter is used in a read-only way — that is, when clients read values of that type from the class but never pass values of that type to the class — then it is safe for the type to be covariant in the type parameter. Use the @Covariant annotation to indicate this. When a type parameter is covariant, two instantiations of the class with different type arguments have the same subtyping relationship as the type
arguments do.
For example, consider Iterator. A client can read elements but not write them, so Iterator<@Nullable String> can be a subtype of Iterator<String> without introducing a hole in the type system. Therefore, its type parameter is annotated with @Covariant. The first type parameter of Map.Entry is also covariant. Another example would be the type parameter of a hypothetical class ImmutableList.
The @Covariant annotation is trusted but not checked. If you incorrectly specify as covariant a type parameter that can be written (say, the class supports a set operation or some other mutation on an object of that type), then you have created an unsoundness in the type system. For
example, it would be incorrect to annotate the type parameter of ListIterator as covariant, because ListIterator supports a set operation.
Sometimes method type argument inference does not interact well with type qualifiers. In such situations, you might need to provide explicit method type arguments, for which the syntax is as follows:
Collections.<@MyTypeAnnotation Object>sort(l, c);
This uses Java’s existing syntax for specifying a method call’s type arguments.
Many type systems have a *Bottom type that is used only for the null value, dead code, and some erroneous situations. A programmer should rarely write the bottom type.
One use is on a lower bound, to indicate that any type qualifier is permitted. A lower-bounded wildcard indicates that a consumer method can accept a collection containing any Java type above some Java type, and you can add the bottom type qualifier as well:
public static void addNumbers(List<? super @SignednessBottom Integer> list) { ... }
Type qualifier polymorphism permits a single method to have multiple different qualified type signatures.
Here is where a polymorphic qualifier (e.g., @PolyNull) can be used:
• Polymorphic qualifiers are most often used in method signatures. See the examples below in Section 32.2.1.
• Polymorphic qualifiers can also be written in method bodies (implementations).
• If you can use generics, you typically do not need to use a polymorphic qualifier. Do not write a polymorphic qualifier on a type variable declaration.
• Polymorphic qualifiers may not be used on a class declaration. To apply qualifier polymorphism to classes, use a class qualifier parameter; see Section 32.3.
• A polymorphic qualifier may be used on a field declaration only in a class with a class qualifier parameter; see Section 32.3.2.
• If a class has a class qualifier parameter, then a polymorphic qualifier written on a method in the class has a slightly different meaning, see Section 32.3.1.
Section 37.5.2 explains how to define a polymorphic qualifier.
A method whose signature has a polymorphic qualifier (such as @PolyNull) conceptually has multiple versions, somewhat like the generics feature of Java or a template in C++. In each version, each instance of the polymorphic qualifier has been replaced by the same other qualifier from the hierarchy.
The method body must type-check with all signatures. A method call is type-correct if it type-checks under any one of the signatures. If a call matches multiple signatures, then the compiler uses the most specific matching signature for the purpose of type-checking. This is the same as Java’s rule for resolving overloaded methods.
As an example of the use of @PolyNull, method Class.cast returns null if and only if its argument is
null:
@PolyNull T cast(@PolyNull Object obj) { ... }
This is like writing:
@NonNull T cast( @NonNull Object obj) { ... }
@Nullable T cast(@Nullable Object obj) { ... }
except that the latter is not legal Java, since it defines two methods with the same Java signature.
As another example, consider
// Returns null if either argument is null.
@PolyNull T max(@PolyNull T x, @PolyNull T y);
which is like writing
@NonNull T max( @NonNull T x, @NonNull T y);
@Nullable T max(@Nullable T x, @Nullable T y);
At a call site, the most specific applicable signature is selected.
Another way of thinking about which one of the two max variants is selected is that the nullness annotations of (the declared types of) both arguments are unified to a type that is a supertype of both, also known as the least upper bound or lub. If both arguments are
@NonNull, their unification (lub) is @NonNull, and the method return type is @NonNull. But if even one of the arguments is @Nullable, then the unification (lub) is @Nullable, and so is the return type.
Qualifier polymorphism has the same purpose and plays the same role as Java’s generics. You use them for similar reasons, such as:
• A method operates on collections with different types of elements.
• Two different arguments have the same type, without constraining them to be one specific type.
• A method returns a value of the same type as its argument.
If a method is written using Java generics, it usually does not need qualifier polymorphism. If you can use Java’s generics, then that is often better. On the other hand, if you have legacy code that is not written generically, and you cannot change it to use generics, then you can use qualifier polymorphism to achieve a similar effect, with respect to type qualifiers only. The Java compiler still treats the base Java types non-generically.
In some cases, you don’t need qualifier polymorphism because subtyping already provides the needed functionality. String is a supertype of @Interned String, so a method toUpperCase that is declared to take a String parameter can also be called on an
@Interned String argument.
Usually, it does not make sense to write only a single instance of a polymorphic qualifier in a method definition: if you write one instance of (say) @PolyNull, then you should use at least two. The main benefit of polymorphic qualifiers comes when one is used multiple times in a method, since then
each instance turns into the same type qualifier. (Section 32.2.4 describes some exceptions to this rule: times when it makes sense to write a single polymorphic qualifier in a signature.)
Most frequently, the polymorphic qualifier appears on at least one formal parameter and also on the return type.
It can also be useful to have polymorphic qualifiers on (only) multiple formal parameters, especially if the method side-effects one of its arguments. For example, consider
void moveBetweenStacks(Stack<@PolyNull Object> s1, Stack<@PolyNull Object> s2) {
s1.push(s2.pop());
}
In this particular example, it would be cleaner to rewrite your code to use Java generics, if you can do so:
<T> void moveBetweenStacks(Stack<T> s1, Stack<T> s2) {
s1.push(s2.pop());
}
As explained in Section 32.2.3, you will usually use a polymorphic qualifier multiple times in a signature. This section describes situations when it makes sense to write just one polymorphic qualifier in a method signature. Some of these situations can be avoided by writing a generic method, but in legacy code it may not be possible for you to change a method to be generic.
It is unusual, but permitted, to write just one polymorphic qualifier, on a return type.
Similarly, it is unusual, but permitted, to write just one occurrence of a generic type parameter, on a return type. An example of such a method is Collections.emptyList().
It can make sense to use a polymorphic qualifier just once, on an array or generic element type.
For example, consider a routine that returns the index, in an array, of a given element:
public static int indexOf(@PolyNull Object[] a, @Nullable Object elt) { ... }
If @PolyNull were replaced with either @Nullable or @NonNull, then one of these safe client calls would be rejected:
@Nullable Object[] a1;
@NonNull Object[] a2;
indexOf(a1, someObject);
indexOf(a2, someObject);
Of course, it would be better style to use a generic method, as in either of these signatures:
public static <T extends @Nullable Object> int indexOf(T[] a, @Nullable Object elt) { ... }
public static <T extends @Nullable Object> int indexOf(T[] a, T elt) { ... }
Another example is a method that writes bytes to a file. It accepts an array of signed or unsigned bytes, and it behaves identically for both:
void write(@PolySigned byte[] b) { ... }
These examples use arrays, but there are similar examples that use collections.
There is no point in writing just one polymorphic qualifier in a method signature, as the main type qualifier on a formal parameter type. Consider this signature:
void m(@PolyNull Object obj)
which expands to
void m(@NonNull Object obj)
void m(@Nullable Object obj)
This is no different (in terms of which calls to the method will type-check) than writing just
void m(@Nullable Object obj)
However, it does make sense to write a single polymorphic qualifier within a formal parameter type, as in
void m2a(List<@PolyNull MySubClass> strings)
which is similar to
void m2b(List<? extends @Nullable MySubClass> strings)
Method m2b() can be called with (for example) List<@Nullable MySubClass> and List<@NonNull MySubClass>, which are not legal arguments to method m2a().
Class qualifier parameters permit you to supply a type qualifier (only, without a Java base type) to any class (generic or not).
When a generic class represents a collection, a user can write a type qualifier on the type argument, as in List<@Tainted Character> versus List<@Untainted Character>. When a non-generic class represents a collection with a hard-coded type (as
StringBuffer hard-codes Character), you can use a class qualifier parameter to distinguish StringBuffers that contain different types of characters.
To add a qualifier parameter to a class, annotate its declaration with @HasQualifierParameter and supply the class of the top qualifier as its argument.
@HasQualifierParameter(Tainted.class)
class StringBuffer { ... }
A qualifier on a use of StringBuffer is treated as appearing both on the StringBuffer and on its conceptual type argument. That is:
@Tainted StringBuffer ≈ @Tainted Collection<@Tainted Character>
@Untainted StringBuffer ≈ @Untainted Collection<@Untainted Character>
If two types have different qualifier arguments, they have no subtyping relationship. (This is “invariant subtyping”, also used by Java for generic classes.) In particular, @Untainted StringBuffer is not a subtype of @Tainted StringBuffer; an attempt to cast between them, in either
direction, will yield an invariant.cast.unsafe error.
@HasQualifierParameter is inherited. If type T has a @HasQualifierParameter annotation, then its subtypes are automatically treated as having the same annotation.
Within a class with a qualifier parameter, the default qualifier for uses of that class is the polymorphic qualifier.
A class qualifier parameter changes the rules for instantiating polymorphic qualifiers (Section 32.2). If the receiver type has a qualifier parameter and is annotated with a polymorphic qualifier, then at a call site all polymorphic annotations are instantiated to the same qualifier as the type of the receiver expression of the method call. Otherwise, use the rules of Section 32.2.
For example, consider
@HasQualifierParameter(Tainted.class)
class Buffer {
void append(@PolyTainted Buffer this, @PolyTainted String s) { ... }
}
Because @PolyTainted applies to a type (Buffer) with a qualifier parameter, all uses of @PolyTainted are instantiated to the qualifiers on the type of the receiver expression at call sites to append. For example,
@Untainted Buffer untaintedBuffer = ...; @Tainted String taintedString = ...; untaintedBuffer.append(taintedString); // error: [argument]
The above append call is illegal because the @PolyTainted qualifier is instantiated to @Untainted and the type of the argument is @Tainted, which is a supertype of @Untainted. If the type of untaintedBuffer were
@Tainted then the call would be legal.
To express that the type of a field should have the same qualifier as the class qualifier parameter, annotate the field type with the polymorphic qualifier for the type system.
@HasQualifierParameter(Tainted.class)
class Buffer {
@PolyTainted String field;
}
At a field access where the declared type of the field has a polymorphic qualifier, that polymorphic qualifier is instantiated to the qualifier on the type of the receiver of the field access (or in the case of type variables, the qualifier on the upper bound). That is, the qualifier on myBuffer.field is the same
as that on myBuffer.
Local variables default to the top type (see Section 33.5.3). Type refinement determines whether a variable can be treated as a suitable subtype, and annotations on local variables are rarely needed as a result. However,
since qualifier parameters add invariant subtyping, type refinement is no longer valid. For example, suppose in the following code that StringBuffer is annotated with @HasQualifierParameter(Tainted.class).
void method(@Untainted StringBuffer buffer) {
StringBuffer local = buffer;
executeSql(local.toString());
}
void executeSql(@Untainted String code) {
// ...
}
Normally, the framework would determine that local has type @Untainted StringBuffer and the call to executeSql would be valid. However, since by default local has type @Tainted StringBuffer, and @Untainted
StringBuffer is not a subtype, no type refinement would be performed, leading to an error. Fixing this would require manually annotating local as an @Untainted StringBuffer, increasing the annotation burden on programmers.
For this reason, local variables with types that have a qualifier parameter use different defaulting rules. When a local variable has an initializer, the type of that initializer is used as the default type of that variable if no other annotations are written. For example, in the above code, the type of local
would be @Untainted StringBuffer. This eliminates the need for type refinement.
If many classes in a project should have @HasQualifierParameter, it’s possible to enable it on all classes in a package by default. Writing @HasQualifierParameter on a package is equivalent to writing @HasQualifierParameter on each class in that package and all
subpackages with the same arguments.
For example, writing this annotation enables @HasQualifierParameter for all classes in mypackage.
@HasQualifierParameter(Tainted.class) package mypackage;
When using @HasQualifierParameter on a package, it’s possible to disable it for a specific class using @NoQualifierParameter. Writing this on a class
indicates that it has no class qualifier parameter, and @HasQualifierParameter will not be enabled by default. Like @HasQualifierParameter, it takes one or more top annotations. It is illegal to explicitly write both @HasQualifierParameter and
@NoQualifierParameter on the same class for the same hierarchy.
Types with qualifier parameters are only allowed as type arguments to type parameters whose upper bound has a qualifier parameter. If they were allowed as type arguments for any type parameter, then unsound casts would be permitted. For example:
@HasQualifierParameter(Tainted.class)
interface Buffer {
void append(@PolyTainted String s);
}
public class ClassQPTypeVarTest {
<T> @Tainted T cast(T param) {
return param;
}
void bug(@Untainted Buffer b, @Tainted String s) {
cast(b).append(s); // error
}
}