What to do when overriding method's annotations indicate weaker contract than overridden method [working decision: finding of distinct category]

[kevinb9n]

We seem to lean toward allowing covariant return types and contravariant parameter types (in the nullness dimension). These are ordinary contractual refinements [EDIT: strengthenings]

I want to discuss backward refinements [EDIT: contractual weakenings]: covariant parameters and contravariant returns. Surprisingly, I'm going to claim these are also valid.

Scenario A: Foo.bar() has a non-nullable return type. SubFoo.bar() should not return null in any case, but for whatever reason, its author has decided to do so and no one will change their mind. (This situation could also arise from Foo changing after the fact.)

From jspecify's point of view, I think that @Nullable is the only correct way to annotate the return type of SubFoo.bar(), and the user should absolutely do so. That way, at least consumers who happen to have the static type SubFoo will behave correctly, and that is better than nothing.

From the "what our annotations mean as specification" perspective, there is nothing wrong here. It's just that from the "preventing bugs" perspective, any reasonable checker is going to want to issue a warning on SubFoo.bar(), explaining that it risks causing an NPE for anyone using SubFoo via its Foo supertype, and strongly recommending against doing this. It should also suggest considering modifying Foo itself, but we have to realize that such decisions tend to be made more on annoyance equilibrium than on correctness.

(I would hope that if the user just changed the SubFoo.bar() return type but left the code alone, they would get louder/worse errors for that, as that's the worst case.)

Scenario B: a covariant parameter type. Foo promises to accept null, SubFoo doesn't want to. Perhaps this case is slightly different: SubFoo has the option of just still declaring @Nullable, since it's allowed to throw NPE or any other exception for any reason it wants to. However, it still shouldn't, because it's withholding useful information from the callers who happen to have the SubFoo static type. So I think it works out similarly the Scenario A anyway.

[mernst]

Let's please use standard terminology "weakening" and "strengthening" rather than making up new terms like "contractual requirement" and "backward refinement".

When a subtype specification is weaker than a supertype specification, then the specification is ill-formed. This is one of the few situations where every tool should issue a warning, analogously to writing @Nullable @NonNull.

[kevinb9n]

Thanks Mike; that works as an assertion of your position, but I've explained why I believe it is not ill-formed, so which part of my argument are you disagreeing with? [EDIT: my mistake: I meant to discuss whether this is a well-formed usage of JSpecify; which adjectives we use for the user's own subtype specification isn't what I cared about.]

I don't think the comparison to @Nullable @NonNull holds much water; that is a single type at war with itself, literally answering a single question "yes no". Basic well-formedness should, I think, be a very low bar, which that still manages not to clear.

I don't see how this case is similar. It is a "bad move" to weaken a supertype contract, but it happens. Given our premise (that the user will not be talked out of their decision to sometimes return null), then the best outcome (if they can't change the supertype) is for them to annotate their return type nullable. It is then honest about the weird thing they are doing. It can't be both the best thing for them to do and ill-formed at the same time.

I don't see a need to dictate that tools should warn; I would simply be surprised if they didn't. If I was tempted to dictate anything, it would be "make sure the warning is somehow less severe than if they declare a non-nullable return type but still return null anyway", because I think that's the worst outcome.

[cpovirk]

This is going to be a contentious discussion in the best of times. And based on my own experience and what I've heard offline from others, I think that some of us bystanders have been confused about what we're discussing here. So I'm going to take a stab at clarifying that.

For starters, we're talking about methods like Collection.contains(Object). But I'll use a slightly different example, Map.containsKey(Object) (courtesy @PeteGillin). It makes a good example because at least one well-known overriding method, ConcurrentHashMap.containsKey(Object), throws NullPointerException if called with a null value.

Here are some things that I think we all agree on:

