general user feedback

[Caleb Cushing]

I'm going to try to provide feedback in sections. To prefix I haven't gone through every piece of documentation, so I apologize if I'm saying anything that is incorrect. I tend to read code and look at text if the meaning of the code is not obvious. I only heard of this project yesterday. In someway you may additionally consider this feedback on the user documentation.

Have you considered using github discuss instead? hopefully subscribe works well, since I'm not on the group.

NullMark: So, I see that the api is more or less considered stable... I'm going to consider this unfortunate as if I was looking at a new code base, and see @NullMark without having heard of jspecify I would not know what it means, and perhaps more importantly I might assume it means a Nullable API. I see that it contrasts with @NullUnmarked, and reading that javadoc makes it make more sense.

However, here's what I'd really like

* NullMark should require the specification of the default, e.g. NullMark(Nullness.NULLABLE)

enum Nullness {
   NULLABLE,
   NONNULL,
   UNMARKED // questionable? isn't this the same as no annotation being defined at all
}

To me this code is infinitely more readable about what is going on. Although, perhaps it's still flawed. It seems to me that it's important for fields and functions to be handled differently. Springs NonNullApi (still a questionable name), and NonNullFields are infinitely more readable.

On that note, the user guide makes no comment on how fields are handled out of the box. I assume they're considered Nonnull by default too. I don't feel that will encourage adoption, my experience with web service development is fields historically are Nullable with getter/setters supporting the same. Other methods are generally not null safe.

This brings up unmarked, and the default. My experience with handling of 3rd party code suggests it will be problematic. Sensible documented handling of truly unmarked code would be as follows (IMHO), 

* Properties (fields + getter/setter) are assumed to  be fully nullable
* Other methods are assumed to have @Nonnull input, and @Nullable output

I've filed at least a couple of bugs with Nullaway on the JDK added support having the second point wrong.

where's the plan for adding external support for it, so that tools can have a standard 3rd party jar that they can use. Perhaps Kotlin is too heavyweight, or a subset needs to be standardized for this as full extensions would be too much (I'd guess). I'm not picky here as to solution, but 3rd party will lag behind with adoption, so there needs to be some solution, and it would appear given checker, and nullaway that it needs to be incremental, meaning a full java class probably doesn't work.

So, what's the deal with the JDK on this? to really get this right, this needs to go into java itself. If anyone from oracle is reading this, I know we were given Optional, but from what I've seen in the "industry" with typescript, kotlin, and more, the `?` operator is better for many things and providing metadata to lead to a language feature for that is really what should be done.

Last note, the documentation doesn't say how to add this to a project. I'd say that you should add the GAV/JPMS to the user documentation.

[Chris Povirk]

Hi, Caleb,

Nice to see you drop by here. I know I've seen you on the tracker for Error Prone and elsewhere in the past.

I'm about to leave for the long weekend, so I'll reply to what I can now. Either someone else will pick up where I leave off, or I'll get back to this in the coming week.

---

I don't know that we've talked about GitHub discuss. It does seem like JSpecify could be well suited to it. Does anyone else on this thread have experience with it?

---

For the naming of @NullMarked, I have taken the difficult-to-defend position that the unclear name is a feature :) The initial name was something like "@DefaultNonNull," but over time, it became clear that that name could mislead. Within the scope of @DefaultNonNull, the default is arguably not always null:

• "List<?>" means a list whose elements might or might not be null. Users could find it surprising that this happens without a @Nullable annotation in sight.
• Usages of type variables don't all become non-nullable (the way they do with existing annotations like @ParametersAreNonnullByDefault). Instead, some have "parametric nullness," which is to say that their nullness comes from the type argument. For example, list.get(...) returns a non-null String if called on a List<String> but a nullable String if called on a List<@Nullable String>.
• "Top-level" types of variable don't become non-nullable.

To "solve" the problem of a misleading name, we picked a somewhat ambiguous name—which, as you've noticed, can mislead in its own way....

