<html><body><div style="font-family: arial, helvetica, sans-serif; font-size: 12pt; color: #000000"><div><br></div><div><br></div><hr id="zwchr" data-marker="__DIVIDER__"><div data-marker="__HEADERS__"><blockquote style="border-left:2px solid #1010FF;margin-left:5px;padding-left:5px;color:#000;font-weight:normal;font-style:normal;text-decoration:none;font-family:Helvetica,Arial,sans-serif;font-size:12pt;"><b>From: </b>"Clement Cherlin" <ccherlin@gmail.com><br><b>To: </b>"Valhalla Expert Group Observers" <valhalla-spec-observers@openjdk.org>, "Remi Forax" <forax@univ-mlv.fr>, "Brian Goetz" <brian.goetz@oracle.com><br><b>Sent: </b>Thursday, October 10, 2024 6:37:01 PM<br><b>Subject: </b>Re: Nullability in Java<br></blockquote></div><div data-marker="__QUOTED_TEXT__"><blockquote style="border-left:2px solid #1010FF;margin-left:5px;padding-left:5px;color:#000;font-weight:normal;font-style:normal;text-decoration:none;font-family:Helvetica,Arial,sans-serif;font-size:12pt;"><div dir="ltr"><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Oct 2, 2024 at 9:30 AM <<a href="mailto:forax@univ-mlv.fr" target="_blank">forax@univ-mlv.fr</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">----- Original Message -----<br>
> From: "Brian Goetz" <<a href="mailto:brian.goetz@oracle.com" target="_blank">brian.goetz@oracle.com</a>><br>
> To: "Remi Forax" <<a href="mailto:forax@univ-mlv.fr" target="_blank">forax@univ-mlv.fr</a>><br>
> Cc: "valhalla-spec-experts" <<a href="mailto:valhalla-spec-experts@openjdk.java.net" target="_blank">valhalla-spec-experts@openjdk.java.net</a>><br>
> Sent: Wednesday, October 2, 2024 2:51:34 PM<br>
> Subject: Re: Nullability in Java<br>
<br>
Hello,<br>
<br>
> This aligns pretty well with what we’ve been discussing. Your principle (1) is<br>
> key, because this is what enables adding nullity annotations to be<br>
> source-compatible, and we want to minimize the friction to adding nullity<br>
> annotations. This means warnings, not errors, backed up by dynamic checks.<br>
> <br>
> From a language perspective, the states `String` and `String?` are semantically<br>
> identical; the only difference between them is what warnings might be emitted.<br>
> <br>
> I don’t see the point of excluding locals (or indeed, any) declarations from<br>
> being null-markable. (Some are already implicitly null-restricted, such as the<br>
> throws clause.) Doing so will creates “gates” that impede the flow of type<br>
> information, which would undermine your principle (3).<br>
<br>
I don't fully understand what you mean by "gates".<br>
<br>
The point is to have the type of locals to change their null-marker implicitly.<br>
I see two reasons why.<br>
<br>
1) If you have a code like:<br>
String s = f();<br>
g(s);<br>
<br>
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.<br>
<br>
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.<br>
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.<br>
<br>
By example, with<br>
class Foo {<br>
void m(String! a) { ... }<br>
<br>
void main() {<br>
String? s = ...<br>
if (s == null) {<br>
// s is know a String!<br>
...<br>
}<br>
}<br>
}<br>
<br>
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.<br>
Avoiding to have a way to denote the nullability of the type of a local variable avoid that issue.<br>
<br>
Rémi<br></blockquote><br><div>Hi,</div></div></div></blockquote><div><br></div><div>Hello,<br data-mce-bogus="1"></div><div><br data-mce-bogus="1"></div><blockquote style="border-left:2px solid #1010FF;margin-left:5px;padding-left:5px;color:#000;font-weight:normal;font-style:normal;text-decoration:none;font-family:Helvetica,Arial,sans-serif;font-size:12pt;"><div dir="ltr"><div class="gmail_quote"><br><div>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?".</div><br>Consider the following example:</div><div class="gmail_quote"><br></div><div class="gmail_quote">String? s = maybeNullString();<br></div><div class="gmail_quote">if (s != null) {</div><div class="gmail_quote"> s = null; // legal<br></div><div class="gmail_quote">}</div><div class="gmail_quote"><br></div><div class="gmail_quote">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.
</div></div></blockquote><div><br></div><div>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.<br data-mce-bogus="1"></div><div>inside the if, and before assigning null to 's', the type of 's' is (WRITE=String?, READ=String!).<br data-mce-bogus="1"></div><div><br data-mce-bogus="1"></div><div><div>Kotlin does something similar for modeling platform types,</div><div>https://www.youtube.com/watch?v=2IhT8HACc2E</div></div><div><br data-mce-bogus="1"></div>regards,</div><div data-marker="__QUOTED_TEXT__">Rémi<br data-mce-bogus="1"></div><div data-marker="__QUOTED_TEXT__"><br data-mce-bogus="1"></div></div></body></html>