1. Some users might like to pass a nullable parameter to the containsKey method of an object whose static type is Map. Those users might or might not want tools to issue warnings or errors when they do, and we might have our own disagreements about that. My only claim is that some users will ultimately want to have that call in their source code (perhaps with @SuppressWarnings applied to it). I contrast this case with...
2. Users definitely never want to pass null to the containsKey method of an object whose static type is ConcurrentHashMap.
3. Given (2), the parameter type for ConcurrentHashMap.containsKey that we'd recommend is @NonNull Object.
4. Suppose that someone declares ConcurrentHashMap.containsKey(@NonNull Object), as in (3). Now additionally suppose that that person declares Map.containsKey to have a parameter of @NullableObject. In that case, when tools compile the annotated ConcurrentHashMap class, we would recommend issuing some kind of error/warning. This would inform the developer about the mismatch between the parent and child classes' signatures for the method.
5. We also agree on the behavior we'd expect from tools when analyzing both callers and implementations of containsKey:
   • Callers of containsKey(@NonNull Object) are likely to see warnings/errors if they pass a nullable parameter. (And, if the parameter type is @Nullable Object instead, they aren't likely to see warnings/errors.)
   • Implementations of containsKey(@Nullable Object) are likely to see warnings/errors if they dereference the parameter without a null check. (And, if the parameter type is @NonNull Object instead, they aren't likely to see warnings/errors.)

To summarize all that: However developers annotate these methods, I think we all agree on how tools are likely to respond. (Aside: There is still disagreement about what exactly our spec/docs should say to encourage such behavior without requiring it. But I think that disagreement is mostly unrelated to this current specific issue.)

The disagreement, then, is: How should developers annotate the parameter of Map.containsKey -- @Nullable or @NonNull? Compared to the various things we agree on, this disagreement is either less fundamental or more fundamental:

The argument that it's less fundamental: All we're debating is how we recommend that our users apply annotations. At most, we're debating how we'll apply annotations to containsKey specifically when we provide an annotated JDK. This is important, but it's mostly a discussion about what we suggest to users, not what we do in our specification and tools.

The argument that it's more fundamental: What we're really discussing here is the meaning of @Nullable (as previously discussed in various places). If we can't tell users when to use our most basic annotation, then how can we feel comfortable telling users anything?

I have Opinions on this, but for now, I want to stop and see if this clarified anything for anyone.

[kevinb9n]

(To be clear, we're using Map and CHM as examples here, so don't be distracted by issues that come from their JDKness.)

Your background looks spot on. But I think the question being asked first is not what Map should do, but rather, assuming that Map declares the parameter to be nullable, then what should ConcurrentHashMap do? And what will motivate it to do that?

I think that non-nullable is the right way for it to go, because it is truthful. The specification will appear to violate substitutability because the implementation DOES violate substitutability. Also because for the users who happen to have the specific static type they will get proper behavior. (Of course, an implementer of such a method may mistakenly think they have some kind of assurance that the value can never be null, but that is already wrong anyway, since the caller might not be null-checked code.)

So I'm advocating that we view this as a well-formed expression of contract... which happens to be bad contract. The problem report that a user gets should explain the dangers, but the hope is that if the user tried to paper over the problem by just changing the annotation, they should get much scarier sounding errors then.

[kevinb9n]

Then, the question you appear to be asking is, should Map have done this at all, if it knows there is even one implementation like this that won't adhere to the contract?

And I think the answer can't be an absolute no (which doesn't erase the problem just discussed anyway). And in real life API owners will probably go whichever route seems to cause the least aggregate aggravation.

[cpovirk]

I agree that we could further discuss what CHM should do if it has to cope with Map.containsKey(@Nullable). My belief, though, is that everyone already agrees on what it should do in that case. Specifically, our position seems to be that CHM should define containsKey(@NonNull).

I do think it's logically defensible to take a different position than that, and I invite anyone to do so. If not, that's fine, too: Easy issues are the best issues :) I just want to make sure that:

1. We don't spend a lot of time violently agreeing with one another.
2. We understand where the disagreements that do exist lie.

I have been particularly concerned about (2). On that note: Bystanders, please do speak up if you disagree with anything that I've claimed "everyone" agrees with. I'm not trying to cut off any lines of discussion, only identify the discussions that someone wants to have.

[kevinb9n]

I feel like we're descending into details that are making this question seem complex and specific, but I want to try to establish something more simple and general:

I propose that it's valuable for us to separate the idea of "invalid application of jspecify annotations" from the idea of "valid application of jspecify annotations, which correctly enables tools to see there's some problem in the code".

The impact to the end user might seem slight -- they'd probably see a warning either way, and it might just be worded a little differently -- but I think we in this group need to differentiate carefully or it will get too hard to have these discussions.

An example of something that is definitely an invalid usage of jspecify would be annotating a type @Nullable @NonNull. There can be no possible reason to allow that. That is ill-formed on its face.