To some degree, this is unsolvable. And at this point, we've finally started going around telling people that we're "extremely unlikely" to make "compilation-breaking changes." So the plan now is to succeed so thoroughly that everyone learns what @NullMarked is :)

The idea of a 3-way default (nullable, non-null, unspecified) was also part of the initial design. Part of the reason that we dropped it was the idea that @NullMarked is slightly more than "default non-null," as discussed above. Another part was that we want nullness to be understandable in isolation as much as possible: It's already bad enough that @NullMarked gives us one "defaulting" annotation that can change what a type like "String" means 1000 lines away (or even in another file); we'd rather users not have to wonder which of 4 meanings the type might have.

OK, I'm out of time :) Feel free to reply to any of that or to wait for more.

[Chris Povirk]

OK, on to fields:

(Yes, they're non-null by default, with the same set of special cases that apply elsewhere.)

Fields are likely a case in which different codebases (or even different parts of the same codebase) would be especially interested in different defaults. Some classes have fields that are entirely optional or that have deferred initialization (the latter of which may or may not be a good case for @Nullable, depending on who you ask :)). Other code has entirely final, non-nullable fields. And other code falls close to either end but with a few places where @Nullable or @NonNull could patch things up.

The arguments against field-specific defaults are similar to the arguments against a 3-way default in general. (Another one that I forgot is that it's arguably useful for "@NonNull" to be a mild smell (at least in @NullMarked code, since it's very rarely necessary there).) In particular, as you note, it's likely that nullable fields are going to be associated with nullable setters and getters. There would be something at least a little surprising about a field `private Map<String, @Nullable Object>` and a corresponding getter `public @Nullable Map<String, @Nullable Object>`, for example.

As I understand it, this is the direction that languages have generally gone when adding nullness to the language. (JSR-305 was unusual in its support for different defaults in different locations, though I admit that the Checker Framework has similar features, too.) Now, it's a bit easier to swallow with a language feature, which typically lets you write just `List<String?>?` instead of `@Nullable List<@Nullable String>`. Still, there are benefits to moving in the direction that languages do, whether you're interoperating with such a language (Kotlin), you're optimistic that Java itself will have nullness built in someday, or you're just familiar with other languages.

As for the documentation of the behavior of fields:

Yes, this sounds like something that the User Guide and Javadoc could be more direct about. They make reference to the idea that "references" or "type usages" are treated the same in (almost) all locations, but they don't put as much emphasis on it as they could, nor do they fully define their terms. (Another place to cover this would be in documentation that explains how JSpecify differs from other nullness libraries/tools that users might be familiar with.)

On the handling of unmarked code:

This is something that I've always thought was cool about the JSpecify model but that I've never been sure anyone else will care about :) The JSpecify model lets tools treat unmarked/default/"unspecified" nullness leniently, strictly, or anywhere in between.

Lenient behavior is what we see with Kotlin: You can dereference the result of a call to an unannotated method (as if "unspecified" meant "non-nullable"), and you can pass null to it (as if "unspecified" meant "nullable").

Strict behavior is the opposite: You can't dereference anything until you've proven that it's non-nullable, and you can't pass null to anything.

It even goes beyond that: It's not merely that unannotated return types are "nullable": If that were the case, then if you were to override one of them (like by implementing List.subList if it were unannotated), you'd be allowed to return null. Of course, subList shouldn't ever return null. So a strict tool shouldn't allow that. And indeed, the JSpecify model, by saying that the return type has unspecified nullness, lets you forbid this, whereas a model that made the return type nullable would let it slide.

For all the interest I have in this, I'm not sure how many users will opt in to such strictness. But it's a part of our model, and I've tried it on a couple base packages just to identify dependencies that we don't have nullness information for yet. Maybe we'll see tools apply heuristics in this area, treating some unannotated APIs differently from others?

For information about third-party libraries and the JDK:

It seems likely that the solution is going to be partial files in Java source format (similar to what the Checker Framework uses) but with a way to preprocess them into a form that is more performant at runtime (like NullAway has). For the JDK specifically, we've been working with the Checker Framework's stubs, and most of Google's 2023 nullness work went toward writing those annotations into a copy of the JDK APIs themselves, which we then pointed javac and kotlinc at (details).

