-
Notifications
You must be signed in to change notification settings - Fork 26
null aware type system
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 likeFoo
,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 NullPointerException
s 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!
Note: The contents of this wiki are not final, and represent current thinking and discussions.