null aware type system - jspecify/jspecify GitHub Wiki

You can start by understanding the basic model. It should be enough to handle most situations.

Eventually it might fall short, or you might crave a deeper understanding of how to "think like an analyzer". At that point it will help to start thinking of the annotations as creating a null-aware type system.

To actually understand a type system probably requires passing at least one graduate-level course in type theory. We don't have time for that! And our goal isn't to jump five levels deeper than the basic model, just one. Fortunately, there's a simplified understanding that should serve us well enough.

A type system:

• Decides, based on the user's code, what types exist. For example, if user code says class Foo {}, Java's type system decides that there are types like Foo, Foo[], List<Foo>, and so on.
• Defines a set of calculations over those types. Most importantly, a type conversion is a rule that permits one type to be given somewhere a different type was expected.

Java's compile-time type system is spelled out in gory detail in JLS 4 and JLS 5. It's not really a recommended read unless you're building your own analyzer.

Java‘s type system ignores our annotations!

When you write @Nullable String, the only type Java recognizes is String. As always, that string is ambiguously nullable.

But Java permits type-use annotations to "ride along with" type usages, like in a sidecar. Any type usage can have such an annotation before it. But Java never treats these as a real part of the type. We call the type as javac sees it (without annotations) a base type.

Part of the special function of a nullness analyzer is to interpret String and @Nullable String (for example) as though they are properly distinct types. We call a base type together with information about its nullness an augmented type.

Java says that null is automatically a member of every reference type. You might write just Object, but what you really get is a union type of Object and the null type.

A "union type" normally has only the capabilities shared by both of the types that form it. But this union type is different:

• You can freely assign null to it (as if it's nullable)
• Yet you can freely deference it as well (as if it's non-null)

We might call this a "lenient union type" or an "optimistic union type" (terms which apparently don't even exist on the web!) And of course, this compile-time leniency is precisely why you see so many NullPointerExceptions at runtime.

What JSpecify[^1] does is to simulate a modified type system where that doesn't happen. (Of course, we're not the first to think of this; we're just standardizing it.)

Within null-marked code, you can in essence pretend that Java doesn't automatically graft null onto every reference type. String means an actual string. When you want null to be included, you write @Nullable String, which forms a proper union type between a real string and the "null type".

By "proper union type", we mean:

• You can only assign null to it if it's nullable
• You can only dereference it if it's non-null

Otherwise, you'll get a warning from your analysis tools.

This is how we'd normally expect a union type to work in a strongly-typed language: it has only the shared capabilities, but the combined constraints.

Note: see notation for a short overview of the shorthand type notation used here. In brief, String? means @Nullable String and String! means "either @NonNull String, or String-in-a-null-marked-context".

String! is always a subtype of String?.

The idea of subtyping (say, that SubFoo is a subtype of Foo) carries both a hard requirement and a soft requirement. The hard requirement is that every possible instance of type SubFoo must have the type Foo as well. But also, we would generally expect SubFoo to have some additional capabilities or relaxed constraints, and that part is the "soft" requirement.

This means that any proper union type A U B has A and B as subtypes. And our case is no exception: String! is a subtype of String?.

Much of the JSpecify specification boils down to this idea: for any scenario where Java specifies that a subtyping check should happen, we apply our extended definition as well.

For example, Java has array covariance, which says (for example) that String[] is automatically a subtype of CharSequence[]. We extend that same notion to say that String![] is also a subtype of String?[] (and of course this is transitive).

On the other hand, generic types are still invariant, so List!<Foo!> is not a subtype of List!<Foo?>, but is a subtype of List!<? extends Foo?>.

(That does get easier to read in time. We're not used to having this additional information present in our types. It is unfortunate that the last example uses the ? symbol in two different ways, but there's never an actual ambiguous case.)

All this means that Object? is the new "top type" of the hierarchy: the common supertype of every reference type. One consequence is that List<? extends Object> no longer means "any list": it now excludes lists with null elements. (The proper way to say "any list" has always been List<?>, in any case.)

Java's generic type system is challenging enough to make sense of as it is, and at times it feels like jamming nullness information in as well makes it that much worse. But, if you learn to think of @Nullable and @NonNull as if they are part of the type they precede, and remember that @NonNull Foo is always a subtype of @Nullable Foo, you'll mostly be fine.

For example, if you want your type parameter to accept only non-null types, you write

// in null-marked context

class MyType<T extends Base>

... whereas to allow nullable types as well, you write

// in null-marked context

class MyType<T extends @Nullable Base>

Hopefully reading (re-reading?) this page has made it clear why these are the right incantations!