
<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>"Kevin Bourrillion" <kevinb@google.com><br><b>To: </b>"daniel smith" <daniel.smith@oracle.com><br><b>Cc: </b>"valhalla-spec-experts" <valhalla-spec-experts@openjdk.java.net><br><b>Sent: </b>Tuesday, February 7, 2023 7:50:08 PM<br><b>Subject: </b>Re: Nullness markers to enable flattening<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>As the person with a foot in both Valhalla and JSpecify camps, and who is obsessed with keeping Java as conceptually simple as it can be, as long as this all works out I'll consider it to be a major win.</div><br><br><div dir="ltr">On Mon, Feb 6, 2023 at 5:26 PM Dan Smith <<a href="mailto:daniel.smith@oracle.com" target="_blank">daniel.smith@oracle.com</a>> wrote:<br></div><div dir="ltr"><br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">- Because nullness is distinct from types, it shouldn't impact type checking rules, subtyping, overriding, conversions, etc. Nullness has its own analysis, subject to its own errors/warnings. The precise error/warning conditions haven't been fleshed out, but our bias is towards minimal intrusion—we don't want to make it hard to adopt these features in targeted ways.<br></blockquote><br><div>(The points below are general, but when the type in question is flattenable it likely makes sense to enforce more strongly.)</div><br><div>I think this is a very salient point: there is a trade-off between enforcing the new nullness information as well as we might like vs. the adoptability of the feature. To arrive eventually at a null-safe world, the most importantly early step is for as many APIs as possible to provide the information. If they worry about breaking clients already, they won't be able to do it; if that means javac being lenient on enforcement, that's okay! Third-party nullness analysis tools have their role to play for a very long time anyway, which is a fine thing. Really, the "worst" thing about these tools today is simply "ugh, the type annotations are too bulky", and there's value even in solving *just that*.</div><br><div>In fact, the spec being stringent about which cases definitely produce a warning might even be counterproductive. Third-party analyzers will analyze more deeply and take advantage of wider sources of information, and the typical effect is to recognize that a certain expression *can't* be null when it otherwise seemed like it could. That means the deeper analysis would end up wanting to *subtract* warnings from javac, which of course it can't do (currently has no way to do?). (Again, this applies less to the value types that are the actual motivating use case here.)</div><br><br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">- That said, *type expressions* (the syntax in programs that expresses a type) are closely intertwined with *nullness markers*. 'Foo!' refers to a non-null Foo, and 'Foo?' refers to a Foo or null. And nullness is an optional property of type arguments, type variable bounds, and array components. Nullness markers are the way programmers express their intent to the compiler's nullness analysis.<br></blockquote><br><div>Altogether, I think you're saying that this nullness attribute is attached to *every* static type recognized by the compiler: types of expressions, of expression contexts, and the (usually explicit) <a href="https://github.com/jspecify/jspecify/wiki/type-usages" target="_blank">type usages</a> you mention. Basically I would expect that most programmers most of the time will be well-served (enough) to think of this attribute as *if* it's an intrinsic part of the type. It's sort of the exact illusion this is all trying to create.</div><br><div>(One mild exception is that it is possibly counterproductive to enforce override strict parameter agreement in the nullness attribute; as far as we can tell, allowing a nullable parameter to override a non-null one is nearly harmless and we think makes for a better migration story.)</div></div></div></blockquote><div><br></div><div>I think we can follow the "generics erasure" playbook here, i.e. if a method has a nullness attribute either an overriden method has a nullness attribute with the same values or it does not have one.<br data-mce-bogus="1"></div><div>This allow to annotate a library with nullness information without having to change the client code that may have a class that override a method from the library.<br data-mce-bogus="1"></div><div>About having a nullable parameter to overrride a non-null one, this goes against the idea that Java parameters are invariant not contravariant (you can not have a method that takes an Object as parameter to override a method that takes a String as parameter even if it is sound in term of type). One advantage i see to keep the method parameter to be invariant is that as a user of a method i know that not only a method but also all its overrides will never allow null, even if the nullness checking is done at declaration site (erasure of the nullness information aside).<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><br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">- There are features that change the default interpretation of the nullness of class names. This is still pretty open-ended. Perhaps certain classes can be declared (explicitly or implicitly) null-free by default (e.g., 'Point' is implicitly 'Point!'). Perhaps a compilation-unit- or module- level directive says that all unadorned types should be interpreted as '!'. Programs can be usefully written without these convenience features, but for programmers who want to widely adopt nullness, it will be important to get away from "unspecified" as the default everywhere.<br></blockquote><br><div>If a release has the rest of it but not this part, users will find it extremely annoying, but it might be survivable if we can see the other side of the chasm from there. It's definitely essential long-term. </div><br class="gmail-Apple-interchange-newline"><div>Of course, TypeScript, Scala, C#, and Dart all do it this way, through either a configuration file or compiler flag etc. Java's analogue is module-info, but yes, I do think adoptability would benefit *very* much from a class- or compilation-unit level modifier as well. And (sigh) I guess package-info, even though when that gets used outside a module it's kind of a disaster.</div><br><br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">

- Nullness is generally enforced at run time, via cooperation between javac and JVMs. Methods with null-free parameters can be expected to throw if a null is passed in. Null-free storage should reject writes of nulls. (Details to be worked out, but as a starting point, imagine 'Q'-typed storage for all types. Writes reject nulls. Reads before any writes produce a default value, or if none exists, throw.)<br></blockquote><br><div>This raises some questions for the scenarios where we are compelled to write `@SuppressWarnings("nullness")`; that information obviously isn't available at runtime. Perhaps there would need to be a more targeted suppression mechanism?</div></div></div></blockquote><div><br></div><div>In that case, the attribute containing the nullness information can be erased/not generated.<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><br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">

- Type variable types have nullness, too. Besides 'T!' and 'T?', there's also a "parametric" 'T*' that represents "whatever nullness is provided by the type argument". (Again, some room for choosing the default interpretation of bare 'T'; unspecified nullness is useful for type variables as well.) Nullness of type arguments is inferred along with the types; when both a type argument and its bound have nullness, bounds checks are based on '!' <: '*' <: '?'. Generics are erased for now, but in the future '!' type arguments will be reified, and specialized classes will provide the expected runtime behaviors.<br></blockquote><br><div>I believe you will need the distinction between *unspecified* T and *parametric* T. This is the second reason why JSpecify needs `<a href="https://jspecify.dev/docs/api/org/jspecify/annotations/NullMarked.html" target="_blank">@NullMarked</a>`; it isn't just "`!` by default"; it's also "type-variable usages become parametric instead of unspecified". Again, what I believe matters is that users have some way to express the distinction, not how much or little javac and the runtime do out of the gates to enforce it.</div><br><div>In summary, I'm extremely glad we're thinking along these lines, and I hope to be helpful.</div><br></div></div></blockquote><div><br></div><div>Rémi<br data-mce-bogus="1"></div><div><br></div></div></div></body></html>