<div dir="ltr"><div dir="ltr"></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Oct 11, 2024 at 12:42 PM <<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"><div><div style="font-family:arial,helvetica,sans-serif;font-size:12pt;color:rgb(0,0,0)"><div><br></div><div><br></div><hr id="m_3674884021808137010zwchr"><div><blockquote style="border-left:2px solid rgb(16,16,255);margin-left:5px;padding-left:5px;color:rgb(0,0,0);font-weight:normal;font-style:normal;text-decoration:none;font-family:Helvetica,Arial,sans-serif;font-size:12pt"><b>From: </b>"Clement Cherlin" <<a href="mailto:ccherlin@gmail.com" target="_blank">ccherlin@gmail.com</a>><br><b>To: </b>"Valhalla Expert Group Observers" <<a href="mailto:valhalla-spec-observers@openjdk.org" target="_blank">valhalla-spec-observers@openjdk.org</a>>, "Remi Forax" <<a href="mailto:forax@univ-mlv.fr" target="_blank">forax@univ-mlv.fr</a>>, "Brian Goetz" <<a href="mailto:brian.goetz@oracle.com" target="_blank">brian.goetz@oracle.com</a>><br><b>Sent: </b>Thursday, October 10, 2024 6:37:01 PM<br><b>Subject: </b>Re: Nullability in Java<br></blockquote></div><div><blockquote style="border-left:2px solid rgb(16,16,255);margin-left:5px;padding-left:5px;color:rgb(0,0,0);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></div><div><br></div><blockquote style="border-left:2px solid rgb(16,16,255);margin-left:5px;padding-left:5px;color:rgb(0,0,0);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></div><div>inside the if, and before assigning null to 's', the type of 's' is (WRITE=String?, READ=String!).<br></div><div><br></div><div><div>Kotlin does something similar for modeling platform types,</div><div><a href="https://www.youtube.com/watch?v=2IhT8HACc2E" target="_blank">https://www.youtube.com/watch?v=2IhT8HACc2E</a></div></div><div><br></div>regards,</div><div>Rémi<br></div></div></div></blockquote><br></div><div class="gmail_quote">I suppose I agree to the extent that one could consider "nullness" to<br>be the read type and "nullability" to be the write type, but I don't<br>really think of "nullness" as type information at all.<br><br>Nullness analysis is more like definite assignment analysis than it is<br>like type analysis. Definite assignment and nullness are<br>flow-dependent. Each node in the control flow graph has both definite<br>assignment and nullness metadata for each variable in scope at that<br>node. Definite assignment and nullness metadata are used to determine<br>whether certain operations, such as reads, writes, and method calls are<br>legal or illegal at each point. It's illegal to read from a variable<br>unless that variable is definitely assigned. Likewise, it is illegal to<br>use a variable in a non-nullable context unless that variable is<br>definitely not null.<br><br>Neither analysis affects the types of variables. A String? always<br>remains a String?. It doesn't become a String! when itis assigned a<br>non-null value, it becomes a String {DEFINITELY_ASSIGNED,NOT_NULL}.<br><br>Side note:<br>There are a few major differences. Non-final variables can change their<br>nullness many times in sequence, while definite assignment only occurs<br>once in a given execution path. Definite assignment is an implicit<br>requirement of the language, while nullability marking is explicit. And<br>nullness can change based on nullness tests, not just assignments.<br><br>Cheers,<br>Clement Cherlin</div></div>