I believe a parameter having some different nullness from its superparameter can never be put in that "ill-formed" bucket, because there is already code out there that is doing this. That code should be annotated truthfully. When it is, those annotations may reveal a deeper problem to tools or they may not. Was a parameter made less nullable than its superparameter -- a weaker contract? I expect roughly all tools would want to complain about this; does jspecify even need to tell them to?

What if the contract is made stronger (parameter more nullable than superparameter)? If we could agree on the above, then the nature of issues like #49 changes a little. It's not about "should we support parameter contravariance?" because that just is supported by default. And I would be surprised if any tools cared enough to complain about it (unless it is a specific kotlin incompatibility that motivates them to do so). Seems like they are free to do what they want.

[cpovirk]

To help make the distinction, maybe we can find words other than "ill-formed" and "valid."

Perhaps what you're proposing is that @Nullable @NonNull String does not express a type? In contrast, the case here with overrides definitely expresses types, just ones that, taken together, might be questionable in some way.

Would "does not express a type" cover all the cases you're putting in your "invalid application of jspecify annotations" bucket?

[kevinb9n]

That feels like an attempt to nail down exactly where the boundaries lie. That might be too hard to do all at once. I think it's enough if we can agree that the boundary should exist. And in trying to decide which side of that line this particular scenario falls on, some principles may start to emerge. For instance, I've suggested "if there can already exist code for which a certain application of annotations is the most truthful expression possible, then we should never consider that ill-formed".

[cpovirk]

I've taken a stab at an issue title that asks whether there is a hierarchy of 2 levels of badness, since that seems to be the root issue. Alternatively, if you'd like to keep this issue specifically about which level we put contractual weakening into, we could open a separate issue for the "2 levels" question and then try to resolve that one first.

[kevinb9n]

I'm not sure this is really a question of degree.

The goal of our annotations is to capture small pieces of information from the developer. @Nullable @NonNull fails to do this (even if we defined a precedence, it would still fail to be a proper and useful way to express whatever information we defined it to express). No matter how low we define the standard for well-formedness it still shouldn't meet it, because it is like answering a question "yes no". I hope this part is not controversial.

It's hard to debate and settle a question of "is there another kind of badness" per se. What we can do is talk about examples of other problematic scenarios and decide which bucket they fall into. If one by one they all fall into the same total-nonsense bucket then we would eventually say we only needed one category. So far we've discussed one example, and I've explained why it doesn't fit in the same bucket: we would be rendering some existing code impossible to annotate.

Do you want to go through other examples too, or....?

[cpovirk]

I'm now confused about the buckets. Maybe I'm envisioning that every case that a checker might warn/error about goes into 1 of 2 buckets, while you're talking about only a subset of cases?

The 2 buckets I'm picturing are:

Bucket 1: "the @NonNull @Nullable Object case":

Possibly @NonNull @Nullable is the only thing I see in this bucket currently. I could also imagine including cases like @Nullable int, which falls under the umbrella of "structurally illegal" (though that umbrella covers many of things): You were expected to provide either 0 or 1 annotation (or, in the case of @Nullable int, you were expected to provide 0), but you provided more.

Maybe the key idea here is that this one single type declaration is wrong in isolation: Even if we know nothing else about any type in the program, we can identify the problem.

Bucket 2: "type mismatches":

This is my "everything else" bucket:

• returning null from an implementation of toString()
• declaring ImmutableList<@Nullable Object>
• overriding a method that returns List<@Nullable Foo> to return List<@NonNull Foo>
• etc.

This bucket contains cases in which we applied some type check / conversion / predicate to 2 types, and it failed.

---

I sometimes have gotten the impression that you're picturing a third bucket. It sounds like it might take some things out of my second bucket on the grounds that "we would be rendering some existing code impossible to annotate." I am also confused about the "impossible to annotation" question, but maybe we can get to the bottom of the buckets first?

[kevinb9n]

I feel hopeful that this conversation can get simpler than it has been, somehow. :-)

We don't have to come up with the whole unified theory of buckets right here. Let's just focus on what is well-formed and what isn't. And our guiding star on that, I suggest, is:

"The purpose of our annotations is to capture valid information from the developer (in a reasonable way)."

@Nullable @NonNull clearly fails to do this, and @Nullable @Nullable is a clearly bad way to do it. These should be considered not well-formed.

I'd like to get this issue back to being just what it started out as, a discussion of whether subtypes can weaken a supertype contract. I argue that this succeeds in capturing valid information from the developer. That valid information allows tools to detect and report a problem, which may be a deeper design issue in the software. This is a good usage of JSpecify that lets JSpecify do its job.

