Null-annotating a lambda parameter type: when can it be, when must it be, what does it mean if it's not? [working decision: applicable when type is present, else inferred]

[kevinb9n]

The overall topic of implementation code, #114, is getting split out into #251 and #252 and now this. There is some brief discussion of lambda parameters in the original issue.

What is the deal with null-annotating lambda parameters?

Let's ignore nullness-unspecified types for now.

WHEN THE TARGET TYPE HAS NO WILDCARDS

All the lambda parameter base types will match those of the functional interface method signature exactly -- either they are inferred as such, or they themselves triggered that particular target type to be selected (target typing and/or maybe generic type inference too??), or they are spelled out just for clarity but still must match.

So, bringing nullness annotations into the picture: for ALL type components of the lambda parameter types, IF the types are given at all, our main choices are:

1. JSpecify dictates that all must be matched explicitly (max clarity, but a pain)
2. JSpecify dictates that none may be annotated because all will be inferred from the interface
3. JSpecify dictates that all will be inferred but it's harmless to annotate redundantly (could be confusing)
4. JSpecify dictates that lambda parameters are handled like local variables (annotate the subcomponents, don't annotate the root type)
5. JSpecify ignores how the lambda parameters are annotated because only the F.I. matters (let's scratch this)
6. JSpecify doesn't care what happens because this is implementation code

WHEN THE TARGET TYPE HAS WILDCARDS

Back to base types (without nullness annotation/analysis):

// m can pass only Strings into this consumer
void m(Consumer<? super String> c) {}

m(a -> out.println(a.hashCode()));

Javac target-types the base type of the lambda to Consumer<String>. You can coerce it to Consumer<Object> like this, but I see no real reason to:

m((Object a) -> out.println(a.hashCode()));

(Note this would've caused a pointless problem if a.length() were being called instead of a.hashCode().)

Now to add nullness to the mix (note: assume @NullMarked context from here on),

First note that a functionally-covariant type parameter should always simulate having no upper bound, i.e. always have @Nullable Object as its upper bound:

interface Consumer<T extends @Nullable Object> {
  void accept(T t);
}

Let's assume the method above is left as it was:

// m can pass only non-null Strings into this consumer
void m(Consumer<? super String> c) {}

(because if it had gotten annotated <? super @Nullable String> then for purposes of nullness annotations it should reduce to the same considerations as the no-wildcard case above.)

So all four of these parameter types would fit the target type:

m((String a) -> out.println(a.hashCode()));
m((Object a) -> out.println(a.hashCode()));
m((@Nullable String a) -> out.println(a.hashCode()));
m((@Nullable Object a) -> out.println(a.hashCode()));

Of course, #s 3 and 4 caused themselves a problem for no good reason. Yeah, it could be fixed by changing a.hashCode() to Objects.hashCode(a), but why bother? The signature of m guarantees we'll never actually be passed null anyway.

This suggests that maybe the same options we listed for the no-wildcards case are appropriate here too.

[artempyanykh]

JSpecify dictates that none may be annotated because all will be inferred from the interface

This can be really hard for us (esp. when fluent APIs, lambdas, and target typing are involved).

So far for lambdas we've adopted the convention that:

1. if the arg type is omitted then we try to infer it in a sense of augmented type,
2. if the arg type is specified it should be specified incl. root nullness.

Although 2 adds a bit more verbosity, it also allows devs to "tell" the analysis what the full augmented type is, when the analysis' inference fails to figure out on its own. It also makes makes lambda params behave more like method params rather than locals.

[kevinb9n]

Thanks!

I think your first convention is a given, since one cannot annotate anyway when the parameter type is omitted (even, I just discovered, if it has @Target(PARAMETER)).

It sounds like your tools' current answer is either option 1 or option 3 above. Thinking more about the difference, I realized this:

Suppose a tool notices a hard discrepancy in how an explicit lambda parameter type is null-annotated compared to what the target type requires. (This will usually be @Nullable being left out somewhere.) I suppose that the tool still has the information it needs to validate the implementation anyway. It could either let the target-type parameter "win", or it could use the more-specific of the two types (i.e. non-null for a root type or wildcard upper bound, nullable for a wildcard lower bound). I don't think JSpecify cares which.

If that rationale checks out, then the tool is probably free to decide whether to issue a warning about the discrepancy at all, which again I think JSpecify doesn't care about.

[artempyanykh]

I guess there's a mixed mode too e.g. foo((@Nullable var bar) -> bar.baz()) which we could read as 'given root nullness infer the rest', but this is not something we support yet.

When it comes to 1 vs 3, we probably fall under option 1.
We do check against hard discrepancies, e.g. in cases like

interface NullEater { void eat(@Nullable Object obj); }
interface Foo<T extends @Nullable>  {
  void takeEater(NullEater e);
  void takeConsumer(Consumer<T> c);
}
//
void bar(Foo<@Nullable String> foo) {
  foo.takeEater(Object s -> ...);
                    // ^-- BAD; missing @Nullable
  foo.takeConsumer(String s -> ...);
                       // ^-- BAD; missing @Nullable
}

We also take the declared type of lambda param as the source of truth (as augmented type) and check that the lambda body is consistent wrt this declared type.

However, in some cases the augmented target type of a lambda may be hard to infer for us, e.g.

<A, B> List<B> mapObj(List<A> ls, Function<A, B> mapper) {...}

mapObj(Arrays.asList("Hello", null), x -> ...)

The user can opt into declaring the type of the lambda

1. String x -> ... – OK, we take A = String and we warn about null in Arrays.asList.
2. @Nullable String x - OK, we take A = @Nullable String, the rest of the code type-checks fine.
3. [@Nullable] Object – also fine, forces A = [@Nullable] Object and also causes the target type of Arrays.asList to be List<[@Nullable] Object> rather than List<@Nullable String>.

Apologies if I'm reiterating something obvious with these examples, but I guess my main point is:

1. We want to be able to annotate lambda params because it allows devs to dial the exact behaviour they want in certain cases;
2. How the annotations are actually used seems tool-specific, but it's fine as it's implementation code anyways.

[msridhar]

We don't have any significant implementation experience with lambdas and generic types yet. But I am convinced by @artempyanykh's comments that we (NullAway) would want JSpecify to at least not prohibit the approach that NullSafe is currently taking with respect to nullability annotations and explicitly-typed lambda params (i.e., allow them to be written, and allow for treating them as ground truth).

[kevinb9n]

Here's what I'm thinking:

• A lambda parameter type, if it is given, is "nullness-applicable": it can be null-annotated, and when not its nullness is determined by surrounding @Null*arked
• We should decide whether a var lambda parameter is nullness-applicable or not. If not, it's probably like an unbounded ? perhaps? Considered nullable in null-marked code, unspecified in unspecified code? [edit: no]
• An analyzer can probably be free to decide whether to allow explicit parameter types to be contravariant; a downside is that then the explicit types give weaker hints to the type inference logic.

Here's some longer rumination I'd typed out (sorry) as I struggled to understand this issue from the bottom up.

---

In Java, every expression has a deterministic compile-time type, and a lambda expression is no exception. This type in turn makes the lambda’s return type and parameter types deterministic as well.

Javac takes care of all this for base types. And as long as it can still figure out a type, it lets the lambda omit as many parameter types as it wants to (individually with var, or all at once).

A nullness analyzer further needs to decide an augmented type for the lambda expression (and thereby for its parameters and return type). Its constraints are:

• First it must adhere to any target-side constraints if at all possible. Examples: if it’s class Foo<T>, or being passed to a Foo<String> parameter, we must not infer Foo<@Nullable String>.
• Any explicit types (and their subcomponents) that do appear in the lambda parameter list are considered “nullness-applicable”. They should at least be supertypes of what the lambda’s augmented type would predict (possibly required to match exactly?).
• (IF we decide nullness annotations are applicable to var in the lambda signature) the root nullness of a var parameter should match predicted

This determination should not take into consideration any nullness information coming from the body of the lambda. This suggests that type inference should be done in as “friendly” a manner toward the lambda body as possible without breaking any of the three constraints. So, in-types (to the lambda) would “prefer” to be non-null and out-types would prefer nullable. This way, a nullness error is likely to be pinpointed to a specific place in the lambda, where the code depended on (in-type being non-null / out-type being nullable) when that type legitimately can’t be. (Otherwise, I'd expect a more generic (no pun) error about the entire lambda expression type not fitting what its context expects.)

[cpovirk]

Note that type-use annotations can't be used with var (though declaration annotations can IIRC?). Even if not for that, I would assume that the nullness of a var lambda parameter would always be inferred (i.e., would not be nullness-applicable).

[kevinb9n]

Sure about that? This does compile in Java 18:

@Target(ElementType.TYPE_USE)
public @interface One {}
...
BiConsumer<?, ?> c = (var a, @One var b) -> System.out.println();

[kevinb9n]

Amusingly, this page cites it as the motivating reason for var on lambda params, while meanwhile we're not sure we'd even want to support it, ha.

[cpovirk]

Serves me right for commenting without testing it. Thanks!

But, but, but... that's not how var works with local variables! I can at least believe that type annotations are more likely to help on lambda parameters. But I'm also hung up on the idea that there's no type there. I mean, yeah, it's there but implicit, but... yuck. If you want a type, then write a type, not half of a type. Maybe I should try to find a JEP or other official document, as I feel I'm being unfair about this.

I would think that the nullness would be inferred in the absence of an annotation, as with lambda parameters without var, and as with local-variable var. I think that might be different from your proposal, which seems to be to make it Nullable (within NullMarked)?

And I would be inclined to say that annotations there are unrecognized. But maybe I'll look silly when someone tries this out in real code.

I was hoping to say that "unrecognized is the conservative option," since we can always define it later. But if the absence of an annotation means that the type is inferred, then obviously we can't safely change it to mean Nullable later :(

[cpovirk]

https://openjdk.org/jeps/323

They give the example of @NonNull, too.

The idea that we would do anything other than inference in the unannotated case feels at least conceptually at odds with:

We also want to enforce that the type inferred for a parameter of an implicitly typed lambda expression is the same whether var is used or not.

(Maybe only "conceptually" at odds with, since we might not have the same constraints as them. But definitely conceptually :))

[cpovirk]

One benefit of uniformity is that modifiers, notably annotations, can be applied to local variables and lambda formals without losing brevity:

Then they show @NonNull on both a var lambda parameter and a var local variable. That suggests to me that they're envisioning a declaration annotation, as a type-use annotation is definitely not applicable on a local variable.

After the quickest of skims through the JLS, my doubts are growing: I'm not actually sure that type-use annotations are "supposed" to be usable on var lambda parameters. I'll try to follow up on that. [update: posted to compiler-dev]

(Digression: This whole discussion is making me realize that inferred types end up in the bytecode, not just for var local variables but also for var (and otherwise implicitly typed) lambda parameters and other synthetic members, like bridge methods. Those won't have proper nullness annotations. I'll file an issue about that.... [update: #301])

[kevinb9n]

So my proposal included this

• (IF we decide nullness annotations are applicable to var in the lambda signature) ...

as a way of not going into it... then all the comments since then have been apparently only about that IF. I'll file it separately, but in the meantime, please note that I'm still awaiting feedback on the proposed resolution. @artempyanykh @msridhar

[cpovirk]

• We should decide whether a var lambda parameter is nullness-applicable or not. If not, it's probably like an unbounded ? perhaps? Considered nullable in null-marked code, unspecified in unspecified code?

If the "not" case, I would assume that the type would be inferred, rather than nullable. Otherwise, a lambda like e -> e.getKey() is going to fail nullness checking until it's rewritten to Entry e -> e.getKey() (OK, fine Entry::getKey in that case :)).

Your longer rumination suggested that you were at one point viewing inference as part of the picture. Is there something specific that drove you away from that?

[kevinb9n]

• We should decide whether a var lambda parameter is nullness-applicable or not. If not, it's probably like an unbounded ? perhaps? Considered nullable in null-marked code, unspecified in unspecified code?

Whoops. I did declare it on-topic to this issue. Sorry! Well, now I'm declaring it belongs to the new #303. :-) [EDIT: FIXED THAT]

Your longer rumination suggested that you were at one point viewing inference as part of the picture. Is there something specific that drove you away from that?

Can you explain what appeared to change in a little more detail? Might have been accidental. I'm speaking at the very edges of my comprehension.

[kevinb9n]

Anyway my real purpose in that comment had been just to give a reminder that the main proposal still needs input.

[cpovirk]

I was responding to:

If not, it's probably like an unbounded ? perhaps? Considered nullable in null-marked code, unspecified in unspecified code?

I see the "nullable" there as in conflict with "It's inferred." Since it sounds like we agree on "It's inferred," I think I'm just reading your bullet differently than you intended it.

[msridhar]

As the proposed resolution allows for writing explicit annotations alongside explicit lambda parameter types, it SGTM. I am also fine with not allowing nullness annotations on var lambda parameters for consistency with locals; I think if a developer wants to annotate a lambda parameter for nullness, they can be asked to give a full type and not use var.

[artempyanykh]

Lambda parameter types are "nullness-applicable"; they can be null-annotated, and when they are not they are seen as non-null (in null-marked code) or unspecified (in null-unmarked code).

I'd imagine unannotated param types should be treated as 'infer me' types. E.g.

Stream<@Nullable String> ss;
ss.map(x -> ...)

We would want the type of x to be @Nullable String so that if x is dereferenced in the body of the lambda we can flag it as an error; but also to improve the UX of fluent interfaces.

nullness annotations on var lambda parameters

To me, lambda params are closer to method parameters than to locals. Therefore, I don't see a problem with var denoting a root type while allowing @Nullable qualification and thus affecting the type argument of the lambda's target type. This also reminds me of auto and auto& in C++ – not saying it's a pinnacle of design but it's a precedent.

OTOH, we don't support annotated var lambdas. I also don't feel too strongly about this. So, if the group decides to forbid the pattern (@Nullable var x) -> ... and require spelling out the full type, I'll support this decision.

[kevinb9n]

Lambda parameter types are "nullness-applicable"; they can be null-annotated, and when they are not they are seen as non-null (in null-marked code) or unspecified (in null-unmarked code).

I'd imagine unannotated param types should be treated as 'infer me' types. E.g.

Stream<@Nullable String> ss;
ss.map(x -> ...)

We would want the type of x to be @Nullable String so that if x is dereferenced in the body of the lambda we can flag it as an error; but also to improve the UX of fluent interfaces.

Whoops! That text (now edited) meant to say that if the type is being supplied at all, then it works as described, i.e. no inference. But in your example, and in case of var x, then yes inference.

Only if x -> changes to (String x) -> the user would then have to change a step further to (@Nullable String x) ->... so we don't interfere with the "string means string" mentality. Until they do, I'd expect a report to the approximate effect that "the target type's parameter type String? is not convertible to the lambda expression's parameter type String!.

Hopefully that's more palatable!

The other part of your comment I'll move to the newer bug.

[kevinb9n]

Working decision: When a lambda parameter type is given (not var, not omitted), then it is "nullness-applicable", which means both: it can be null-annotated, and if not its nullness is subject to @Null*arked. When it is not given (either var or all types omitted), it's inferred.

If there's variation in how that inference could be done, then there could be possible benefit in standardizing how it works a bit, but let's let that shake out by way of the test suites.

[cpovirk]

Sounds like type-use annotations on var lambda parameters will indeed end up becoming invalid Java (thread, issue), so that's all the more reason for the decision we already made :)

[cpovirk]

(similar discussion about record patterns: uber/NullAway#840)

[netdpb]

Current decision: Lambda parameters that are var or untyped have their nullness inferred. @Nullable and @NonNull apply to those with explicit types just like method parameters.

Argument for changing: None.

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: This proposal received six 👍s and no other votes. It is finalized. I'll edit the title to reflect that.

[netdpb]

Decision: Lambda parameters that are var or untyped have their nullness inferred. @Nullable and @NonNull apply to those with explicit types just like method parameters.