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

Should we specify a meaning for annotations on a receiver parameter's _type arguments_? #157

Closed
cpovirk opened this issue Dec 3, 2020 · 26 comments
Labels
design An issue that is resolved by making a decision, about whether and how something should work. nullness For issues specific to nullness analysis.
Milestone

Comments

@cpovirk
Copy link
Collaborator

cpovirk commented Dec 3, 2020

We already say that the receiver parameter itself is intrinsically non-nullable (soon to be covered by a sample input): It is one of the non-nullable type contexts. That is, we'd call the following an unrecognized location:

interface Foo {
  void go(@Nullable Foo this);
}

But I have come to feel that it's a bit weird to annotate even the type arguments of a receiver parameter, as in the following:

interface Foo<T extends @Nullable Object> {
  void go(Foo<@Nullable T> this);
}

I'm not saying that we should call those locations "intrinsically non-nullable" but rather "unrecognized locations". (Aside: I don't know that the draft design proposal makes quite the same distinction: It speaks of "unspecified" behavior for "implementation code," but the samples doc I'm linking to uses "unrecognized" to refer to a probably somewhat different concept.)

The intention of the code above, presumably, is to say "You may call foo() only on instances of types like Foo<@Nullable String>, not on instances of types like Foo<[@NonNull] String>."

