Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Applicability of TYPE_USE annotations to class declarations [working decision: no] #7

Closed
dzharkov opened this issue Nov 26, 2018 · 26 comments
Labels
design An issue that is resolved by making a decision, about whether and how something should work. needs-decision-before-jar-1.0 Issues needing a finalized decision for the 1.0 jar release nullness For issues specific to nullness analysis.
Milestone

Comments

@dzharkov
Copy link
Collaborator

The question was initially raised by @amaembo:

TYPE_USE annotation can be applied to class declaration. Does @nullable class X{} make sense?

@dzharkov
Copy link
Collaborator Author

Comments from the document:

[@abreslav] I think such things should be reported as errors by the checker, unless we find a good meaning for them

@kevinb9n
Copy link
Collaborator

Agree with Andrey.

@kevinb9n kevinb9n added the nullness For issues specific to nullness analysis. label Nov 26, 2018
@kevin1e100
Copy link
Collaborator

So noted

@wmdietlGC
Copy link
Collaborator

TYPE_USE allows annotations to appear on a class declaration.
This is useful to specify classes that should not be allowed to be @Nullable, for example, java.util.Optional should never be used as @Nullable Optional.
This can be achieved with the following declaration:

@NotNull
class Optional<T> {...}

If nothing is specified, all class declarations are @Nullable, allowing @Nullable uses. Explicit uses of @Nullable should be forbidden.

This goes well together with @NotNullByDefault, as e.g. parameter types are @NotNull by default. With @NullableByDefault and the above Optional declaration, all uses of Optional would need to be annotated @NotNull explicitly.

Should we define this semantic or keep this for a future extension?

@cushon
Copy link
Collaborator

cushon commented Jan 10, 2019

java.util.Optional should never be used as @Nullable Optional

I don't think there's consensus on that: https://stackoverflow.com/questions/9561295/whats-the-point-of-guavas-optional-class#comment12143090_9561334

@wmdietlGC
Copy link
Collaborator

I think there are two questions:

  1. Do we think class declaration annotations are useful for anyone to enforce this property?
  2. Do we agree that we should use this for java.util.Optional? That is, are you a believer in @kevinb9n Optional rules or in Stuart Mark's.

Question 2 raises a more general issue: are we imagining standard CodeAnalysis specifications for the JDK? Eclipse, the Checker Framework, and other tools come with JDK specifications. Are we imagining a repository with agreed upon specifications?

@kevin1e100
Copy link
Collaborator

kevin1e100 commented Jan 10, 2019 via email

@kevinb9n
Copy link
Collaborator

I don't think there is any such thing as a class that should viewed as "never let this be nullable". As soon as you try to get that thing out of a Map, there you are.

@kevinb9n
Copy link
Collaborator

I claim it does not make sense for a class to try to constrain what kinds of nullability its type usages can have. The Map.get just mentioned example illustrates that nullability often has nothing to do with the specific type in question.

So, I believe our type-use annotations should all be disallowed to appear as type annotations.

(There is also the chance that they could be misconstrued as setting the default nullability for elements contained in the class.)

@kevinb9n
Copy link
Collaborator

I will acknowledge that Optional, collections, and enums that define an "unknown" constant are examples of cases where you might want to discourage nullable usages of their static type.

My leaning right now is that even if we want to assist in that kind of check, public class @NotNull Foo is not self-evident enough in its meaning. (One issue already mentioned is that it might be assumed to function like @DefaultNotNull.)

So I am still content to consider this closed for now.

@kevinb9n
Copy link
Collaborator

kevinb9n commented Jul 25, 2019

Another use case might be marking Void as always @Nullable, but I can't think of any other class that should ever do that (an empty enum? but pray tell why?), so it doesn't amount to a strong argument imho.

@cpovirk
Copy link
Collaborator

cpovirk commented Sep 21, 2020

(Aside: Marking Void as always @Nullable is done differently in CF. That's not to say that someone couldn't prefer to do it with a class-declaration annotation.)

