Declaring that one annotation aliases or specializes another (`@Implies`) [working decision: no] about jspecify HOT 30 CLOSED

I wonder if we can decide among a few options for moving forward here for 1.0.

1. Maybe 1.0 doesn't need any @Implies annotation at all. Each checker tool has a way to configure aliases already. For libraries that want to be used by clients who use any tool, it behooves them to change their annotations to the JSpecify ones. For users who are committed to a specific tool, they can configure it however it expects to recognize the aliases it wants to.
2. 1.0 needs to support a common use case for aliasing the JSpecify nullness annotations, but we can decide not to support more complex annotations (such as those with parameters) or more complex relationships besides simple implication (such as refinement or implies-except) for now because we believe we have a reasonable path toward supporting those more complex use cases in a later release without breaking existing users.
3. 1.0 has to support more general use cases, such as those described above, because we do not believe we can support only the common use case first without precluding support for the more complex ones later.

from jspecify.

Now, replacing @TypeQualifierDefault with @Implies(NullMarked.class) won't make a big material difference except that it would make me feel better and bring one step closer to removing JSR305 from our deps.

Our experience inside Google is consistent with this: @NullMarked finds some additional errors beyond what @TypeQualifierDefault does because @NullMarked also applies to type arguments, like the Bar in Future<Bar>. And we're happy for that, as we have a lot of Future instances floating around. Still, my impression has been that we can produce the majority of the errors that people see with just @TypeQualifierDefault.

Relatedly, JSpecify helps with type-variable usages: For a method like Future.get(), the return type isn't @Nonnull T, and it isn't @Nullable T: It's "just T," which @TypeQualifierDefault doesn't provide a way to express.

Some people avoid these issues by always having non-null type arguments: You can use a List<String> but not a List<@Nullable String>. (If you want the latter, you use List<Optional<String>> or something.) People in that situation will see less benefit from @NullMarked.