[kevinb9n]

I'll acknowledge that the observable consequence of our decision here might not even be massive. Maybe it's just "six of one". But, if we can't get on the same page conceptually, that seems like ill portent to me. Cmon, we can do this. :-)

My claims are:

1. Code exists, where SuperFoo.bar(Object) promises to accept null but SubFoo.bar(Object) throws on it.
2. This code is problematic because it violates substitutability.
3. Nevertheless, the most correct and useful application of JSpecify annotations to this code is that SuperFoo's parameter is @Nullable and SubFoo's is not.
4. That is accurate, and also provides information that tools can use to report a problem: "SubFoo.bar(Object) parameter 1 should be of type @Nullable Object, because calls to it via the overridden method SuperFoo.bar(@Nullable Object) will be permitted to pass null."
5. Because it communicates correct information about (problematic) code, prima facie it cannot be "ill-formed".

I might be missing all manner of things. But I believe the point I am making is very basic, and I also don't see it being refuted either; however it seems as though each response above tries to branch the conversation hither or thither. (Truth be told, I just wanted to get to say "hither or thither".) Can you help me understand what's going on here? :-) Thanks

[cpovirk]

I'm going to be thinking about this more today, but as a quick response:

The part of that that sits poorly with me is the phrasing "promises to accept null": Yes, we have a method whose parameter type includes null[*], but I'm nervous about describing that as a "promise": The method might do anything when given null, including "throw NullPointerException," just as it might do anything when given 1 or "foo" or Color.RED. Now, the method should have some defined behavior for those inputs. (Or, alternatively, it could explicitly call the behavior unspecified.) But I see that part of the contract as something to explain in Javadoc.

From this point of view, a definitively non-null parameter is a way of saying that the behavior of the method on null inputs is undefined. (Analogy: If a method accepts an Iterable<String>, its Javadoc doesn't need to talk about what happens if you manage to cram an Iterable<Integer> into it.) But if the parameter type can include null, then that isn't a "promise" of anything more than (ideally) to explain what the behavior for that input is.

[*]: Again, I think that there may be actual controversy over whether the parameter type does include null. I am with you that it does. But I have forgotten the state of the wider conversation on this, so I say that there may be controversy because that's not how the Checker Framework annotates its JDK.

[kevinb9n]

Correct that "promises to accept" is wrong. I reached for that word only to express that when we're annotating an overridable method, we aren't just making a choice for the method's own body, we're making contract that constrains overriders. How that constraint manifests, and what remedies it admits, are in a sense what's at issue here. Looking forward to the broader reply.

[kevinb9n]

Still trying to understand what position I'm arguing against (i.e., where a 'no' to my proposal means we end up). My confused guess at it is "there's no meaningful difference between 'wrong usage of JSpecify' and 'correct usage that highlights a problem', or we just don't need to care, or trying to care would get us into more trouble than it's worth". Is that even it?

[kevinb9n]

[NOTE: my pushing on this is not proportional to its importance to the project. No urgency per se. It is just that I don't feel like my mental model is on solid foundations while it's unresolved.]

The following is NOT an actual argument. I'm just disclosing something that I "hope" will end up being the case in most tools. I don't have a guess how relevant it is here.

Suppose we're retrofitting legacy code, and the below is now in null-marked scope:

interface SuperFoo { void bar(@Nullable Object o); }

class SubFoo implements SuperFoo {
  @Override void bar(/*1*/Object o) { ... }
}

We assume most/all tools want to report a problem at 1. Suppose the user thinks "It's saying this is wrong, and I have to add @Nullable to fix it", then when they still get a problem reported in the body, they reason "I'm trying not to change things, just annotate, so I'll suppress on this line of code for now."

Result: now no problem reported at 2 here:

anyClient(SubFoo subfoo) {
  subfoo.bar(/*2*/somethingNullable);
}

And that had represented a real bug, whereas the problem at 1 was "you are doing something super bogus that risks real bugs".

I've hoped that the spec will lead tool vendors to recognize these as two quite different cases (if we must say "levels of badness", okay :-)). Because then it's even possible that they will surface them in correspondingly different ways (maybe 1 as warning, 2 as error, or whatever).

[kevin1e100]

I'd expect tools very well may report /2/, since a nullable argument is passed to a method declared to expect a non-null parameter. Seemingly it would be more work not to report something here, and reporting seems better than not reporting in this case, but ultimately it's a tool decision what to report in implementation code.

[kevinb9n]

I'd expect tools very well may report /2/, since a nullable argument is passed to a method declared to expect a non-null parameter.

No, my scenario is that the parameter had been non-null once, but it was changed to nullable in a half-hearted attempt to "make the tools happy".

Note, the scenario is also contrived, and not posed as an argument that "some terrible thing will happen 100,000 times per day to users!". Only illustrating why the conceptual treatment in https://github.com/jspecify/jspecify/issues/111#issuecomment-862976659 "sits right" with me.

but ultimately it's a tool decision what to report in implementation code.

This is what I believed I was addressing when I said:

I've hoped that the spec will lead tool vendors to recognize these as two quite different cases .... because then it's even possible that they will surface them in correspondingly different ways (maybe 1 as warning, 2 as error, or whatever).

We may have to say this over and over, "we are not dictating what tools must do. but our choices have consequences on what they will want to do, and that matters."

[kevinb9n]

At this point I feel pretty satisfied just having this be a distinct category of finding, "override conflict" -- distinct from "irrelevant annotation" and from "types not assignable". Does that make this issue resolved?

[cpovirk]

Having another category of finding sounds eminently inoffensive :)

