<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">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><div><br></div><div>Hi,</div><div><br></div><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><div><br></div>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 class="gmail_quote"><div><br></div><div>Now consider another example:<br></div><div><br></div><div>void nonNullableStringMethod(String! notNullString) { ... }</div><div><br></div><div>void main() {<br></div><div> String? s = maybeNullString();</div><div> if (s != null) {</div><div> nonNullableStringMethod(s); // legal<br></div><div> }</div><div> nonNullableStringMethod(s); // illegal<br></div><div>}<br></div><div><br></div><div>The value s holds is known to be non-null inside the if block, so that non-null value is a valid argument to nonNullableStringMethod(). But outside the if block, the value s holds is not known to be non-null, so the value s holds is not a legal argument to nonNullableStringMethod().</div><div><br></div><div>This is different than type information. As you mentioned, type information is not control-flow-dependent, requiring casting or pattern matching to change.<br></div><div><br></div><div>CharSequence cs1 = "x";</div><div>if (cs1 instanceof String) {</div><div> nonNullableStringMethod(cs1); // illegal<br></div><div>}</div><div><br></div><div>The variable cs1 has type CharSequence, not String, and Java does not use instanceof to perform flow-dependent type inference (it could, but it doesn't).
</div><div><br></div><div>
<div>CharSequence cs2 = "x";</div><div>if (cs2 instanceof String s) {</div><div> nonNullableStringMethod(s); // legal<br></div><div>}</div><div><br></div><div>Rebinding declares a new variable with the specified type.
</div>
</div><div><br></div><div><div>Cheers,</div><div>Clement Cherlin<br></div></div></div></div>