Address the "findViewById problem" (generally nullable, but in *common* specific cases not)

[cpovirk]

We've discussed using @NullUnspecified as a way of saying something like "a smarter tool would be able to tell you when this is safe" -- or just "this method is used commonly enough that some users/owners are unwilling to tolerate null checks on every call size." See this earlier discussion from when we discussed using a @LessEnforced annotation for this and this even earlier discussion.

There are a number of places that this could be useful. Rather than dumping these into #32 (as I did recently), I'll start a new bug with a list, carrying over items from past discussions:

Possible usages for @NullnessUnspecified on return types:

• Map.get
• Activity.findViewById (rough stats on how often callers perform a null check on the result)
• Context.getSystemService
• Fragment.getContext
• Throwable.getCause
• ResourceLoader.getClassLoader
• Thread.getUncaughtExceptionHandler
• HttpMethod.resolve
• DateTimeFormatterFactoryBean.getObject
• Map.Entry.getValue: technically "undefined" if the entry has been removed, but some implementations return null in that case. Checker Framework leaves it returning V, but we could switch to @NullUnspecified V if we wanted to be paranoid.
• Matcher.group(int)
• Injector.getInstance()
• various reflection APIs

Possible usages for @NullnessUnspecified on parameter types:

• Joiner.join
• MoreObjects.firstNonNull? (Or maybe we'd consider this like checkNotNull, for which we might allow null inputs that might result in a NullPointerException?)
• Collection.contains?
• requireNonNull / checkNotNull?
• various reflection APIs

Another category of use cases is @PolyNull, whose status is up in the air. I've compiled a list of @PolyNull methods.

(I got to wondering if an evil way to support @PolyNull without @PolyNull would be to allow stubs to contain 2 versions of a method -- so one could include @Nullable and the other not. This might work, but it would probably require special rules, and anyway, it would require stub files for a library, while we want code to be annotated inline -- and we especially wouldn't want it to be mostly annotated inline but with magic elsewhere.)

[kevinb9n]

I just want to reassert that I think condoning the use of @NullUnspec for these methods should be a last resort, to be avoided if at all possible.

I think all these type usages are nullable. Then we've done everything we can do via the avenue of a type system to prevent errors. Analyzers can always do more.

[cpovirk]

Even Map.get? My impression was that you were fairly recently in favor of using @NullUnspec there (and presumably in the similar Android cases).

[kevinb9n]

I would not describe myself as ever having been "in favor" of it, so much as against defining a fifth kind of nullness. And musing aloud on the question of how much we should try to account for the fact that even if we declare @Nullable as the right way to go many users will still go this route anyway since it might appear to do something like what they want. I don't feel good about @NullUnspec on Map.get at all.

[cpovirk]

Oops, sorry, thanks. I think my belief was based on remembering that you'd closed the @LessEnforced issue in favor of @NullUnspecified, apparently backtracking on your hope to support "cop-out" use cases without @NullUnspecified.

But it sounds like your position is that Map.get is clearly @Nullable, as are the Android cases, but you're willing to live with the Android team's decision to apply @NulUnspecified instead, since we're not likely to provide another way to get the behavior they'd like?

[PeteGillin]

When you talk about Map.get, you're talking about the return type, I guess? Because there's also a slight question mark over the parameter type: the spec allows get(null) to NPE, and it does for ConcurrentHashMap. I guess there's still no reasonable choice for Map except to say that its argument is @Nullable Object. That raises the question of whether CHM.get is allowed to take @NonNull Object, which is accurate but would be an illegal override if we really treated nullability like a type hierarchy. But maybe that's a different question to the one that this bug is addressing.

[PeteGillin]

One method that I think should be added to the list for this issue is Thread.getUncaughtExceptionHandler(), which returns null but only if the thread has terminated. In Android, I made its return type nullable, which broke some folks legitimately not checking for null because they know the thread is running (e.g. because it's Thread.currentThread()).

I guess that Thread.getThreadGroup() is the same.

[stephan-herrmann]

But it sounds like your position is that Map.get is clearly @nullable, as are the Android cases, but you're willing to live with the Android team's decision to apply @NulUnspecified instead, since we're not likely to provide another way to get the behavior they'd like?

Since Map.get clearly mentions the null case in its javadoc, I don't see a way around a @Nullable V return type. If google likes to help users for a particular application of Map where it is possible to analyse if a given key "exists", then they are free to define a new subtype of Map with a different contract. Users of platforms other than Android should really not suffer any additional complexity due to this one use case.

[PeteGillin]

I think there's been some miscommunication. Android, AFAIK, does indeed declare @Nullable V get(@Nullable Object). I don't think we consider ourselves special in this case. I know that there are some folks (not Android-specific) who would prefer to be more liberal. I'm pretty sure that Android will go along with whatever the consensus is here.

There are some interesting Android-specific examples, such as the return type of Activity.findViewById(int). The overwhelmingly common way of using this is to pass in a constant defined in generated code as its argument, e.g. findViewById(R.id.toolbar), and it is guaranteed to return non-null when you do that. For anyone following that pattern, which is practically everyone, requiring then to do null checks adds friction. But it is formally speaking nullable, because it returns null for other arguments.

[kevinb9n]

Back to the Map.get key parameter type: that's a nasty one, but I think the best we can do is to say that some implementations are kinda "doing it wrong". They should arguably reannotate the key to @NotNull and suppress the warning that results just in case someone is actually speaking directly to that static type; on the other hand, maybe we don't want to encourage that kind of thing.

[cpovirk]

Anecdote from @dzharkov:

In Kotlin, [Map.get] always had a nullable return type and users used to it.

Naturally, as he also points out:

But for Java users, it might be paintful because there's already a lot of code that doesn't check returned value and that code doesn't fail because the user somehow is sure about it.

But I think this is overall yet more encouragement to make get return @Nullable.

I don't think we're in danger of making any kind of binding decision here, but I would say that, if people feel strongly the other way, it would be good to hear about it at their convenience. If we end up using @NullnessUnspecified more widely than anticipated, we might want to take that into account while we make decisions about its semantics.

[cpovirk]

We have a small internal discussion going about Matcher.group(int) and group(String). They're another case in which @Nullable is clearly correct but probably inconvenient in a large fraction of cases. I doubt this is fundamentally different than Map.get, though.

[amaembo]

Yes, we don't annotate Matcher.group methods as Nullable. A sophisticated analysis could be done to check whether the original pattern contains alternating groups, but this is out of the scope of our project and cannot be always determined statically. I agree that the problem is not substantially different from Map.get.

[cpovirk]

I was talking to @kevin1e100 yesterday, and he mentioned a trick that might apply here: using aliases.

Instead of making Map.get return @NullnessUnspecified V, we could make it return @NullableUnlessKeyPresent V, where @NullableUnlessKeyPresent is an alias for @Nullable. This is equivalent to directly annotating it as @Nullable V -- with one important exception: Tools may provide a way for users to silence or downgrade errors from the specific aliases they choose[*].

I have a couple follow-up thoughts, but I'll put them in separate posts.

[edit: Update: In my second follow-up thought, I end up not liking this idea much anymore.]

[*]: The use case for aliases that kevin1e100 and I were discussing was migration (#26, Kotlin support): When library owners adopt jspecify annotations, they might choose to annotate their code with a custom annotation like @RecentlyNullable, rather than with @Nullable itself. Then, when users upgrade to the new version of the library and see errors from the new nullness information, they can turn those errors off without disabling all nullness analysis.

[cpovirk]

Follow-up thought 1:

As I hinted in my previous message, the aliasing approach lets us define different "kinds" of unspecified nullness, each of which users may handle as strictly as they like. So we could have:

• @NullableUnlessKeyPresent for Map.get, Table.get, etc.
• @NullableIfRegexGroupIsRequired for Matcher.group, etc.
• etc.

Then each team could decide which should be errors for their codebase, given the kinds of operations they tend to perform and their risk tolerance.

However: Would we really want to provide n annotations in our artifact (or even in a separate artifact)?

• We are sure to be in for many discussions about whether each new use case is sufficiently different from the existing ones to justify a new annotation.
• Our users may have to have similar discussions about their own APIs.
• At some point, some users will worry about binary bloat from so many annotations.
• The large number of annotations may intimidate and confuse users. (But maybe it's still less confusing and intimidating than having a common method like Map.get return @NullnessUnspecified V, if anyone is advocating for that?)
• Many users will just want to turn off "all those optional errors," without having to turn off n different kinds. (Maybe we can still make this possible, like by putting all these new annotations in a subpackage and asking tools to let users say "Ignore everything from this package?")

So maybe users who want this level of control should just write stub files. (We could even host stub files that are commonly requested, similar to what the Checker Framework does. However, this would require that we settle on a stub format that all tools are required to recognize.)

[cpovirk]

(This next post is long and definitely skippable -- not that you need my permission to skip anything I post :))

Follow-up thought 2:

• How much does the aliasing approach reduce the need for a type annotation @NullnessUnspecified -- or at least let us define @NullnessUnspecified as an alias of @Nullable?
• How much does it let us treat the general concept of "unspecified nullness" as "nullable, but only if the user wants it to be?"

My thinking so far:

• We could mostly get away with making @NullnessUnspecified an alias for @Nullable. But I don't think I'd recommend it, in part because:
• It definitely can't explain the whole concept of unspecified nullness.

The easiest way to see the problem is by comparing @NullnessUnspecified on return types to @NullnessUnspecified on parameter types.

Return types: Consider Map.get. Its return type is "conditionally nullable," so we could annotate it @NullnessUnspecified. Users can then choose to treat it as @Nullable (which prevents them from dereferencing the result) or to ignore it (which lets them dereference the result).

Parameter types: Consider Method.invoke: Its parameter type is "conditionally nullable," so we could annotate it @NullnessUnspecified. Users can then choose to treat it as @Nullable (which lets them call invoke(null)) or ignore it (which forbids invoke(null)).

But wait: These two are backward from one another! A user who wants "strict" checking wants to treat Map.get as returning @Nullable but Method.invoke as requiring non-null. But this is impossible if all the user has is a switch to either turn every @NullnessUnspecified into @Nullable or else ignore every @NullnessUnspecified.

To get universally strict (or universally lenient) handling:

• Our tools need to ask "Would the code work with if we replaced @NullnessUnspecified Foo with either @Nullable Foo or just Foo?"
• For cases in which only one of those possibilities is valid, our tools need to let users specify whether to issue an error or not.

So: Making @NullnessUnspecified an alias for @Nullable "works" for the return-type case but not the parameter-type case. It's asymmetric.

I do think that, in practice, @NullnessUnspecified will be more commonly used for return types. So we might be willing to accept that we can use it only there. But we are still going to need a concept of "unspecified nullness" for parameters (and return types) in unannotated code. And once we have that, I think it would be confusing to also provide a similar but distinct way of handling certain other return types.

(Users might still be able to take this aliasing approach themselves if they want to, but we would probably recommend against it.)

[edit: Forgot to add: We could consider having 2 separate @NullnessUnspecified-like annotations, one for parameters and one for return types. But this is yet more complexity. In particular, it feels like what Kotlin provides is a way to say "Don't report nullability errors for this API," but we'd be abusing it as a way of saying "Don't permit nulls in this API." I'm not even sure that Kotlin's feature would do what we want, and if it does, it's confusing.]

[mernst]

Here is an issue related to having different types of @Nullable. (It might be the same as what Chris bringing up -- my thoughts on this were inspired in part by discussions with Chris. But it makes no mention of unspecified nullness, so maybe unspecified nullness is orthogonal this this issue, or maybe I don't deeply understand what unspecified nullness means.)

Consider a method like Field.get().
There are situations where passing null yields no NPE, and there are situations where passing null yields NPE. (It depends on whether the field is static or not, but but that is not relevant to this discussion.)

A sound verification tool needs this method to be annotated as

  ... get(Object obj) { ... }

The tool issues no false negative warnings (as a sound tool must) because it issues a warning whenever the argument might be null. However, it does issue false positive warnings.

A bug-finding tool that aims to avoid false positive warnings might prefer the annotation

  ... get(@Nullable Object obj) { ... }

Put another way, a bug-finding tool might want to treat these methods differently:

  void m1(Object arg) {
    if (...)
      arg.toString();
  }

  void m2(Object arg) {
    arg.toString();
  }

The bug-finding tool might want to issue a warning whenever null can flow to m2, but issue no warning when null can flow to m1. We don't have a way to express that in our annotation language.

[cpovirk]

Yep, that is one of the cases we have in mind. (I don't think I'd see it defined that simply before, so thanks.)

Your case is about parameter types. The other main case is with return types, and I don't think it's even possible to define precisely. It's more of a case-by-case question: If we force callers of this method to null-check the result before dereferencing it, what percentage of the time will that catch a bug? Our main example here is Activity.findViewById(int id): It's an Android method that returns null if there's no view with the provided ID. But the method is frequently called with a compile-time constant whose value comes directly from the views defined for the app. So in practice, some users complain if they're forced to check the result for null -- even if those users normally like having a checker that looks for nullness bugs.

So we consider annotating the return type as @NullnessUnspecified T, which effectively lets users choose whether to treat it soundly or not. This, of course, has downsides:

• This is a slippery slope.
• We might prefer for library owners to improve the APIs themselves, rather than for us to accommodate the quirks of the APIs as they are today. (Even if such APIs aren't available, users can often write wrappers.)
• @NullnessUnspecified may be intimidating and confusing to users.

I have one other thing I've been meaning to say about @NullnessUnspecified T as a return type. I'll save it for a separate post. First, I think I'm going to go back and organize the list in my first post into sections, one for parameter types and one for return types.

[cpovirk]

Some thoughts about @NullnessUnspecified T as a return type:

One way that we could make things easier on users is to have at least one method like requireNonNull that permits a @Nullable argument. (This is one of the topics discussed in #29.) Now, this would mean that the method could throw NullPointerException -- and I'd really like for there to be a method like requireNonNull that can't throw NullPointerException (unless called from unchecked code). But it would let users perform the check they need more easily. And that might be a net win if it means users will accept a @Nullable return type on methods like Activity.findViewById and Map.get: That way, users are at least forced to check for null in a fairly explicit way.

Aside: Map.get is an interesting case when it appears in generic library code: Map.get returns a @Nullable V, but sometimes the library may know that it's safe to convert to "plain V." Normally, the library would do this by checking for null and throwing NPE, just to be safe. But sometimes that's not the right solution: The library might be permitting users to specify V itself to be a nullable type! In that case, they don't want to throw if the map happened to contain a null value.

So they have to suppress the nullness warning. That's the best I can imagine doing in that case. It's just also a small argument that @Nullable T can be more of an inconvenience to users than @Nullable Foo, at least when T might be specified to be a nullable type.

Fortunately, most "normal code" won't encounter this issue often. We did see it in Guava occasionally, but Guava is weird. (We would have seen it more in Guava, but the Checker Framework's @KeyFor helped in most cases.)

[mernst]

The name @NullnessUnspecified confuses me because it suggests that no one has yet considered how to annotate the code -- somewhat like "legacy code".

Can we think of a better name? Here are some suggestions.
@NullableUnspecifiableByJspecify
@NullnessUnspecifiable
@NullableSometimes
I think they are better than the current name, but I would welcome suggestions of even better names.

[cpovirk]

I dug up a past thread on the topic of naming, and I've quoted you and replied there.

[cpovirk]

@kevin1e100 pointed out today that, for Kotlin users, parameters really need to err on the side of being @Nullable.

Suppose that Collection.contains is instead annotated to require a non-null argument. Not only will Kotlin not let make you call collection.contains(null), but it will also not give you a way to suppress the resulting error. And, if you attempt to work around this in various ways, Kotlin will often insert runtime null checks before your call, making it throw an exception. (There's probably some way to make it work, even if only with a Java wrapper, but it would be ugly.)

This heightens the conflict between Checker Framework users' desire for sound annotations and Kotlin users' desire for flexible ones. And as everyone reading this thread is probably already aware, we have conversations on this topic underway.

[cpovirk]

Also on the subject of Kotlin: I was starting to worry about how hard it was to convince Kotlin that a T? (where T is some unbounded type variable) is actually a T when you "know" that this is safe. This would be relevant for cases like Map.get if it returned a V?.

It turns out to be easy:

@Suppress("UNCHECKED_CAST")
class Foo<T> {
    fun go(t : T?) : T {
        return t as T
    }
}

[kevinb9n]

I want to sort of "insist" :-) that we please retitle and reframe this issue. I think we need to remember very solidly that:

1. If we extend the type system to account for null inclusion/exclusion, we'll have done a lot of good.

2. That will be quite hard enough to get done as it is.

3. These cases listed above, as types, are all nullable, plain and simple.

4. We always take as granted that our annotations are one source of information that a nullness analyzer will consult when making its decisions of what to report and how. There is nothing stopping it from having additional smarts that cover the nuances of the cases listed above. Those smarts might depend on custom annotations. Those annotations might use our @Implies if we provide it. Or they might not.

5. Every time a user voluntarily sticks with unspecified, or makes their own annotation @imply unspecified instead of nullable, I will shed a tear, because I think this is wrong, but what can you do? That annotation represents the withholding of all information. If they don't like what their tools are doing with the information, they're allowed to withhold it.

I want to push back on the idea I've been hearing that there are "kinds of nullness that are too complex for our annotations to be able to express". I think that's not the right mindset. A (non-type-variable) type usage is either nullable or not (well, or legitimately unspecified), just like an integral type is either int or long. The type must include the union of all values that ever might come through. Now there can be any manner of additional knowledge someone could code up about which values of that type it can actually take on in real life and in which circumstances. Maybe someone will even bring "refinement types" to Java (shudder). But this really shouldn't be our concern in this project.

Post-1.0, however far off that is, sure, we could always talk about this again.

Can everyone live with this? If there's an objection that's sticking in your mind that won't go away easily, then sure, let's have that out.

[cpovirk]

I had 2 small realizations around this. They may be old news to people:

• If Map.get were annotated as returning @NullnessUnspecified V, then implementations of Map.get would produce errors if compiled by a strict tool. That feels wrong.
• In principle, it make sense for an extremely strict tool (probably one run during tests only) to be able to insert runtime checks on any value whose type is not annotated @Nullable (with appropriate handling for type-variable usages based on their bounds). Such a tool would reject null values returned from a method like ImmutableMap.get. This also feels wrong.

[kevinb9n]

The feeling has continued to gnaw at me that we will have to have some reasonable approach to this case by 1.0 (but not by 0.3).

It could be just advice for users that is almost satisfying while being better than "leave it unspec". If such a stance exists.

My concern is that without this, users will have irritating experiences that will get disproportionate attention.

[kevinb9n]

Hello from 18 months later. I think it's now fair to assume we won't have anything special for this case in 1.0. I'm moving to post-1.0, and filing a separate doc bug for what to do in the meantime.

[netdpb]

Current decision: JSpecify 1.0 will not explicitly address this problem.

Proposal for 1.0: Finalize the current decision. If you agree, please add a thumbs-up emoji (👍) to this comment. If you disagree, please add a thumbs-down emoji (👎) to this comment and briefly explain your disagreement. Please only add a thumbs-down if you feel you can make a strong case why this decision will be materially worse for users or tool providers than an alternative.