Nullability in Java

[Clement Cherlin]

On Fri, Oct 11, 2024 at 12:42 PM <forax at univ-mlv.fr> wrote:

>
>
> ------------------------------
>
> *From: *"Clement Cherlin" <ccherlin at gmail.com>
> *To: *"Valhalla Expert Group Observers" <
> valhalla-spec-observers at openjdk.org>, "Remi Forax" <forax at univ-mlv.fr>,
> "Brian Goetz" <brian.goetz at oracle.com>
> *Sent: *Thursday, October 10, 2024 6:37:01 PM
> *Subject: *Re: Nullability in Java
>
> On Wed, Oct 2, 2024 at 9:30 AM <forax at univ-mlv.fr> wrote:
>
>> ----- 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
>>
>
> Hi,
>
>
> Hello,
>
>
> The type of a nullable variable does not change even when the nullness of
> the value it contains is known. If a variable declared as "String? s"
> contains a value that is known to be non-null at a given execution point,
> the type of s is still "String?".
>
> Consider the following example:
>
> String? s = maybeNullString();
> if (s != null) {
>   s = null; // legal
> }
>
> Inside the if block the _value_ of s is known to be non-null, but the
> _type_ of s is still "String?" and not "String!". If the type had changed
> to "String!", the commented line would be illegal.
>
>
> The way I see this is that the type is composed of two types, the one you
> used when writing and the one used when reading.
> inside the if, and before assigning null to 's', the type of 's' is
> (WRITE=String?, READ=String!).
>
> Kotlin does something similar for modeling platform types,
> https://www.youtube.com/watch?v=2IhT8HACc2E
>
> regards,
> Rémi
>

I suppose I agree to the extent that one could consider "nullness" to
be the read type and "nullability" to be the write type, but I don't
really think of "nullness" as type information at all.

Nullness analysis is more like definite assignment analysis than it is
like type analysis. Definite assignment and nullness are
flow-dependent. Each node in the control flow graph has both definite
assignment and nullness metadata for each variable in scope at that
node. Definite assignment and nullness metadata are used to determine
whether certain operations, such as reads, writes, and method calls are
legal or illegal at each point. It's illegal to read from a variable
unless that variable is definitely assigned. Likewise, it is illegal to
use a variable in a non-nullable context unless that variable is
definitely not null.

Neither analysis affects the types of variables. A String? always
remains a String?. It doesn't become a String! when itis assigned a
non-null value, it becomes a String {DEFINITELY_ASSIGNED,NOT_NULL}.

Side note:
There are a few major differences. Non-final variables can change their
nullness many times in sequence, while definite assignment only occurs
once in a given execution path. Definite assignment is an implicit
requirement of the language, while nullability marking is explicit. And
nullness can change based on nullness tests, not just assignments.

Cheers,
Clement Cherlin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/valhalla-spec-observers/attachments/20241015/d35f1abc/attachment-0001.htm>