(And yes, we'll be happy to finally remove that jsr305 dependency, too :))

from jspecify.

We have made a working decision to include this for 0.3. This will help us discover any serious problems with it before 1.0.

EDIT: we later pulled it back. #307 has relevant newer discussion.

from jspecify.

Notably it wouldn't be a complete solution, since there will be users who want to alias an annotation they don't own and the owner won't do it.

from jspecify.

Other names for @Implies?

@Extends
@Specializes
@Refines

[edit: see #218 as the new home for the topic that follows here. The comment here is asking whether we might just do that instead of having @Implies at all.]

But an alternative to @Implies might be to establish a pattern instead, that most annotations should include Target(ANNOTATION_TYPE) and any code which for the presence of annotation @Foo should check any other annotations present to see if they have @Foo, and so on. This is a pattern we've actually used a fair number of times, and I wouldn't be surprised if it has plenty of industry precedent too.

It's less clear/readable than @Implies and also leaves each annotation needing to specify "and here's what it means if you apply me to another annotation type" instead of just letting @Implies take care of that. OTOH, even in the latter case the annotation may still want to say "NOTE: any code checking for the presence of this annotation is expected to recognize @Implies!!!" anyway.

from jspecify.

Such annotation synonyms make IDEs life harder, and code analysis slower for everyone, even those not using synonyms. I'd prefer to avoid adding them if possible, unless there's a very high demand and specific scenarios.

The reason: when we know the notnull annotation is called NotNull and we see some @Foo, we can safely skip it and save some time on resolving the Foo. But when there are synonyms, we should either resolve all annotations always, or precompute the names of all synonyms, which requires a whole-project search (using another index, but still not instant), which should also be repeated each time the caches are dropped, which is often. Building an efficient index of synonyms is complicated by the fact that they can be defined in any JVM language, and not all languages are supported equally well and allow for efficient annotation search. We're already suffering from similar issues in Spring support.

from jspecify.

Very good to know, thank you.

from jspecify.

From meeting notes:

The added burden to IDE analysis - does it scale with the number of usages of @Implies on encountered annotations, not the number of usages of the marked annotation?

It depends on the specific syntax. If it's @Implies(NotNull.class), then with the current APIs it scales with the total number of usages of @Implies in the project and libraries. Shouldn't probably be too much. But note that this syntax doesn't allow implied annotations to have parameters. There are other approaches that allow parameters.

One (AFAIK Spring takes it) is to just annotate an @interface Foo with your annotation, and then @Foo will also have your semantics. This one is the most expensive, it scales with the number of @YourAnnotation usages in the project&libraries, both on annotation types and in other places. Or with the total number of @interface declarations, which is lower, but still unfortunately a lot.

The other is represented by @TypeQualifierNickname: when your @interface Foo is annotated with this @Nickname, then some subset of the other annotations on Foo is propagated to @Foo. Not all, obviously, because some of those annotation apply only to Foo, e.g. @Retention. Thus one should distinguish these subsets. In JSR-305, this is done with the "interesting" subset having @TypeQualifier. This scales with the number of @Nickname usages in the project&libraries, comparable with @Implies cost, but to me this added ceremony of type qualifiers feels a bit heavy.

from jspecify.

Spring has already been mentioned in previous comments, but I would like to add more context since our use case impact a lot of users and could also apply to other projects.

Given the unclear status of JSR 305, we have decided not to expose it directly, but rather to hide its usage via the meta annotation support behind Spring null-safety annotations that are now part of our public API. We introduced them by anticipating a better replacement, which is currently happening with this codeanalysis annotations effort.

We have following annotations:

• @Nullable: equivalent of codeanalysis.experimental.annotations.Nullable
• @NonNull: equivalent of codeanalysis.experimental.annotations.NotNull
• @NonNullApi: equivalent of codeanalysis.experimental.annotations.DefaultNotNull currently with a narrower scope due to limitation of JSR 305, but the ideal target is to extend it to generics, varargs and array elements of related APIs, so same scope.
• @NonNullFields: I don't think we have an equivalent currently in codeanalysis annotations.

I am currently doing some test with @dzharkov on a local branch with codeanalysis annotations instead of our Spring ones meta-annotated with JSR 305 ones in order to provide feedback to the working group, but for any kind of real word usage, this "meta annotation feature" is mandatory, and the lack of it would prevent us from using codeanalysis annotations.

We have no strong opinion about how that should be implemented, we are indeed usually using implicit meta annotations, but if a dedicated annotation like @Implies allows IDEs to implement that feature more efficiently that's perfectly fine.

I think we would support both JSR 305 and codeanalysis annotations for some time (let say 1 year then sunset JSR 305 and let our null-safety annotations only annotated with codeanalysis annotations.

from jspecify.

In Nullsafe we use @Nullsafe class-level annotation to

• mark that the class is DefaultNonNull
• allow users to configure certain aspects of checker's behaviour.

Annotation aliasing would be very helpful for us at least for the following reasons:

• Help with interop between @Nullsafe Java classes and Kotlin code.
• Make OSS FB libraries (that again use @Nullsafe classes) more friendly for the community.

Given that annotations currently present in the design are parameterless there's not much difference between

1. @Implies-annotation

@Implies({DefaultNonNull.class})
public @interface Nullsafe ...

2. Aliasing via application

@DefaultNonNull // alias
public @interface Nullsafe ...

No.1 is clearer, but No.2 (w/ a comment) is not too bad either, and added flexibility in allowing to specify arguments to aliased annotation seems to be a nice bonus.

Notably it wouldn't be a complete solution, since there will be users who want to alias an annotation they don't own and the owner won't do it.

@kevinb9n this is somewhat restrictive, but I don't feel this is necessarily a bad thing. At the very least this prevents people from producing inconsistent aliases. In this (rather far-fetched) example I wouldn't like to be the person who depends on MySuperAnnot and both libA and libB if

libA:

@Nullable
public @interface MySuperAnnot ...

libB:

@NonNull
public @interface MySuperAnnot ...

@donnerpeter do I understand correctly that your concern with option No.2 (aliasing via application) is that it would require to scan all @interface declarations to build aliasing index compared to just uses of @Implies (but the resulting index size would be the same)?

from jspecify.

@artempyanykh It'd require to either scan all @interface declarations in all JVM languages, or all usages of @NotNull, or the intersection of these two sets (and do it after any change in the project, any typing).

I'm not sure which index you mean and what would be the same.

from jspecify.

@donnerpeter sorry, I have 0 experience in implementing IDEs, but want to understand better the situation, so please bear with me.

To support aliases in Infer, we would just lazily build a mapping from encountered annotations to their base jspecify analogues as we walk the CFG. Since this is a batch job, the overhead of this lookup would be low and there wouldn't be much difference between @Implies(DefaultNonNull.class), @DefaultNonNull public @interface MyAnnot, or the combination.

Now in IDE this should happen incrementally, but I don't quite understand why the cost cannot be efficiently amortised.

For instance:

...and do it after any change in the project, any typing

Why would it need to be any typing? I'd assume it depends on the "context", so if someone is not editing annotation classes or changing annotations on elements there's no need to rebuild the index of aliases. Or am I missing something?

On related note, perhaps one aspect of @TypeQualifierNickname that I find questionable is its recursive nature. Theoretically, it allows for very flexible setups, but I have found 0 usages of it both in our Android and server code. This may very well be idiosyncratic to our codebase, so input from people with more sophisticated setups would be appreciated.

But anyhow, would it be easier to limit the scope of such annotation to be just a marker to simplify life of IDE implementers (if it's really needed) without the requirement to propagate annotations from an alias to annotations this alias is applied to?

So that when someone wants to alias some base annotation from jspecify they would need to write:

import jspecify.nullability.DefaultNonNull
import jspecify.meta.Alias

@Alias
@DefaultNotNull
@Nullsafe { ... }

from jspecify.

Why would it need to be any typing? I'd assume it depends on the "context", so if someone is not editing annotation classes or changing annotations on elements there's no need to rebuild the index of aliases. Or am I missing something?

You're right, in an ideal world that'd be so. Unfortunately it's too expensive to determine what an edit (or an update from version control, or a library jar change) could affect across the project, so, at least in IntelliJ, we drop most caches on any change, and try to be fast in recomputing them.

Non-recursive aliasing would indeed simplify the life of (our) IDE. But explicit marking seems much more important IMHO.

from jspecify.

I'm still not in a position to comment on the performance implications, but can only speak to my continued positive impressions of the benefits of the feature.

First, the topic of this comment is: what would it mean, exactly?

Assuming this simple usage:

@Implies(Foo.class)
public @interface Bar {}

And this generalized usage of our example annotation:

// elsewhere
@Bar /* some annotatable element here*/

Implies says that IF @Foo is also legal to appear in that context (by its target type):

// elsewhere
@Bar @Foo /* some annotatable element here*/

then these two snippets just above convey identical information; no meaning should be ascribed to the difference between them.

(Of course, checkers that want to issue a warning to the latter that @Foo can be safely removed would be welcome to, so that is a difference in behavior, but still not a difference in meaning.)

We would say that @Bar is a "specialization" or "refinement" of @Foo, and in fact @Refines and @Specializes are potential names for the annotation.

Bar may or may not add semantics of its own. If it does not, we may use the term "alias" to describe it, and its javadoc should presumably say nothing but "Alias for {@link Foo}". (We might wish in theory that the @Implies link could be made in both directions, but in real life we'd have to be content with just one.) In this alias scenario, each client codebase may have its own policy for which annotation's usage is preferred; it is probably not something that @Bar itself can define and thus not something @Implies would have anything to do with.

(The alias use case makes the name @Implies a little more attractive than @Refines or @Specializes, since the latter might subjectively be seen as suggesting more than the trivial refinement.)

All the above doesn't provide any solution for implying another annotation with particular attribute values; e.g. you can't define a @Bar that implies @Foo("value here"). However (a) many of these cases would want some "pass-through" of values anyway, which it's hard to see any way to accomplish, and (b) for the hardcoded no-pass-through case, @Foo could choose to enable that differently, by adding @Target(ANNOTATION_TYPE) and documenting it to have that meaning when applied to annotations.

(Aside: we've said we might offer small helper libraries for checker implementations or runtime/reflection code to use, if the need arises. A "does this element have this annotation on it" method that automatically traverses @Implies would be a simple example of this.)

from jspecify.

Now starting to get at why I feel this is important,

A thought experiment: if some codebase converts over to use our annotations completely, let's say that's what a 100% victory looks like for us. But what if it does not use our annotations at all, but it does use annotations that contain hard links via @Implies to ours? Would we call that a 50% victory, or 80%, or 10%, or what?

imho, I think of it as like 90% victory. Because it can still be very concretely observed in the code that our semantics are the ones in play.

If they use annotations that maybe mention ours in javadoc, that's kinda okay, except that that's going to serve no purpose until they go around configuring all their tools to say "please recognize our annotation as their annotation" (which would happen magically if we had @Implies). Of course, in the real world people will do that without even bothering to mention this in their annotations' javadoc, and from their pov, why should they?

from jspecify.

A few design points:

• @Implies still seems like a fine name to me
• It should take a Class<? extends Annotation> ... it will only be useful for marker annotations
• Possibly a boolean isAlias() default false might be useful, to signify that this class promises it adds no additional semantics and thus the two annotations are equivalent
• The specified annotation type should have all the target types the current annotation type has [soft requirement]
• The Implies javadoc should warn that it's important for "all" code that checks for the presence of an annotation to do it using a mechanism like that takes @Implies into account.

from jspecify.

The ability to remove runtime retention is looking even more important than I'd thought, thanks to old versions of Android.

from jspecify.

Earlier today, I noted one way that we could end up with a nullness annotation and an alias for its inverse in the same location (though presumably we'll work to avoid that).

This relates to an earlier possibility that has come up a few times -- namely, that we'd end up with a nullness annotation and another annotation that implies that same annotation in the same location. Specifically, we've discussed that this could happen with @PolyNull @Nullable (1, 2, 3). In theory, aliasing/implies should make that unnecessary: By declaring that @PolyNull implies @Nullable, we eliminate the need for @Nullable. On the other hand, I would anticipate that:

• Sometimes an annotation like @PolyNull will not have been updated that way (yet?), so people may want to use both. If so, it would be a little sad to have to remove @Nullable in lockstep with updating the definition of @PolyNull.
• Some tools will recognize any annotation named "Nullable" but not implement our aliasing/implies logic. Then again, I guess a solution here is to use @PolyNull for JSpecify tools and some non-JSpecify annotation named "Nullable" on the same usage? But mixing in a non-JSpecify "Nullable" annotation is confusing and error-prone in its own way.

Anyway, this is all to say that aliases open up the possibility of writing @Foo @NotFoo or @Foo @Foo in indirect ways. We'll want to think that through.

from jspecify.

Another thing to consider, especially if we embrace aliasing/implies as a broad solution to many problems:

A JSpecify checker can always recognize code with @org.jspecify.annotations.Nullable on it, even if that class isn't on the classpath.

(OK, it's possible that the implementation of a particular checker will in fact require that class to be present. But in principle, the checker could work without the class definition. And if it really wants the class definition to be present, then the checker (or at least its build-system integrations) can add that class to the classpath automatically.)

And that can be important, because people like to hide their annotation dependencies entirely from their users. This is (I have argued) a bad idea, but people do it because Maven has no true compile-time-only scope.

But if code uses @com.foo.MyNullable, then the JSpecify checker needs to see the definition of @com.foo.MyNullable in order to know that it implies @org.jspecify.annotations.Nullable.

One bit of good news is that, if we provide aliases as part of JSpecify itself (e.g., for a CLASS-retention version of @InTheClub), then it's likely that (a) they will appear in most JSpecify users' classpaths or at least (b) JSpecify-based tools can hardcode knowledge of those annotations for the case in which they're not in the classpath.

from jspecify.

As far as I can tell, javac itself at least doesn't mind usages of an annotation whose declaration has @Implies(SomeClassNotOnTheClasspath.class). That's the case even though it does mind usages of an annotation whose declaration has @Target(SOME_ENUM_VALUE_NOT_ON_THE_CLASSPATH). (Caveat about that latter problem: I don't know if it's specific to @Target (since javac cares specifically about that) or more general. It would be easy enough to test.)

$ tail -n +1 *.java
==> Implies.java <==
@interface Implies {
  Class<? extends java.lang.annotation.Annotation> value();
}

==> JSpecifyNullable.java <==
@interface JSpecifyNullable {}

==> OtherNullable.java <==
@Implies(JSpecifyNullable.class)
@interface OtherNullable {}

==> User.java <==
@OtherNullable
class User {}

$ javac -sourcepath none Implies.java JSpecifyNullable.java OtherNullable.java && mkdir othernullableonly && cp OtherNullable.class othernullableonly && javac -sourcepath none -cp othernullableonly User.java
<no errors or warnings>

[edit: I later did some testing of runtime reflection, too (after increasing annotation retention to RUNTIME :)). I didn't see trouble there, at least not for the simple case of looking up the annotations on User.]

from jspecify.

Assuming @interface Foo {} and @Implies(Foo.class) @interface Bar {}.

First, ignoring TYPE_USE cases: If Bar includes any target type that Foo doesn't, compiling Bar "deserves" a warning. If @Bar appears on such a target, then as stated above, none of the semantics of @Foo are considered to apply there.

Bringing TYPE_USE in, the primary concern is to nail down what happens in ambiguous cases like @Bar String x();.
(a) decide exactly what kind of annotation @Bar is here without any regard to what @Foo supports
(b) decide it more leniently; if @Foo supports only one interpretation consider it to be that one

Then #124 discusses possible intentional provisions we might want to make for implication across this boundary.

from jspecify.

RE: (1):

An impression that I got (which may or may not be accurate) is that part of the reason we're here is that at least one tool vendor (Kotlin) is trying to avoid adding nullness annotations to its list and also avoid exposing arbitrary configuration abilities to users. Maybe we can run that by someone from Kotlin to see if it's accurate?

Aside from Kotlin, my impression is indeed that most tools will let you specify which annotations to recognize, or they'll recognize anything with the simple name "Nullable."

from jspecify.

As for how to decide among your options (which sound like the right set of options to me):

There are 2 use cases for @Implies that I've been thinking will most influence its design, and each comes with a prototypical user:

1. I already annotated my library for nullness, and I worry that switching even the type of annotations (perhaps especially when switching between declaration and type-use annotations) could break something. I suspect that this is the situation Spring is in?
2. I want to minimize how "strongly" I depend on JSpecify, so I'd rather use my own alias. This is what we may see with protobuf, who may want their generated code to depend directly on the protobuf library but not directly on anything else.

(To be clear, there are also other use cases, like having @PolyNull imply @Nullable, but my feeling has been that those are less likely to influence the design of @Implies.)

This suggests that we should talk to Spring (whom we haven't been in contact with as much lately) and other possible users of aliasing to see:

• how much they care about it (especially compared to alternatives, like a hypothetical tool to help them rewrite their existing annotations)
• how they feel about specific possible features (like #124, which, notably, may well be a requirement for @Implies to be useful for Spring)

(We can also talk to protobuf, but that feels less pressing for a couple reasons.)

from jspecify.

Pulling all the way up to "why even do this?":

The alternative to this proposal is just continuing to embrace the idea that tools are just all going to have their own big config files as always.

And what that model says is: "Who is the authority on what an annotation means? The tool and the user get to decide what it means."

I see it as a core part of JSpecify's goal and raison d'etre as trying to push toward shifting that answer: the annotation decides what the annotation means. Users and tools can still do their tricks to imbue them with extra meanings that might not have been intended, but we shouldn't have to count on that, and I'd love to discourage it as much as possible.

(And after all, this project is about more agreement between tools, is it not?)

(EDIT: this argument doesn't necessarily make the case for 1.0 vs. 1.1, etc., though.)

from jspecify.

I fully support the idea of JSpecify taking on the big challenge of unifying meta-annotation semantics, or at least of exploring that possibility.

My comment was focused only on figuring out whether that challeng is one we can reasonably decide is not necessary for us to take on before the successful launch of JSpecify 1.0.

from jspecify.

My 2¢ - having some form of @Implies is not a deal breaker for us, but there's a number of OSS libraries that are released with our @Nullsafe annotation (ex. in Fresco, the annot. is similar in spirit to @NullMarked).

Currently, we piggyback on JSR305's @TypeQualifierDefault to ensure that Kotlin code does understand the default nullability and doesn't try to infer platform types. This is actually a big deal for us.

Now, replacing @TypeQualifierDefault with @Implies(NullMarked.class) won't make a big material difference except that it would make me feel better and bring one step closer to removing JSR305 from our deps.

from jspecify.

I wonder if we can decide among a few options for moving forward here for 1.0.

1. Maybe 1.0 doesn't need any @Implies annotation at all. Each checker tool has a way to configure aliases already. For libraries that want to be used by clients who use any tool, it behooves them to change their annotations to the JSpecify ones. For users who are committed to a specific tool, they can configure it however it expects to recognize the aliases it wants to.

(To express this decision we would move all Implies-related issues to the post-1.0 milestone.)

2. 1.0 needs to support a common use case for aliasing the JSpecify nullness annotations, but we can decide not to support more complex annotations (such as those with parameters) or more complex relationships besides simple implication (such as refinement or implies-except) for now because we believe we have a reasonable path toward supporting those more complex use cases in a later release without breaking existing users.
3. 1.0 has to support more general use cases, such as those described above, because we do not believe we can support only the common use case first without precluding support for the more complex ones later.

And 2-vs-3 breaks down like this by feature:

• Parameters: absolutely, assume we will say/do nothing about this case. Separately, #218 argues for a simple solution.
• Refinement: I don't think refinement is a special case, it's just generally how this works. Did I misunderstand anything?
• Alias: the ability to mark an annotation as being a pure alias (non-refinement?) is an optional feature, with some value, that is NOT part of this (andisAlias=false would be the default anyway). #233
• Implies-except: this is about precedence rules when a conflict is found, and we have to have some decision on it (#216)
• Imply-multiple: assume no, because #213 tracks that.

from jspecify.

TODO: reopen this with new summary, as this is one of the 3 most vertical issues we have open for 1.0 currently.

from jspecify.

As discussed with @kevinb9n recently, and as described in this old but still relevant comment, @Implies or meta-annotation support is mandatory for Spring Framework 6 adopting jSpecify.

from jspecify.

Appreciate you reasserting this. It may seem like it should be unnecessary to repeat, but it really does help. Will address in meeting and update here.

from jspecify.