> From: "Kevin Bourrillion" <[email protected]> > To: "daniel smith" <[email protected]> > Cc: "valhalla-spec-experts" <[email protected]> > Sent: Tuesday, February 7, 2023 7:50:08 PM > Subject: Re: Nullness markers to enable flattening
> 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. > On Mon, Feb 6, 2023 at 5:26 PM Dan Smith < [ mailto:[email protected] | > [email protected] ] > wrote: >> - 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. > (The points below are general, but when the type in question is flattenable it > likely makes sense to enforce more strongly.) > 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*. > 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.) >> - 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. > 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) [ > https://github.com/jspecify/jspecify/wiki/type-usages | type usages ] 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. > (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.) 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. 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. 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). >> - 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. > 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. > 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. >> - 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.) > 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? In that case, the attribute containing the nullness information can be erased/not generated. >> - 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. > I believe you will need the distinction between *unspecified* T and > *parametric* > T. This is the second reason why JSpecify needs ` [ > https://jspecify.dev/docs/api/org/jspecify/annotations/NullMarked.html | > @NullMarked ] `; 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. > In summary, I'm extremely glad we're thinking along these lines, and I hope to > be helpful. Rémi
