Nullability in Java
forax at univ-mlv.fr
forax at univ-mlv.fr
Wed Oct 2 14:29:53 UTC 2024
----- Original Message -----
> From: "Brian Goetz" <brian.goetz at oracle.com>
> To: "Remi Forax" <forax at univ-mlv.fr>
> Cc: "valhalla-spec-experts" <valhalla-spec-experts at openjdk.java.net>
> Sent: Wednesday, October 2, 2024 2:51:34 PM
> Subject: Re: Nullability in Java
Hello,
> This aligns pretty well with what we’ve been discussing. Your principle (1) is
> key, because this is what enables adding nullity annotations to be
> source-compatible, and we want to minimize the friction to adding nullity
> annotations. This means warnings, not errors, backed up by dynamic checks.
>
> From a language perspective, the states `String` and `String?` are semantically
> identical; the only difference between them is what warnings might be emitted.
>
> I don’t see the point of excluding locals (or indeed, any) declarations from
> being null-markable. (Some are already implicitly null-restricted, such as the
> throws clause.) Doing so will creates “gates” that impede the flow of type
> information, which would undermine your principle (3).
I don't fully understand what you mean by "gates".
The point is to have the type of locals to change their null-marker implicitly.
I see two reasons why.
1) If you have a code like:
String s = f();
g(s);
If 's' has its null-marker computed automatically, the null marker will flow naturally without the user having to update his code each time the API of a dependency is updated to use null-marker.
2) until now, the type of a local variable would never change, we have even introduced the concept of binding to explicitly avoid a local variable to have its type changed.
But we also want the nullability part of the type of a local to change dependending on the control flow, so having a way to denote the nullability on a local's type given that it can changed is weird.
By example, with
class Foo {
void m(String! a) { ... }
void main() {
String? s = ...
if (s == null) {
// s is know a String!
...
}
}
}
Here, declaring that the type of s is a '?' is not true for the lifetime of the variable because the nullability of the type of s can change depending on the control flow.
Avoiding to have a way to denote the nullability of the type of a local variable avoid that issue.
Rémi
>
>> On Oct 2, 2024, at 3:16 AM, Remi Forax <forax at univ-mlv.fr> wrote:
>>
>> Hello,
>> i would like a propose a semantics adding a null-analysis to Java.
>>
>> Principles
>> - 1/ the compiler should emit a warning only if a NullPointerException will
>> occur if the value is null
>> - 2/ the syntax should explicitly indicate where a NPE can occur
>> - 3/ the compiler should be smart enough to avoid bothering users when a NPE can
>> not occur (by example: after a "if (a != null)" a should be considered as
>> non-null)
>>
>> Nice to have
>> - while the internal representation is a 3 states (String!, String? and String),
>> it should be cool if users can only denote two states to simplify the action a
>> user can do
>> - the change of the JLS should be confined to a section
>>
>> Proposal:
>> - on field, methods, casts, arrays and type arguments, the null-analysis marker
>> '!' can be used to denote a non-null type.
>> A NPE will be raised
>> - if a null value is stored in such field, array,
>> - if a null value is casted to a non-null type,
>> - if a null value is pass as argument of a method parameter typed with a
>> non-null type
>>
>> Example:
>> class Foo {
>> String! s;
>> String![] array = ...;
>>
>> void m(String! a) {} // NPE
>>
>> void main() {
>> s = aMethodThatReturnsNull(); // NPE
>> array[0] = aMethodThatReturnsNull(); // NPE
>> var o = (String!) aMethodThatReturnsNull(); // NPE
>> m(aMethodThatReturnsNull());
>> }
>> }
>>
>> - on field, methods, casts, arrays and type arguments, the null-analysis
>> marker'?' can be used to denote a nullable type.
>>
>> - Inside methods, local variable declaration are NOT annotated with nullability
>> marker, the nullability is inferred,
>> so the analysis
>> - can be smarter than the current type-checking, especially the nullability of a
>> local variable can change depending on the control flow
>> - the analysis can be separated from the type checking in the spec (but not in
>> the compiler)
>> - even if the proposed semantics is not non-null by default, a user will not
>> have to annotate a lot of locus, mostly only fields and methods.
>>
>> Example:
>> class Bar {
>> String! aMethodThatCannotReturnsNull() { ... }
>> String? aMethodThatReturnsNull() { return null; }
>>
>> void main() {
>> String s = aMethodThatCannotReturnsNull(); // the type of 's' is inferred as
>> String!
>> String s2 = aMethodThatReturnsNull(); // the type of 's2' is inferred as
>> String?
>> if (s2 != null) {
>> // here the type of s2 is String!
>> }
>> }
>> }
>>
>> - on fields and methods, every type wich is not a ! (a non-null type) is a ? (a
>> nullable type)
>> if there is already a '?' or '!' in the same compilation unit (same file).
>> Having a '?' or '!' somewhere acts as an opt-in to the null-analysis mechanism,
>> it guarantee that
>> - until you opt-in, no warnings can be raised
>> - if you opt-in, the user model has only two denotable kinds of nullability,
>> String! and String?, the latter can written String
>>
>> - A type variable is nullable by default and propagate the nullability
>> information if a user has opt-in to the null-analysis.
>> At declaration site, E is equivalent to E?, which really means E extends Object?
>>
>> Example:
>> class Foo<E?> { // a '?' is present so the user as opt-in to E propagating the
>> nullability information
>> void m(E! e) { } // m() can not be called with null
>> void m2(E e) { } // equivalent to void m2(E?)
>> )
>>
>> - As discussed previously, a field with a non-null type must be initialized in
>> the constructor before the call to the super constructor call.
>>
>> - @SuppressWarnings("null-analysis") allows to suppress any null warnings so
>> even if a user has opt-in to the null analysis it can still
>> incrementally had the null marker later. This also allows add null markers on
>> public methods (on the API) without having any warnings
>> in the implementation.
>>
>> regards,
>> Rémi
More information about the valhalla-spec-experts
mailing list