Nullability in Java

[forax at univ-mlv.fr]

----- 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