But I have ~5 reservations about this:

  1. I'm aware of only ~1 use case for this. It's around Collection.removeAll and retainAll. But Collection<@Nullable E> this is at most part of the story because the story is quite strange. (I wonder if there are any use cases around @NonNull? I don't recall any, but if there are some, that's a tiny point relevant to both this issue and good old [moved to #230] Decide whether to include a @NonNull annotation #4.)

  2. Anytime we add a feature, users are going to misuse it by accident on occasion. I don't want to make this sound very likely -- receiver parameters are rarely used to begin with! -- but if we anticipate that users will rarely want this feature, then we might well see accidental misuses constitute the majority of uses.

  3. The Checker Framework does not currently support this, and I would assume that Kotlin does not, as well. (I assume both that there is no way to express receiver constraints in the Kotlin language and also that Kotlin does not have handling for Java receiver constraints.) Both could add such support, but since neither supports it now, that may be a sign that this is not worth specifying. (Again, I'm not proposing to ban such support, only to call it an extension to our specified semantics.)

  4. This provides a very limited level of support for definitely nullable type parameters. I guess that's not exactly a bad thing, but it feels to me like we'd be putting some of the implementation complexity onto tool authors and some of the conceptual complexity onto users (e.g., in the error messages that result). And we'd be doing all that without getting the full support for definitely nullable type parameters that such complexity could unlock.

  5. I think the syntax is a bit misleading. I'm not sure I can explain this well, and I somewhat doubt that this point about syntax is going to be decisive, so I'll just handwave: What Foo<@Nullable T> expresses to me is "another type, possibly distinct from the Foo<T> that we have an instance of." And while that's not exactly wrong, I would tend to express what we "really mean" as follows:

interface Foo<T extends @Nullable Object> {
  <require T extends @Nullable Object super @Nullable void> void go();
}

Essentially, we're overriding the definition of <T> for the scope of this method, and that lets us give it a more strict bound. (And yeah, this example takes us back to discussions of setting lower bounds on type parameters. But setting that aside...)

(context)

@kevin1e100
Copy link
Collaborator

kevin1e100 commented Dec 4, 2020

So I think our hypothetical filterNonNull is also an example:

interface Sequence<T extends @Nullable Object> {
  Sequence<@NonNull T> filterNonNull(Sequence<@Nullable T> this);
}

As for non-null constraints, maybe:

interface Numbers<T extends @Nullable Number> {
   int[] asInts(Numbers<@NonNull T> this);
}

While certainly rarely useful this seems like the kind of thing that's more easily allowed than forbidden, since it's valid Java syntax, so we'd have to have an explicit rule about it. Plus nothing really surprising happens, I think, when you use it.

Two other thoughts that don't really help with this issue:

  1. Where this in principle could be more commonly useful is for constructors, e.g., for the ThreadLocal case discussed ... somewhere, where new ThreadLocal<@NonNull Integer>(); should ideally be illegal. But alas it's not syntactically allowed there, while the following is ironically both unhelpful and syntactically allowed:
class Foo {
  public @Nullable Foo() {...}
}
  1. As another aside, reading this made me think receiver annotations might be interesting for using @PolyNull with legacy collection methods:
interface Collection<T extends @Nullable Object> {
  boolean contains(Collection<@PolyNull T> this, @PolyNull Object);
  boolean remove(Collection<@PolyNull T> this, @PolyNull Object);
}

@cpovirk
Copy link
Collaborator Author

cpovirk commented Dec 4, 2020

For filterNonNull, I wouldn't expect a @Nullable constraint on the receiver type. While it's true that it would be silly to call filterNonNull on a collection of known-non-null elements, there is an additional case, in which we don't know whether the elements are non-null or not:

Sequence<?> sequence = ...;
return sequence.filterNonNull();

For that call to be valid, we have to permit a call to filterNonNull on any receiver type.


As for allow vs. forbid: I suggest more of a middle course. We can treat it more like implementation code, leaving it unspecified. That way, we neither have to go to the trouble of banning it nor the trouble of defining what it means.

We do still have to say something, which I grant is probably just as hard to write as an outright ban would be. (And maybe we'd even write a relevant sample -- but perhaps not, given how rare receiver parameters are.) But I think this is still easier than defining behavior, and it leaves open the door for us to think more about the importance and semantics of that syntax in the future.


(For contains and remove: I feel like there must have been a discussion of this somewhere, but I can't find it at the moment.)


Constructors: Yes, that is ironic :)

@kevinb9n
Copy link
Collaborator

kevinb9n commented Jun 24, 2021

I would describe the IDEAL here -- with absolutely no suggestion of how either important or feasible it is -- as:

"Given a static method whose first parameter is of reference type Foo, and any valid way of null-annotating that method, then it can be refactored to become a Foo instance method in the expected way, including a receiver parameter if necessary, and the resulting method will share the nullness properties of the original, EXCEPT for these listed caveats (1) (2) (3)...."

@kevinb9n kevinb9n added the nullness For issues specific to nullness analysis. label Jul 2, 2021
@netdpb netdpb added this to the 1.0 milestone Sep 14, 2021
@kevinb9n
Copy link
Collaborator

Proposal (reaction emojis pls?):

First, I do think supporting this would at least not be nonsense; I see one clear expected interpretation:

  • a call-side receiver expression's augmented type is expected to type-check against the receiver-parameter's augmented type (as the type of an argument expression does for its corresponding parameter type)
  • within the method body, this should have that more specific type

BUT,

(Unlike other languages) Java chose not to support this kind of thing in the base type, so it'd just be strange for us to do it for the annotation part only. And if it does something like it in the future, it'd probably be better if we could take a fresh look at how to handle that then.

So I favor declaring these locations unrecognized. It would thus remain true that you cannot change the type of this.

Support?

@kevin1e100
Copy link
Collaborator

Maybe this is obvious, but what does "unrecognized" entail exactly? To name a few possibilities: are we asking tools to error when they see it, ignore it, or are they allowed to use it but JSpecify doesn't prescribe how, or something else? I guess I would prefer error but can get behind ignore. I'm less convinced allowing to use without specifying what it means works, given that--without thinking about it too hard--this could have bearing on overriding, for example.

@kevinb9n
Copy link
Collaborator

I'm just trying to figure out if there's already a bug where that discussion belongs or if I should (shudder) file it. I do have some specific thoughts.

@cpovirk
Copy link
Collaborator Author

cpovirk commented Jan 28, 2022

Coincidentally, I just cited the question of "unrecognized" in a doc I was putting together about open questions earlier this week.

Issues have occasionally touched lightly on this (like #136), but I'm not sure if any have gotten to the question of the definition. (I don't think anything came up about this during our spec reviews, either.)

The main current spec text on this:

A location is a recognized location for our type-use annotation in the circumstances detailed below. This spec does not define semantics for annotations in other locations.

When analyzing source code, tools are encouraged to offer an option to issue an error for an annotation in an unrecognized location (unless they define semantics for that location). Tools are especially encouraged to issue an error for an annotation in a location that is “intrinsically non-nullable” (defined below).

When reading bytecode, however, tools may be best off ignoring an annotation in an unrecognized location (again, unless they define semantics for that location).

There's been discussion in the past of requiring some behavior from tools for certain unrecognized locations. I'm not a fan of that for a few reasons, but I was mentioning this question in the doc because I likewise see it as a discussion we should have :)

@cpovirk
Copy link
Collaborator Author

cpovirk commented Jan 28, 2022

As to the actual question above: I gave a thumbs up for declaring these locations to be unrecognized.

Conveniently, I don't think any existing tools support checking of annotations on receiver type arguments -- which are the only parts that are relevant to nullness (OK, along with array components), since this itself can never be null. (CF has support but only for the "top-level" type, which it needs so that it can support @UnderInitialization Foo this.)

Personally, I find this feature to be even stranger than discussed above. If I write...

void copyTo(List<@Nullable E> this, List<E> destination);

...then I'm wondering if destination needs to likewise be treated as a List<@Nullable E>, as it would if we are substituting @Nullable E in for E everywhere. Maybe? I keep getting myself confused. So that is another reason that I'd be happy for us not to take this on.

@cpovirk
Copy link
Collaborator Author

cpovirk commented Jan 28, 2022

Sigh, sorry, I'm repeating myself from the initial post here. (I went looking for that post in other places but somehow never thought to look here!)

@kevinb9n
Copy link
Collaborator

kevinb9n commented Feb 2, 2022

Proposal remains: do not recognize JSpecify annotations as carrying any valid meaning when applied to any part of a receiver parameter's type.

@kevin1e100
Copy link
Collaborator

If we can ask tools to error on these in source code (and presumably ignore in bytecode) then that seems fine to me. Background is that I'm concerned that ignoring annotations in these locations completely could seemingly become an issue if we later want to give them meaning.

@kevinb9n
Copy link
Collaborator

kevinb9n commented Feb 2, 2022

Yes, I totally share that concern and have some rough suggestions about it; it's just that it's a cross-cutting concern to this particular question. I've been hesitating to open an issue on it quite yet, but given that I have pages of draft thoughts on it, I won't forget to.

@kevinb9n
Copy link
Collaborator

kevinb9n commented Feb 4, 2022

Personally, I find this feature to be even stranger than discussed above. If I write...

void copyTo(List<@Nullable E> this, List<E> destination);

...then I'm wondering if destination needs to likewise be treated as a List<@Nullable E>, as it would if we are substituting @Nullable E in for E everywhere. Maybe?

I don't think so? I think if we had reason to care about this at all, we could simply treat a receiver parameter exactly like a parameter, and a receiver expression (call-side) exactly like a (non-nullable) argument expression.

@cpovirk
Copy link
Collaborator Author

cpovirk commented Feb 4, 2022

I keep getting confused about what this means. Like, the following seems like it should be allowed:

void nullOutMatches(List<@Nullable E> this, Predicate<...> predicate) {
  for (int i = 0; i < size(); i++) {
    if (predicate.test(get(i)) {
      set(i, null);
    }
  }
}

But that would be allowed only if we know that set accepts a @Nullable E. And that would happen only if we performed substitution to replace every copy of E with @Nullable E. So presumably we'd do it on the parameter (which matters to callers) just as we do on the method calls (which matter only when checking the implementation code).

Anyway, I'm very happy to not get into this now. I just had this better example pop into my head when I read your message, so I'm writing it down before I forget it.

@cpovirk
Copy link
Collaborator Author

cpovirk commented Feb 4, 2022

Since kevinb9n bumped this and #86 at similar times, I made a connection!

FluentIterable<E> has a bunch of methods that return an Optional<E>, such as first(). It would be nice if those methods could be called only a on FluentIterable with a non-nullable element type.

It's possible that a tool could be smart enough to detect that it's calling a method that returns, say, an Optional<@Nullable String>, and it could act based on that information to issue an error. (Certainly I'd expect it to issue an error if you tried to write the type "Optional<@Nullable String>." But I wouldn't necessarily expect an error if you wrote fluentIterable().first().get().hashCode(), since the source code never names the type, even though an expression has that type.)

But another possibility is that a tool wouldn't detect the problem based on that but would detect the problem based on... a receiver type argument!

Optional<E> first(FluentIterable<@NonNull E> this)

(I guess that this particular approach to Optional.first and friends would require @NonNull, too, then.)

But given that tools already could detect this problem, it seems less compelling. Still, I'm recording it here.

[edit: Similarly, SetView has an immutableCopy() method that returns an ImmutableSet, and Ordering has an immutableSortedCopy() method that returns an ImmutableList.]

@kevinb9n
Copy link
Collaborator

kevinb9n commented Feb 4, 2022

I keep getting confused about what this means.

Oh that's only because it's confusing. As hell.

Seeing it a bit more clearly now: it's a disaster. The receiver parameter wants to project E, but the effect of that should be that every other E in the signature and body magically becomes the already-projected E.

Also, the use case is something Kotlin has features for and Java decidedly doesn't. So I think we should leave it alone.

@jspecify jspecify deleted a comment from cpovirk Feb 5, 2022
@kevinb9n
Copy link
Collaborator

kevinb9n commented Feb 5, 2022

I think it's fair to call this a "working decision" now, because it seems like any other decision would require a clear and compelling (and probably complex) proposal.

Working decision: Any JSpecify type-use annotation located on any (non-root?) type component of a receiver parameter type is classified as jspecify_unrecognized_location, meaning it definitively carries no meaning, like putting it to the left of a type parameter declaration or wildcard.

(Can go either way about "non-root" since null annotations won't work there anyway)

Feel free to reopen if you think it's being closed in error.

@kevinb9n kevinb9n closed this as completed Feb 5, 2022
@kevinb9n kevinb9n changed the title Should we specify a meaning for annotations on a receiver parameter's _type arguments_? Should we specify a meaning for annotations on a receiver parameter's _type arguments_? [working decision: no] Feb 5, 2022
@kevinb9n kevinb9n added the design An issue that is resolved by making a decision, about whether and how something should work. label Nov 30, 2022
@kevinb9n kevinb9n modified the milestones: 1.0, 0.3 Dec 2, 2022
@netdpb
Copy link
Collaborator

netdpb commented Apr 9, 2024

Current decision: No. Nullness annotations are unrecognized anywhere within a receiver parameter's type. [EDIT on 2024-06-14:] This decision for 1.0 does not prevent us from changing the spec in a future version to define semantics for these or other annotations in those positions.

Argument for changing: It's a special "one-off" exception that might not be worth having to call out. [edited in by kevinb9n]

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

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.

Results: Four 👍, one 👎. The 👎 has been resolved after further discussion with @wmdietl.

@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
@wmdietl
Copy link
Collaborator

wmdietl commented May 7, 2024

In other issues we valued uniformity of treatment, whereas here we add a special case that doesn't seem motivated.

Take this example:

import org.checkerframework.checker.nullness.qual.Nullable;

class MyBox<E extends @Nullable Object> {
  E f;

  MyBox(E in) {
    f = in;
  }

  void set(E in) {
    f = in;
  }
  
  void nullOutThis(MyBox<@Nullable E> this) {
    set(null);
  }

  void nullOutParam(MyBox<@Nullable E> in) {
    in.set(null);
  }
}

class User {
  void use(MyBox<String> mbs, MyBox<@Nullable String> mbns) {
    mbs.nullOutThis();      // error
    mbs.nullOutParam(mbs);  // error
    mbs.nullOutParam(mbns); // ok
        
    mbns.nullOutThis();      // ok
    mbns.nullOutParam(mbs);  // error
    mbns.nullOutParam(mbns); // ok
  }
}

nullOutThis should only be callable on a receiver that allows nullable values. This issue proposes to forbid this.
nullOutParam allows us to specify that the parameter needs to be a box of nullable values. We allow the @Nullable annotation on the type variable use here.

So for consistency, I would propose treating annotations on type variable uses in the type arguments of a method receiver like similar annotations in method parameters.
This likely won't affect many people, but adding a special case here seems unnecessary and forbidding the use in receivers prevents a meaningful usage.
(Note that these annotations are currently ignored in calls in EISOP, but we want to fix that: eisop/checker-framework#104)

@kevinb9n
Copy link
Collaborator

kevinb9n commented May 8, 2024

There's something weird about the nullOutThis example.

What it wants to say is: only allow calling this method when E is already nullable.
But what it is doing is: projecting E to nullable, implying that E itself might not be (and we don't care whether it is).

I feel more solidly about my thumbs-up now.

[EDIT: all this, from this comment and the previous, was already discussed above. See Feb 4 2022]

@wmdietl
Copy link
Collaborator

wmdietl commented May 8, 2024

There's something weird about the nullOutThis example.

What it wants to say is: only allow calling this method when E is already nullable.
But what it is doing is: projecting E to nullable, implying that E itself might not be (and we don't care whether it is).

Isn't that the same for nullOutParam? What is less confusing about the projection in that position?

@cpovirk
Copy link
Collaborator Author

cpovirk commented May 8, 2024

I think there's an asymmetry once E appears elsewhere in the signature:

E nullOutParam(MyBox<@Nullable E> in) {
  E result = in.f;
  in.set(null);
  return result; // error
}
E nullOutThis(MyBox<@Nullable E> this) {
  E result = f;
  set(null);
  return result; // NOT error
}

@netdpb
Copy link
Collaborator

netdpb commented May 17, 2024

Receiver parameters are not formal parameters, so I don't think we're required to treat them the same.

Also, Java doesn't let you do anything like that kind of narrowing constraint for generic receiver parameters. You can't do the following:

class Foo<T> {
  void method(Foo<String> this) { ... }
}

But of course you can do

class Foo<T> {
  void method(Foo<String> that) { ... }
}

I think if you wanted to do that kind of constraint, you'd need a static method:

class Foo<T extends @Nullable Object> {
  static <T> void method(Foo<@Nullable T> foo) { ... }
  static void methodForString(Foo<String> stringFoo) { ... }
}

@kevinb9n
Copy link
Collaborator

kevinb9n commented Jun 6, 2024

I apologize for parking more text here between now and when a doc is created for this issue. Just trying not to lose it.

I have no doubt the receiver parameters feature was created with just this thing in mind, and there's an irony or a sadness to us rejecting it anyway. I do think that in general annotating the receiver type can have meaning. But, this project has tripled down heavily on a "type system" model and "stay analogous to base types" has been an excellent North Star for us many times. (Granted, we don't apply it so zealously that we would, say, complain about a contravariant parameter type for that reason alone.)

We've been focusing on the strangeness that this creates within the method itself, not the value that could bring to the caller side. Maybe a compromise is that we say it has the first of these two effects only, not the second:

  1. a call-side receiver expression's augmented type is expected to type-check against the receiver-parameter's augmented type (as the type of an argument expression does for its corresponding parameter type)
  2. within the method body, this should have that more specific type

I'm still pretty scared this will bite us.

@kevinb9n kevinb9n reopened this Jun 6, 2024
@netdpb
Copy link
Collaborator

netdpb commented Jun 14, 2024

I've edited the proposal to clarify that we're not deciding that JSpecify will never recognize these annotations in these locations, just not in version 1.0.

Please adjust your votemojis accordingly!

@netdpb
Copy link
Collaborator

netdpb commented Jun 20, 2024

After discussion among myself, @kevinb9n, @wmdietl, and @cpovirk, we've decided that in JSpecify 1.0, nullness annotations will be unrecognized in receiver parameter type arguments, but without prejudice. @wmdietl will likely propose how they can be used to indicate that an instance method is intended to be called only on some parameterizations of a type.

That's really the same as the proposal from April 9, but it resolves @wmdietl's 👎.

@netdpb netdpb closed this as completed Jun 20, 2024
@netdpb netdpb changed the title Should we specify a meaning for annotations on a receiver parameter's _type arguments_? [working decision: no] Should we specify a meaning for annotations on a receiver parameter's _type arguments_? Jun 20, 2024
@netdpb netdpb removed the needs-decision-before-jar-1.0 Issues needing a finalized decision for the 1.0 jar release label Jun 20, 2024
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. nullness For issues specific to nullness analysis.
Projects
None yet
Development

No branches or pull requests

5 participants