I imagine that we'll have more to discuss around:

• any user-facing docs about this
• the more general question of whether the spec makes these sorts of distinctions

But it sounds like the high-order bit is the "just" in your proposal: We get most of what we want by calling this "another category" without additionally trying to take positions on whether a particular way of annotating is "correct," what tools should do, etc.?

[kevinb9n]

Yes.

[kevinb9n]

I propose that it's valuable for us to separate the idea of "invalid application of jspecify annotations" from the idea of "valid application of jspecify annotations, which correctly enables tools to see there's some problem in the code".

The impact to the end user might seem slight -- they'd probably see a warning either way, and it might just be worded a little differently -- but I think we in this group need to differentiate carefully or it will get too hard to have these discussions.

An example of something that is definitely an invalid usage of jspecify would be annotating a type @Nullable @NonNull. There can be no possible reason to allow that. That is ill-formed on its face.

I believe a parameter having some different nullness from its superparameter can never be put in that "ill-formed" bucket, because there is already code out there that is doing this. That code should be annotated truthfully. When it is, those annotations may reveal a deeper problem to tools or they may not. Was a parameter made less nullable than its superparameter -- a weaker contract? I expect roughly all tools would want to complain about this; does jspecify even need to tell them to?

I've now written this up at https://github.com/jspecify/jspecify/wiki/two-kinds-of-analysis

[netdpb]

Current decision: JSpecify-compliant tools must recognize when a method's static return type is not a subtype of that of the directly overridden method, or a parameter type is not a supertype of that of its direct superparameter. (By Java language rules, these types could only vary along the nullness axis.) As always, tools can handle that finding however they wish.

When analyzing a call to such a method, only the nullness information of the static type of the receiver should be considered.

Argument for changing: Such overriding methods are incorrect, and like Java, JSpecify should consider them invalid and require tools to report them as such.

However, the current decision preserves the ability of tools to report such overriding methods as strictly incorrect, but it does not prevent tools from interpreting such methods in any case.

Timing: This must be decided before version 1.0 of the spec.

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.

[netdpb]

I've made that edit, with some small changes.

1. I removed the reference to a distinct category, since we haven't formalized anything about that.
2. I moved the point about direct supermethods into the main paragraph, and made the second paragraph only about analyzing calls to such methods.

[kevinb9n]

The "distinct category" has been the whole point, so I'm a firm thumbs-down for now.

[cpovirk]

I have taken "category" to be a well-defined concept in the conformance tests (not that we have a system fully fleshed out, but I think we understand what a different category means there), but there is some ambiguity as to whether we're also talking about things like @SuppressWarnings strings. (Presumably we can all agree that we're not saying that a tool has to decide either (a) to report to users every finding of a particular "category" or (b) to not report to users every finding of a particular "category.")

[kevinb9n]

We can make clear that we're not talking about suppression keys or anything else. It's just that to be fully conformant a tool needs to be able to assign this kind of inference to a special category we define.

I like this because whatever the tool decides (don't report it, report it the same as other categories, report it differently from other categories), it did so intentionally.