On a JDK feature:

Yes, that is clearly the best option from my perspective. We've been in contact with OpenJDK to do what we can to keep that possibility open, including when Valhalla touches on nullness. The more that we're able to work out now, the less we leave for them to figure out later, and the better the chance that we converge on answers that would work for both JSpecify and a hypothetical future JDK feature.

And finally (or did I miss anything?):

It is pretty weird that "org.jspecify:jspecify:0.3.0" does not appear anywhere, nor the module name ("org.jspecify"). We should fix that.

[Caleb Cushing]

> Now, it's a bit easier to swallow with a language feature, which typically lets you write just `List<String?>?` instead of `@Nullable List<@Nullable String>

Honestly I think the JDK should just end up compiling the former to the latter. The former being pure syntactic sugar.

If I have one other thought on the JDK implementing this later on down the line it would be that it would be nice to have it auto throw runtime errors at the boundaries of nonnulls (explicit or implicit).

On that, One problematic method though is Objects.requireNonNull. the whole point of the method is to take something that is nullable and then throw an error explicitly. I use it in lieu of the JDK feature that would be nice to have.  There's kind of a problem currently. The way I resolved it because I use nullaway is simply to have tests use a warning for null dereference. The problem is basically testing, for those that don't use a tool there's not really a great way to avoid an NPE; but it's better to have one at the boundary.

> It seems likely that the solution is going to be partial files in Java source format (similar to what the Checker Framework uses) but with a way to preprocess them into a form that is more performant at runtime (like NullAway has)

I'm assuming that none of the tools out there are using anything in common yet?? Simply commenting/ asking because I noted a method in the JDK that wasn't marked properly by nullaway the other day. It's since been fixed although I don't think there's been a release. My experience with the way that checker framework was doing it was kind of frustrating because no IDE really supports their format. Of course the big concern here is that we really don't want all of the tools doing it themselves because then the effort is just duplicated, and different tools will have different coverage of the JDK, and maybe other libraries.

As sort of another note on third party libraries. I feel like there should be a common way to support common libraries that haven't added any kind of null annotations. I'm looking at you Apache Commons... Since otherwise obviously every tool is probably going to ship the JDK stuff.

[Chris Povirk]

If I have one other thought on the JDK implementing this later on down the line it would be that it would be nice to have it auto throw runtime errors at the boundaries of nonnulls (explicit or implicit).

Yeah, I'm hoping that it can be done that way, too, at least optionally if it's too disruptive to turn on everywhere. (My sense is that Valhalla might force it in some places, but maybe even going that far will be too disruptive? I haven't followed that as closely as I might like to.)

There was a neat paper (one of whose authors passed it along to us) that rewrote bytecode to detect where to add annotations. I've also seen but not tried this instrumentation tool.

On that, One problematic method though is Objects.requireNonNull. the whole point of the method is to take something that is nullable and then throw an error explicitly. I use it in lieu of the JDK feature that would be nice to have.  There's kind of a problem currently. The way I resolved it because I use nullaway is simply to have tests use a warning for null dereference. The problem is basically testing, for those that don't use a tool there's not really a great way to avoid an NPE; but it's better to have one at the boundary.

Objects.requireNonNull has been the subject of multiple discussions over the years... :)

We have:

public static <T> T requireNonNull(@Nullable T obj)

So, as far as our annotations are concerned, `requireNonNull(nullableValue).bar()` is fine. Tools may still elect to treat requireNonNull specially.

And in fact we hope that tools will conclude that the `nullableValue` variable is non-nullable after that call, too. We don't currently provide a way to express that, but I think that tools that analyze Java source generally already have a special case to recognize that method.

I feel like there have been yet more questions about the method, too. Does any of that speak to your concerns?

> It seems likely that the solution is going to be partial files in Java source format (similar to what the Checker Framework uses) but with a way to preprocess them into a form that is more performant at runtime (like NullAway has)