@mernst asked about this in an earlier doc about our sample/test-data format.

I think there are a few levels to approach it on:

First: Do we want to define meaning for JSpecify annotations on a class declaration in JSpecify 1.0? The current thinking is "no," though Mike may want to reopen that.

Second: If we don't define such meaning, is it better to declare such annotations illegal or implementation-defined? (Note that, as always, users might hand us bytecode with whatever they want in it, and they might be able to suppress errors even when compiling sources with a JSpecify-aware compiler. So our tools may see such annotations, and we'll want them to not explode.)

Digressing for a moment to set the stage: I think this takes us back to discussions about API vs. implementation code. I've grown increasingly dissatisfied with the blanket statement that "We don't care about implementation code": First of all, it doesn't save us from having to define many of the rules we thought it might (e.g., substitution, subtyping). But even beyond that, what is the point of defining the nullness of APIs unless that provides a well-defined signal to their callers' implementation code?

I still think it makes sense that we don't speak specifically about implementation concerns. And as I've said before, we have no true power to "require" any tool to do anything, anyway. Most of what I see us as doing is defining rules (again, like substitution and subtyping) and leaving it up to tool authors what to do with that information, if anything, in any particular case.

Tying that back to this issue: I do think there's still a case to be made that we don't care about defining the meaning of annotations that are placed inside implementation code. However, when an annotation is placed in an API -- such as on a class declaration -- then I think we have reason to want to say something about it. I think this fits with the existing text in the design proposal / spec, which mostly declines to define the legality of annotations in implementation code (though I notice a few exceptions, which may generate further discussion [edit: see also #114]).

That can lead us to questions about the future: If we want to give meaning to JSpecify annotations on a class declaration after 1.0, is it better for us to have made them illegal in 1.0 or left them implementation-defined? The downside of making them illegal is that users of JSpecify-aware compilers need to wait for their update to JSpecify 1.1 (or, at minimum, they need to be able to suppress some errors). The downside of making them implementation-defined is that different implementations might pick different semantics (like whether public class @Nullable Void marks Void as always @Nullable or not).

Third: If JSpecify annotations don't support this, other nullness annotations still might. This lets people who want, say, CF semantics use the CF @Nullable. However, this may raise questions around aliasing/implies: If someone asks a JSpecify checker to treat CF @NonNull like JSpecify @NonNull, then does that mean that checker sees it as an error to put CF @NonNull on a class declaration? That could be unfortunate for existing users of this feature (though I'm not sure how common it is outside of Optional). But the alternative is to allow users to accidentally put their custom @Nullable annotations in locations where JSpecify checkers will ignore them, perhaps silently :(

(Final comment: We may be able to find a better term than "illegal" for that rough concept. I think we've spoken before about "well-formedness," but that may have other connotations that we don't mean to imply here.)

@kevinb9n kevinb9n changed the title Applicability of TYPE_USE annotations to class declarations Applicability of TYPE_USE annotations to class declarations [working decision: no] Jan 27, 2022
@cpovirk
Copy link
Collaborator

cpovirk commented Mar 13, 2024

(Piling on: Especially now that we have @NonNull, it's also easy to imagine that someone might try to annotate a class with @NonNull when the person actually wants @NullMarked.)

[edit: clarification: Of course, we can't do anything to make javac prevent users from putting @NonNull on a class declaration, since TYPE_USE annotations are always allowed there. However, if we at least declare that the class declaration is an inapplicable location for JSpecify annotations, then we can have JSpecify-aware checkers produce errors if users put JSpecify annotations there (including even tools like Error Prone that aren't "nullness checkers" but that can check for JSpecify annotations in inapplicable locations (example)).]

@kevinb9n kevinb9n added the design An issue that is resolved by making a decision, about whether and how something should work. label Mar 13, 2024
@kevinb9n kevinb9n added this to the 0.3 milestone Mar 27, 2024
@cpovirk
Copy link
Collaborator

cpovirk commented Mar 28, 2024

And in fact, we just saw something similar but slightly different: an attempt to use @NonNull as a meta-annotation.

[edit: and, to be clear, also @Nullable and @NullMarked. I think I'd heard that meta-annotations are a common pattern in Spring?]

@netdpb
Copy link
Collaborator

netdpb commented Apr 9, 2024

The current, working decision, as of release 0.3, is that JSpecify 1.0 will not allow its type-use annotations (@Nullable and @NonNull) to apply to class declarations. @Nullable class Foo {} is not legal.

The argument for changing this decision is that it would allow us to mark a class so that all its type usages are forced to be either non-null or nullable.

However, nobody has made a strong argument that always-nullable or never-nullable type parameters represent an important use case. It's not worth complicating the model.

This must be decided before version 1.0 of the jar.

I propose the current decision be finalized for 1.0. 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.

EDIT on 2024-05-07: Please see the revised proposal below (#7 (comment)). It doesn't represent a significant change compared to this proposal (just a clarification of potential future use), so a 👍 for this proposal will continue to count for the revised proposal.

@netdpb netdpb added the needs-decision-before-jar-1.0 Issues needing a finalized decision for the 1.0 jar release label Apr 9, 2024
@sdeleuze
Copy link
Collaborator

sdeleuze commented Apr 10, 2024

Meta-annotations are indeed a common patterns in Spring, and an alternative to the @Implies feature could simply be to allow meta-annotating custom annotation classes definition with JSpecify annotations, and treat those custom annotations as aliases. So I am wondering if that could make sense to authorize (in the spec) such usage only on other annotation classes definitions. See also this related comment.

I would like to discuss if all usages on class declaration should be forbidden in the spec in 1.0, and potentially authorized post 1.0 (for example 1.1). But I have related fears that if we forbid that now, that will be a nightmare if we introduce that later with some tools supporting it and some other triggering an error. As consequence, I thumbs-down this issue in order to have a related discussion before taking a decision.

For other use cases than annotation classe declarations, I am ok to consider them not legal.

@kevinb9n
Copy link
Collaborator

kevinb9n commented Apr 10, 2024

If it's okay, I'll file a separate issue about the implies use case. The possible resolutions for that issue would be "we provide @Implies", "we support meta-annotation" -- or, of course, if it's deprioritized or closed, then "neither".

Then, this issue would cover whether our annotations would be allowed on class declarations for any other purpose but that. (The thread above covers the common use case we were aware of, but there could be others.) This part might be easy to get consensus on.

Sound okay?

[If not we at least need to reopen this issue]

@sdeleuze
Copy link
Collaborator

Then, this issue would cover whether our annotations would be allowed on class declarations for any other purpose but that. (The thread above covers the common use case we were aware of, but there could be others.) This part might be easy to get consensus on.

Ok for that, once clarified I will turn my thumbs down to thumbs up.

If it's okay, I'll file a separate issue about the implies use case.

I would maybe suggest waiting we discuss the document I am about to write before creating a new issue if that's ok for you.

@netdpb
Copy link
Collaborator

netdpb commented May 7, 2024

For this issue, I'll change the wording of the proposal to this:

Proposal: JSpecify 1.0 will not allow its type-use annotations (@Nullable and @NonNull) to apply to general class declarations. However, these annotations applied to annotation types are considered meaningless but reserved for future use. The annotation in @Nullable class Foo {} is meaningless, as is the one in @Nullable @interface Bar {}, but the latter may become meaningful in a future version of JSpecify.

Note that this doesn't represent a significant change to the previous proposal (#7 (comment)) in that that proposal also considers these annotations to be meaningless on annotation types, but it does clarify that we may assign a meaning to such annotations in the future, whereas we plan not to assign any meaning to them on other class types.

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. Note: A thumbs-up on the previous proposal will be considered a thumbs-up to this proposal as well.

EDIT on 2024-05-21: Please see the new proposal below (#7 (comment)).

@GregDThomas
Copy link

I'm not adding a thumbs-down, as a mere bystander I'm sure I don't fully understand the reasoning behind this, but ..

@nullable class Foo {} is not legal, but
@nullable interface Bar {} is [legal] meaningless ...

I can't help but feel that this breaks the principle of least surprise, no? One is legal, the other is not.
Also, what about an interface that has default method? What will the implication be on those default methods? Why is that different from standard class methods?

@netdpb
Copy link
Collaborator

netdpb commented May 7, 2024

Thanks for your comment!

@Nullable class Foo {} is not legal, but
@Nullable interface Bar {} is [legal] meaningless ...

To clarify:

  1. We're talking about annotation types, so your second example should be @Nullable @interface Bar {}. As you say, interfaces and classes are pretty similar and it would be surprising for JSpecify to treat them differently; but annotation types are very different from both, and so it's not so surprising if JSpecify treated them differently.

  2. The difference between "not legal" and "meaningless" is a fine one, and maybe "not legal" is a bad phrase. (I'll edit the revised proposal to remove "not legal".) The clarification I'm trying to make here is that although the annotations in @Nullable class Foo {} and @Nullable @interface Bar {} are both meaningless in JSpecify 1.0, the latter may have some meaning in a future version of JSpecify.

Does that help?

@GregDThomas
Copy link

It does, yes. Sorry, somehow missed the @interface vs interface distinction!

@wmdietl
Copy link
Collaborator

wmdietl commented May 8, 2024

I find the updated proposal text confusing.

JSpecify 1.0 will not allow its type-use annotations (@Nullable and @NonNull) to apply to general class declarations.
I'm not sure what a "general class declaration" is, but here the annotations are "not allowed".

Then later:
The annotation in @Nullable class Foo {} is meaningless, as is the one in @Nullable @interface Bar {}, but the latter may become meaningful in a future version of JSpecify.
Here the proposal uses "meaningless" for both cases.
So are the annotations "not allowed" or "meaningless"?

@kevinb9n
Copy link
Collaborator

kevinb9n commented May 8, 2024

JSpecify specifies which type usages are nullness-applicable. We should add that only type usages can be nullness-applicable, not any of the other places type-use annotations can go.

Have we ever put anything else in this category "meaningless but reserved"? If not, I would much rather not casually start down that road. I would like putting a nullness annotation on a class declaration to be forever meaningless, because whatever meaning we might like it to have in the future, we would do better to define a new annotation to express that more clearly anyway. We can get into why, but not here/now.

So, 👎🏼 on the proposal. [resolved below, yay!]

@cpovirk
Copy link
Collaborator

cpovirk commented May 8, 2024

My perspective would be that we need to make a decision for 1.0, and the only decision we can make for 1.0 is between "This is applicable with meaning x" and "This is not applicable." Any discussion of what might happen in the future is out of scope. In that respect, I'd see this issue as the same as all the other 1.0 issues, and I wouldn't try to differentiate is as "reserved," nor would I attempt to commit now to never using it. Neither strikes me as necessary: Those two options are exactly the options that we leave open by saying that the annotation is inapplicable for 1.0. And part of our goal is to avoid having to block 1.0 on even the basic shape of the design of an implication/aliasing system.

@netdpb
Copy link
Collaborator

netdpb commented May 21, 2024

New Proposal

This proposal is essentially the same as the original proposal.

Proposal: JSpecify will not allow its type-use annotations (@Nullable and @NonNull) to apply to class (and interface, and annotation, etc.) declarations.

This proposal does not mean that JSpecify won't implement a mechanism for one annotation to imply another in the future (#35 and friends).

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. Note: A thumbs-up on the original proposal will be considered a thumbs-up to this proposal as well.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
design An issue that is resolved by making a decision, about whether and how something should work. needs-decision-before-jar-1.0 Issues needing a finalized decision for the 1.0 jar release nullness For issues specific to nullness analysis.
Projects
None yet
Development

No branches or pull requests

10 participants