Nullability in Java

[forax at univ-mlv.fr]

> 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 < [ mailto:forax at univ-mlv.fr | forax at univ-mlv.fr
> ] > wrote:

>> ----- Original Message -----
>>> From: "Brian Goetz" < [ mailto:brian.goetz at oracle.com | brian.goetz at oracle.com ]
>> > >
>> > To: "Remi Forax" < [ mailto:forax at univ-mlv.fr | forax at univ-mlv.fr ] >
>>> Cc: "valhalla-spec-experts" < [ mailto:valhalla-spec-experts at openjdk.java.net |
>> > 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 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/valhalla-spec-observers/attachments/20241011/fb34ac60/attachment-0001.htm>