Expressing the "strictness" of enforcement

[wmdietlGC]

Google-side discussions of #2 lead us to the proposal below.
I wanted to write up my understanding of the discussions, to give people a chance to think about this before the meeting on Tuesday.
@kevinb9n please clarify or start with a different issue.

Basic idea

Instead of adding additional nullness annotations or adding attributes to the nullness annotations, we add additional declaration annotations that express the "strictness" of enforcement.

The default is that annotation semantics should be enforced by tools.
Specifically-marked APIs have alternative, more relaxed enforcement, without specifying exactly how that relaxed handling is done.

A conservative tool could just ignore this additional information.
Another tool could turn related errors into warnings.
Yet another tool could use runtime checks for such methods.

The particular checker (type)-annotations always have their precise semantics.
For example, a @Nullable return type means that the method can sometimes return null.
The additional declaration annotation conveys how convenient enforcing the property would be.
For example, if the method is usually expected to be non-null, a tool could chose to not enforce null checks.

Naming

We need to discuss what qualifier names would best express this intent. Some ideas:

• @MoreEnforced / @LessEnforced
• @StrictChecks / @LenientChecks
• @PreventMisuse / @AllowMisuse

Scoping

As the less-enforced status should be used sparingly, we could restrict its usage to method declarations.
We would then also only need one annotation, where the implicit alternative is strict enforcement.

Alternatively, we could allow the annotation on the package/class/method level to allow specifying on all levels of granularity. We would then probably want two annotations to allow to specify possible nestings, e.g. the package is marked as less-enforced, however a class within it is strictly-enforced.

Relation to Migration

#26 proposes an @UnderMigration annotation. We feel that these express two separate dimensions.
Migration is time-bounded, whereas enforcement is about the particular API and will not change.

Strict enforcement and additional checker information

One thing to note: even for a strictly-enforced @Nullable annotation, a checker might have some additional information that tells it that in this particular use something is non-null. So strict enforcement doesn’t mean every @Nullable dereference will give an error.

For example, a checker could support pre-/post-condition annotations on a method that gives additional information in certain invocations.

Selecting which checks should be less enforced.

A blanket @LessEnforced is probably too coarse. Similar to @UnderMigration we need a way to express which checks are less enforced.

@LessEnforced(Nullable.class)
@CheckReturnValue @Nullable String getName() { ... }

would express that only the nullness part of the specification is less strict and the @CRV should still be enforced.

Like for @UnderMigration we need to discuss what the best representation for this is, e.g. class literals as above, canonical checker names, names that are also used for warning suppressions, etc.

Example

#2 contains many examples, all of which should be able to use this proposal. Let's look at findViewByID:

In the use:

setContentView(R.layout.foo);
Button button = findViewById(R.id.send);

Errors on uses of button would be inconvenient on users.

We would declare the method as:

@LessEnforced
@Nullable View findViewById(int id) {...}

The return type is still correctly annotated as @Nullable. However, the @LessEnforced tells clients of this API to be less strict about enforcing the rules, which in this case could mean to treat the method as returning a @NonNull value.

An analysis is still free to give better information, e.g. by checking proper resource IDs and warning on unknown values.

[wmdietlGC]

The basic idea seemed well received.
We should implement this in a prototype to see the complexity and usability of this.

[elizarov]

We've discussed this internally in Kotlin team and have found an issue that would need to be clarified before we go down this road.