I'm assuming that none of the tools out there are using anything in common yet?? Simply commenting/ asking because I noted a method in the JDK that wasn't marked properly by nullaway the other day. It's since been fixed although I don't think there's been a release. My experience with the way that checker framework was doing it was kind of frustrating because no IDE really supports their format. Of course the big concern here is that we really don't want all of the tools doing it themselves because then the effort is just duplicated, and different tools will have different coverage of the JDK, and maybe other libraries.

Maybe sorta kinda... but basically no. A big reason that we did things the way we did in Google was that we wanted a solution that didn't require tools to do anything to take advantage of the annotations: The annotations are just there like in the class file, exactly like any annotations that were compiled in the source code would have been. That seemed likely to be the only way to improve Kotlin's coverage, and it helps other tools for free.

But the work we did to put the annotations into the JDK APIs isn't published externally. (Maybe someday?)

NullAway has expressed interest in trying to use our JDK information somehow, but I don't think much has happened yet.

As sort of another note on third party libraries. I feel like there should be a common way to support common libraries that haven't added any kind of null annotations. I'm looking at you Apache Commons... Since otherwise obviously every tool is probably going to ship the JDK stuff.

Yep, the theory is that such libraries should actually be the easy case, relative to the JDK (which requires more messing with the module system, among other things) :) I know that the Checker Framework, Eclipse, and probably others have some information for some third-party libraries. (We have a smattering of our own inside Google.) But I don't know quite how much anyone has, and of course there are a lot of libraries out there. Another part of the story has to be making it easier for library owners to add actual annotations when they're up for it, but there will always be ones that don't want to make or even accept such changes, so we need an answer for them, too. Our expectation is that the same approach of Java source code + preprocessing will be at least part of the answer.

[Caleb Cushing]

The problem of course is that that third party information isn't currently shared in any way. There's way too much duplication of effort currently.  if I'm using one tool but not another I don't get the benefit of those other libraries. So I'll be honest that I see this as a real requirement for any sort of general solution.

Also, it feels like maybe there needs to be a guide on what library authors might want to do if they don't want to add the dependency. Yay yet another library. I personally don't care and I'm happy to add a dependency. Most of the tooling these days recognizes nonnull and nullable, So for now I'm just marking every single thing since it seems likely that it's going to be the only thing that actually works consistently across all tools (Right now). I'm not entirely certain if I need to mark fields though... If all my public boundaries are covered.

[Chris Povirk]

If we can get to the point at which we have a way to share the information across tools (by making it easy to write it into existing class files and/or preprocessing it into formats that tools already recognize), then that should at least somewhat encourage the collection of more information into one place. And we should be able to build out some of the information automatically from bytecode or source code (example). I don't expect us to get anywhere close to coverage that is universal or even particularly acceptable to an average user who is looking for near-soundness. But we've got to lay what groundwork we can, and every bit of information helps, especially in common libraries. That can be true sometimes even for users who aren't using a "full" nullness checker. (Like, IntelliJ can give you warnings for dereferences of random APIs without breaking your build or forcing you to annotate everything.)

I think we do have a work item listed somewhere for a guide for what to do if you can't/won't annotate a library directly. We might also have an item about the idea of annotating only your public API, which is definitely something that we anticipate people will do. (It's what we've mostly done for the JDK.) There is still a lot to be written, sadly....

[Manu Sridharan]

Just a note that on the NullAway side we are actively working on a way to translate the annotations from the jspecify/jdk repo into an astubx format that NullAway can use.  It’s my goal for NullAway to eventually get rid of its hacky support for JDK library models and go with importing jspecify/jdk instead.  I hope to have concrete progress on this in the next month or two.

Best,

Manu

--
You received this message because you are subscribed to the Google Groups "jspecify-discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to jspecify-discu...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/jspecify-discuss/CAEvq2nod%2B24dMu5ACVNAWKVCzUyAapt3yabZcd%3DS-68Yr4%2Bnaw%40mail.gmail.com.