The issue is orthogonality of @LessEnforced annotation with respect to @Nullable and @NotNull annotations. For example, let us wear a hat of a library maintainer who has a method in their Java library with non-trivial nullability contract (not unlike Map.get that was worked out at length in #2) and they want to annotate it:

/**
 * Can return null sometimes, but only under some conditions on params.
 * These conditions are spelled out in docs, but cannot be easily expressed with 
 * machine-verifiable/tractable contract. Some tools may be smart enough to understand
 * those additional conditions via additional annotations, some others might not be.
 */
String foo(Params params);

How this library's maintainer is supposed to annotate this method? Repeating analysis from #2, both of the simple options we have are bad:

• @Nullable forces users of foo to always do a null check (which Java has no concise form for) even if they can verify in the docs that their actual params ensure non-null result.
• @NotNull forbids users of foo to check for null when needed and forbids implementation of foo to ever return null.

Now, per this proposal, we give library maintainer a way out with @LessEnforced annotation and they have two more options to choose from:

• @LessEnforced @Nullable
• @LessEnforced @NotNull

But what are the semantics differences between those two options? We've spend a while on the discussion and could not really find any difference either for tools or for library maintainer. We could not find a use-case to differentiate between the two either. Did we miss something?

For a library maintainer, all they want to express while annotating their code is that "nullability contact of this method cannot be easily expressed". Basically they just need a single @LessEnforcedNullability annotation to say that (as was discussed at length in #2).

One possible resolution is to allow only @LessEnforced @Nullable combination and forbid @LessEnforced @NotNull (unless there is some important difference between them that we've missed). This is an acceptable compromise, but it still raises a question as to why we would need a wordy incantation like @LessEnforced @Nullable as opposed to combining them into a single @LessEnforcedNullable annotation.

Please, clarify.

[wmdietlGC]

In this proposal @LessEnforced is a declaration annotation that a library designer can put on a method to express that the whole signature of the method should be interpreted in a "less strict" way.

The nullness annotations should be chosen purely based on the semantics of the nullness annotations. That is, if the method can return null, it should be annotated as @Nullable.
If experience then shows that enforcing this would lead to many false positives, adding @LessEnforced gives an escape hatch to not enforce the contract as strictly.
However, tools would still have the correct signature of the method available to them and could decide to not modify their behavior based on @LessEnforced.

The benefits over a @LessEnforcedNullable are:

• the method signature is annotated in the semantically correct way, without introducing additional "weak" type annotations;
• a single declaration annotation can be used for the whole signature of the method;
• a single declaration annotation can be used for multiple different checkers, instead of adding a "weak" annotation for each type system/checker.

Please let me know whether this clarifies the proposal.

[elizarov]

The way it works with @Nullable is clear. The combination @LessEnforced @Nullable is explained in the accompanying text pretty well.

But what about @LessEnforced @NotNull? Is it a valid combination of annotations? That is not clear. There are no examples with this combination in the text and it is not clear if it is even allowed. Can you clarify, please, if @LessEnforced @NotNull is allowed and if yes, then can you, please, add some examples that would explain how it is different form @LessEnforced @Nullable.

[kevin1e100]

Let's consider based the earlier example:

@LessEnforced
@NotNull foo(@NotNull String bar) { return null; }

I think at a call site, @LessEnforced would allow suppressing errors for foo(null), but indeed there's probably no impact on how to reason about the method result (though technically it may still may sense to use a "platform type", for instance). Conversely, when checking the implementation of foo, maybe no error would be raised here for return null?

[kevinb9n]

This discussion might be a sign that the idea is flawed, and I'm really glad it was brought up.

If we're lucky, we can look at the information conveyed by annotations on a method and we can neatly categorize them into "information that might result in more warnings" vs. "information that might lead to fewer warnings". (Note: for nullability, the kind of warnings we care most about are "this might throw NPE", not things like "seemingly unnecessary null check", which might complicate this model if we treat it as equally important.)

Then we could simply say that @LessEnforced only affects the first kind of information and has no effect on the second. (The question of whether the annotation should even be allowed in a position where we can prove it has no effect should hopefully be a second-order concern.)

I don't know if we will be as "lucky" as I just described or not. Maybe it's just fundamentally more complicated than that. Also I might already be missing some things you're trying to say (sorry!).

[elizarov]

In my mind, the major concerns that we have are not the details of errors/warning that our tools are going to produce, but the fact that we must give library writers a clear guidance of how they should decide between @LessEnforced @NotNull and @LessEnforced @Nullable when annotating their methods.

As a way out of this conundrum, here is a proposal. Can somebody add to this proposal a concrete and specific example of two different existing (non-hypothetical) methods in JDK, Guava or in another widely used Java library, where one of the methods would be best annotated with @LessEnforced @NotNull while the other with @LessEnforced @Nullable, please? With those examples at hand we might be able to work out a more general rule/advice to the library authors and those examples would also serve as a use-case to validate our assumptions about the expected behavior of our tools.

[wmdietlGC]

The guidance to library writers is something like: for each checker/type system/annotation, write the semantically correct signature. If that signature produces too many false positives for a checker, and these false positives are caused by some inherent complexity of that method, add @LessEnforced("@Anno").
This guidance separates the semantic correctness of the signature from the issue of enforcement.

If the false positives are only temporary, migration issues, the guidance is to instead add @UnderMigration as described in #26. In both cases, the semantics of the annotations is correct and an extra declaration annotation expresses that either 1) some inherent complexity causes false positives that should be suppressed using @LessEnforced or 2) the API is under migration @UnderMigration, but eventually the true semantics will be enforced.

Specifically for nullness, there were many examples for @LessEnforced methods that return something @Nullable starting at #2 (comment).
As a concrete example, let's take Button button = findViewById(R.id.send);. Method findViewById is correctly annotated as returning something @Nullable, but by marking the method as @LessEnforced we express that most apps don't misuse the resource ID parameters. A conservative tool still has the correct semantic information to enforce correct usage.

As a concrete example for a @LessEnforced method that returns something @NotNull, we can take Object.toString, raised in #2 (comment).
If we annotate the method as @NotNull String toString() conservative callers that compare the result to null will now get a warning. By adding @LessEnforced to toString we express that these warnings aren't particularly useful. Alternatively, one could use @UnderMigration to ease the migration pain, but eventually enforce that such comparisons are cleaned up. (I agree with #2 (comment) that we should use @NotNull for toString.)

Do note that errors depend on whether the @NotNull/@Nullable is used for a return type or a parameter type:

• @Nullable return type: can cause too many dereference errors for callers;
• @NotNull return type: can cause too many null-comparison errors for callers;
• @Nullable parameter type: can't think of an error for this;
• @NotNull parameter type: can cause too many errors for callers that pass something @Nullable.

If we only think about nullness, having something like

@LessEnforced
void foo() { ... }

might not immediately make sense.
However, there could also be a checker that provides precondition annotations, like this:

@LessEnforced
@RequiresNonNull("this.field")
void foo() { ... }

and this could tell a checker to not issue errors for a violation of this precondition and instead only issue a warning.

Separating enforcement and migration issues from the semantic meaning of the checker-specific annotations seems like a big win. Enforcement and migration will come up with all systems that we define and having standard annotations for them will also be useful for third-party annotations.

Does this make the motivation for separating @LessEnforced clearer?

We should discuss whether @LessEnforced and @UnderMigration should be two separate annotations or whether we should merge them. And then come up with good names for the annotation(s).

[elizarov]

Let's assume that the goal is to recommend the following annotations:

• @LessEnforced @Nullable findViewById(...)
• @LessEnforced @NotNull toString()

Let us see how it affects the users and implementors of these methods. It seems that they produce the same effect of suppressing all the nullability warnings on use-site of findViewById and toString and well as all the warnings for methods that implements them. Is it correct or am I missing something? Is there some code pattern that would be still be giving warnings for @LessEnforced @Nullable findViewById but not for @LessEnforced @NotNull toString or vice versa?

Franky, the analogy with @UnderMigration does not help me here, since I don't see any analogy. @UnderMigration annotation is supposed to annotate a future change in the method semantics to give users an advance warning and give them time to adjust their code for an upcoming change. In this case @UnderMigration is similar to @Deprecated.

On the other hand, @LessEnforced has completely different goal. The methods annotated with it are there to stay forever. Neither findViewById nor toString are going to ever change their contract and we want to let everybody just continue writing they Java code as they did before.

Let me add, that I'm not questioning here the proposal for @LessEnforced itself. I just want to clarify its orthogonality and the correctness of our interpretation of this proposal. It is Ok to have both @LessEnforced @Nullable and @LessEnforced @NotNull as different ways to annotate a method and to convey some additional human-readable semantics. I just want to clarify that we correctly understand that both ways to annotate a method lead to the same machine-readable effect for tools, or do we miss something and there is some difference between them that we need to properly take into account in our tools.

[wmdietlGC]

Both @LessEnforced and @UnderMigration only have an effect on users of an API.

Implementors of a method would still see the usual errors/warnings and should use @SuppressWarnings to suppress them. This allows implementors to ensure the correctness of their implementations while giving users lenience in enforcement.

Tools are free to interpret @LessEnforced in whichever way they see fit. Kotlin might ignore all annotations on a @LessEnforced method and use platform types for the method. The Checker Framework might completely ignore @LessEnforced and use the given annotations. A different tool could give warnings instead of errors for a @LessEnforced method that returns something @Nullable, while no longer issuing anything for a @LessEnforced method that returns something @NotNull.

A developer usually has a choice whether they want to use @LessEnforced or @UnderMigration.
For the findViewById example, the discussion mentions that an Activity.requireViewById(int) method was added as alternative. So instead of adding @LessEnforced to findViewById the API designers could use @UnderMigration and point to requireViewById as the preferred alternative. Once all users are migrated or correctly check for null, the @UnderMigration can be removed and the correct errors will start to get issued.

For either @LessEnforced or @UnderMigration the API designer first picks the semantically correct annotations and then decides about whether this is an inherent complexity or a temporary issue. Because of this similarity between the two issues, we should discuss whether one annotation is enough for this.
I'm fine with two distinct annotations, but wanted to highlight this.

Regarding implementors, I would also like to discuss method overriding. I would like to argue that @LessEnforced should only apply to the such-annotated method, not also to overrides of the method. This allows us to have overrides that enforces the full semantics, makes less-strict enforcement explicit on every method, and avoids having to add a @StrictlyEnforced annotation for expressing the opposite of @LessEnforced.
Take this example:

class A {
  @LessEnforced
  @Nullable Object foo() ...
}

class B extends A {
  @Override
  @Nullable Object foo() ...
}

A a = new B();
B b = new B();
a.foo().toString(); // less strict enforcement
b.foo().toString(); // strict enforcement

Do people agree with this handling of overrides?

[kevinb9n]

Quickly on the override question: I think it is a general principle that we "never" want to automatically inherit annotation-based knowledge from a supermethod, because it is not reasonable to expect developers who are seeking understanding to have to chase upward an arbitrary number of levels. There will be some annotations where we need the policy that any overrides are required to repeat the same annotation (or stronger). I need to open a lot of issues on topics like this.

[kevin1e100]

I want to propose to move away from @LessEnforced. I liked the idea at first but based on the discussion here and further reflection I now believe it has a number of problems:

1. There's no satisfying name for it; "LessEnforced" clearly isn't it and I haven't seen any better proposals.
2. The ambiguity of @LessEnforced @Nullable vs @LessEnforced @NotNull discussed here at length.
3. It's not obvious to me (anymore) that this concept carries over to anything other than nullness. For nullness, @LessEnforced gives a way of talking about the default state, called "flexible" or "platform type" in Kotlin, rather than @Nullable or @NotNull. But in other annotation systems it's not clear such a 3rd state exists. With @CheckReturnValue for instance appears fine to just use @CanIgnoreReturnValue, which happens to be the platform default. Since @LessEnforced is specifically not concerned with migration concerns where unused return values would be warnings instead of errors, I don't see room for @LessEnforced @CheckReturnValue; what would it mean other than simply @CanIgnoreReturnValue?

So I'd propose to abandon @LessEnforced as a standalone/modifier annotation, and instead to look for an annotation that can express the desired semantics (platform/flexible type) for nullness in particular, to avoid the problems above.

[kevinb9n]

These are of course valid points. I think that this is not exactly a decision that we can make ("drop @LessEnforced"); what we can do instead is

• make sure the related requirements are specific and well-justified
• propose what alternative solution instead of @LessEnforced will satisfy those requirements.

OR, another approach is to sidestep the whole debate by saying we'll kick the relevant requirements down the road six months and just deal with them then. There are probably some subset of the requirements we can safely do that with.

[kevinb9n]

Oh, er... after just having said these are valid points now I want to quibble a bit with them, sorry. The previous comment is the more important branch of the conversation.

1. I don't think this counts as an argument to drop a feature; also, I and my teammates are pretty good at generating 57 possible names for a thing, but we deliberately have never done that for "less enforced" because the name isn't close to being important yet.

2. I felt that Werner's comments addressed that ambiguity.

3. Two variations of the question here are: (a) is this conceptually orthogonal to nullness and (b) can we currently think of anything else besides nullness that needs it? I guess the risks of focusing on (b) are implicit in the way I worded it. :-)

Next I'm curious about "can express the desired semantics (platform/flexible type)". My understanding of a "platform type" is that it's what you're forced to use when you have absolutely zero knowledge to go on from the API designer. I see that as something we would never in any circumstances want the API owner to choose intentionally; that would only illustrate that we had failed to properly account for their use case. I think they should always have a way to get what they want that makes their code distinguishable from "no one thought about this yet". This is discussed under what is currently requirement #11 (look for "part-legacy").

[kevin1e100]

I'm honestly confused. My understanding is that this issue was filed as a proposed solution to issues around findByViewId and similar methods that can return null but are too onerous to be usable from Kotlin when annotated @Nullable. That is, the API designers would like Kotlin to use flexible types for the return values from these methods. (A similar argument would apply to Java callers of said methods, where it would also be onerous if a tool forced explicit null checks on the result.)

(As an aside let me say I've been assuming these cases are rare. That is, for most method parameters and results, @Nullable (which forces explicit null checks in Kotlin) or @NotNull are desirable to use.)

All of this is specific to nullness; I don't see an argument to be made that it's orthogonal. It also doesn't have anything to do with legacy or non-legacy, in my opinion. These are (rare) cases where it is sensible for API owners to want Kotlin to use platform types. And I agree that we should strive to give API owners the ability to express this intent.

But I have concerns about providing this expressiveness with an annotation that is intended to apply to non-nullness annotations as well. Add to that the combinatorial problem that, from Kotlin's perspective at least, @LessEnforced @Nullable == @LessEnforced @NotNull (see here), which I believe will be confusing to API owners, as @elizarov has pointed out, since it'll be hard to explain this distinction that has no effect on Kotlin.

One other issue I ran into when experimenting with this was that since @LessEnforced as I understand it applies (by default at least) to all annotations in its scope, that makes it harder to still specify @Nullable / @NotNull for select method parameters. For instance

@LessEnforced
@Nullable String foo(@NotNull String key) {...}

As an API designer I might only want a platform type for foo's result, but not its parameter. I guess the idea is to annotate key with @MoreEnforced @NotNull String? This seems very verbose considering there could be multiple parameters.

Finally, again, I'm not proposing to give up on this use case; I'm proposing to solve it in a nullness-specific way instead, e.g.

@LessEnforcedNullable // to keep the name, subject to change
String foo(@NotNull String key) {...}

Where LessEnforcedNullable could be a type or declaration annotation. If it's a declaration annotation it would apply to otherwise unannotated types in its scope.

[kevinb9n]

Ugh, I'm sorry for misunderstanding so badly. Now I see what you mean. I have to come back to this later but my gut reaction is I will probably agree with you by the time I process it all.

[kevinb9n]

For now, we are fine with this being addressed via @NullnessUnknown, so this is considered resolved.

[cpovirk edit 2021-03-09: There's definitely not consensus at this point that we should endorse/recommend @NullnessUnspecified for this purpose. See, e.g., #71 (comment) and #137 (comment), among others. Granted, I don't think there's a push to add @LessEnforced at this point, either, so I'll keep this issue closed. But we should reopen it as needed. Finally, note that there's also a slightly different proposal for "less enforcement" in #26, which is focused more on temporarily reduced enforcement.]