Re: <@Nullable T> vs <T extends @Nullable Object>

[Piotr Zielinski]

On Mon, Nov 16, 2009 at 9:31 PM, Michael Ernst <mer...@cs.washington.edu> wrote:
> Piotr-
>
> Thanks for your question.
>
> I'd like to differentiate the syntax that is permitted by JSR 308 (Java's
> type annotations syntax) and the subset of that syntax that is used by the
> Checker Framework.  I'm not positive which of these you are referring to.

The Checker Framework.

>
>> public static <T extends /*@Nullable*/ Object> T identity(T object)
>> { return object; }  // works
>> public static </*@Nullable*/ T> T identity(T object) { return
>> object; }  // works
>>
>> Is the latter officially supported (the manual only mentions the
>> former).
>
> These are both permitted by JSR 308.
>
> Only the latter is officially supported by the Checker Framework (I guess
> that's the manual you are referring to).
>
> Someone could build a tool that uses the latter, or could enhance the
> Checker Framework to use the latter.
>
>> Also, for classes, only the former construct works, could somebody
>> comment on this?
>>
>> class Test<T extends /*@Nullable*/ Object> {}   // works
>> class Test</*@Nullable*/ T> {}  // doesn't work
>
> Our rationale was that having two distinct syntaxes for the same concept
> could be confusing to users, and the former more closely corresponds to the
> type-checker's rules.  (Or, do you want the two syntaxes to mean different
> things?)

Ideally, I think I'd prefer both of these syntaxes to mean the same,
in the same way as <T> and <T extends Object> mean the same. I'd vote
for allowing the <@Nullable T> syntax because is it is shorter than
'extends @Nullable Object', and the need for it is seems much more
common than for a generic 'extends @Nullable XXX'.

In my particular case, I'm adding @Nullable annotations to a shared
codebase, and the verbosity of 'T extends @Nullable Object' is the
number one complaint I hear. Many programmers browsing that codebase
don't care about jsr308, so the more jsr308 stuff I add, the more
people get confused. In particular, a java6 programmer unfamiliar
with jsr308 sees '<T extends /*@Nullable*/ Object>' as '<T extends
Object>' and is confused why the code isn't just '<T>'.
</*@Nullable*/ T> is easier to understand.

Thanks,
Piotr
>
>                    -Mike
>
>
> PS:  If the discussion is about the Checker Framework, then let's move
> followups to checker-fram...@googlegroups.com .
>

[Artemus Harper]

I would really like to minimize the number of different ways there are
to express the same coding statement. The 'extends' statement might be
harder to understand, but not correctly understanding what it means
can lead to further problems down the road (I've seen many developers
that think 'import' is the same as the c '#include' statement).

<T extends Object> should read: where T is a Object. And by extension,
<T extends @Nullable Object> should read: where T is a nullable
Object. Since non-null is a subset of nullable, it makes sense to type
T as @NonNull String.

[Adam Warski]

Hello,

I think that this only makes using the checker annoying to use, and will discourage developers from trying it out (I can see people spending an hour trying to figure out what's wrong, only to find out later that that have to write "T extends @NonNull Object", and ultimately dumping the tool altogether).

If nobody every writes <T extends Object>, I see no reason why the checkers framework would require people to do so. If the tool can be easier to use, why make it harder? :)

Adam

[Mahmood Ali]

Greetings Piotr,

First, I want to apologize for not handling this request well on my
end. I just went through this discussion and I just realized that I
was making assumptions about some undocumented behavior and I didn't
communicate that well in my replies and the code Issue.

=====================
Summary:

<@Nullable T> could have two meanings:
(1) be a syntactic sugar for <T extends @Nullable T>. This is nice
and compact.
(2) be a restriction on T, so T has to be of nullable type. So if
we have `MyClass<@Nullable T> { ... }`, we can only construct it with
a nullable type arguments e.g. `new MyClass<@Nullable String>()` but
not `new MyClass<@NonNull String>()`. This is a bit more expressive,
and may be desirable. I should admit that I haven't run into cases
where this is desirable.

With this proposal, we lose the ability to describe the second case.
=====================

First of all, actually, the Checker Framework does have different
semantics for both syntaxes, e.g. <T extends @Nullable Object> and
<@Nullable T>, as type parameter declaration. The difference is a bit
subtle.

But before describing the proposals, let's examine the use cases of
the constraints, as they'll guide us through the evaluation. There
are few possible constraints for the type parameters:

1. Constraining the qualifier of the upper bound of a type. For
example, PriorityQueue can only accept NonNull elements, while
LinkedList (another Queue) may have Nullable elements. The syntax for
that is:

class PriorityQueue<E extends @NonNull Object> { ... }
class LinkedList<E extends @Nullable Object> { ... }

Here, one would expect `E` to resolved to the proper concert type that
is passed in construction phase:

new PriorityQueue<@NonNull String>().element() is @NonNull String
new LinkedList<@NonNull String>().element() is also @NonNull String

2. Sometimes, particular use of the type parameter needs to ignore
qualifier and preserve the Java type. Map.get() is the most known
example. Map.get() type is Nullable regardless of the declaration of
the receiver map. Similarly, Queue.peek() could always return null,
even for PriorityQueue. The syntax for this is:

for PriorityQueue: @Nullable E peek();
for Map: @Nullable V get(k k);

The previous two cases are the documented cases. The following ones
are the questionable uses and not that popular:

3. A class may be parameterized, but every single use of the parameter
type has its qualifier overriden. Consider the reflection class
Constructor<T>.
Whether we have a reference of Constructor<@Nullable String> or
Constructor<@NonNull String>, constructor.newInstance() is always
@NonNull Constructor. Class<T> is the same (with the exception for
Class.cast() return type that needs to be @PolyNull).

To express this, one can either restrict in those class to <T extends
@NonNull Object>, or simply override every single use of T in the
class body of such classes. The first approach is limited in
capability (it doesn't handle the case where every single use is
overriden with @Nullable).

4. A class may decide to restrict its instantiation of its parameters
to a particular qualifier, as an invariant constraint. Consider the
following hypothetical method:

public <T> void addNullToList(List<T> list) { list.add(null); }

Here, we want to express that T has to be of Nullable type, not just a
subtype of Nullable Object. In other words, you want to express T as
<T extends @Nullable Object super @Nullable <Bottom-Type>>.

This case differs from the previous case, in that it actually requires
checking in the call site (i.e. addNullToList(List<@NonNull String>)
is invalid, while `new Class<@Nullable String>()` may be valid.

Behavior And Proposals:

The Checker Framework up to this current release (1.0.2), uses
<@Nullable T> to refer to case 3, but we are considering changing it
to mean case 4 (similar to previously but with type checking the call
sites).

The proposal put here, basically eliminates the possibility of
expressing these constraints, so there wouldn't be a possibility of
expressing the method `addNullToList`. Granted though, we haven't run
into many case 4s in the wild, only case 3 so far.

I think we could use some feedback on whether it's more desirable to
have more expressive syntax (i.e. treat <@Nullable T> as <T extends
@Nullable Object super @Nullable void>) or more compact syntax (i.e.
<@Nullable T> as <T extends @Nullable Object>).

Note, the same problem occurs with wildcards, but wildcards are a
different beasts on their own, since almost every use of a wildcard is
a declaration by itself.

Thanks again, and sorry for the long reply.

Regards,
Mahmood

[Adam Warski]

Hello,

> Here, we want to express that T has to be of Nullable type, not just a
> subtype of Nullable Object. In other words, you want to express T as
> <T extends @Nullable Object super @Nullable <Bottom-Type>>.

That's more or less what I wrote in the other thread.

> The Checker Framework up to this current release (1.0.2), uses
> <@Nullable T> to refer to case 3, but we are considering changing it
> to mean case 4 (similar to previously but with type checking the call
> sites).
>
> The proposal put here, basically eliminates the possibility of
> expressing these constraints, so there wouldn't be a possibility of
> expressing the method `addNullToList`. Granted though, we haven't run
> into many case 4s in the wild, only case 3 so far.

You haven't run into a case where you want to add a null to a list? I certainly think this should be possible :]. (Unless I'm missing the point here?) And it's not really a @NotNull/@Nullable discussion, but what the semantics of annotated type parameters should be in general. I can bet there are other type annotations, which also use inheritance, which will also exhibit the problem.

Adam

[Piotr Zielinski]

On Sat, Dec 5, 2009 at 2:58 AM, Mahmood Ali <msae...@gmail.com> wrote:
> I think we could use some feedback on whether it's more desirable to
> have more expressive syntax (i.e. treat <@Nullable T> as <T extends
> @Nullable Object super @Nullable void>) or more compact syntax (i.e.
> <@Nullable T> as <T extends @Nullable Object>).

Ok, now I understand the tradeoff. It seems that the answer may
depend on which of the following two interpretations you adopt.
Interpretation 2 with @PolyNull may be worth looking at.


Interpretation 1 (more or less the current one).

The @Nullable/@NonNull annotations are used to enrich the type system
and then more or less disappear from the picture. For example, the
subtype relationship between @NonNull Object and @Nullable Object is
no more special than that between @NonNull Object and @NonNull String.

In this view, the extends/super mechanism is the primary way of
expressing all type constraints (including nullability). For example,
to express any type, you write <T extends @Nullable Object>. The
meaning of <@Nullable T> or <@NonNull T>, if anything, is just
syntactic sugar for extends/super.

The nice thing about this interpretation is that it reuses the
existing extends/super mechanism to express type constraints.
Unfortunately, the current extends/super syntax in java is not
complete, so some types (eg <T super @Nullable Bottom>) cannot be
expressed (at least not without assigning a special meaning to
<@Nullable T>).


Interpretation 2.

The @Nullable/@NonNull annotations and the standard type system are
orthogonal and handled independently. The extends/super mechanism is
used exclusively for constaints on standard types, and
@Nullable/@NonNull/@PolyNull annotations are used for specifying
nullness. In this interpretation:

<@Nullable T extends String>
T can be @Nullable String but not @NonNull String

<@NonNull T extends String>
T can be @NonNull String but not @Nullable String

<T extends @Nullable String>
doesn't mean anything, extends can only be used on non-annotated types

To express a type that can be both nullable or not, use @PolyNull:

interface Something<@PolyNull T> {
void method1(@PolyNull T object);
void method2(@Nullable T object);
void method3(@NonNull T object);
void method4(T object); // default nullability
}

expands to

interface Something<String> {
void method1(String object);
void method2(@Nullable String object);
void method3(@NonNull String object);
void method4(String object);
}

interface Something<@Nullable String> {
void method1(@Nullable String object);
void method2(@Nullable String object);
void method3(@NonNull String object);
void method4(String object);
}

interface Something<@NonNull String> {
void method1(@NonNull String object);
void method2(@Nullable String object);
void method3(@NonNull String object);
void method4(String object);
}

The nice thing about this interpretation is that generic and concrete
variable declaration (eg 'String obj' and 'T obj') obey the same
default nullability rules. You don't have to check the constraints on
T to find out whether it's nullable or not.

Thoughts?

Piotr

[Michael Ernst]

Piotr-

> The @Nullable/@NonNull annotations are used to enrich the type system

Yes, this is the fundamental idea behind the Checker Framework: using type
qualifiers for pluggable type-checking. This reuses the ideas and
mechanism of type-checking, which programmers are already familiar with.

You could imagine other ways to build program analysis tools, and you could
even use type annotations to do it.


In your interpretation 2, different syntax and semantics are used for types
and for type qualifiers. I fear that the non-uniformity may confuse
programmers. Also, it seems less expressive than the current semantics.
As one example, suppose that you have a hierarchy of type qualifiers of
depth 3: @A, @B, and @C, and suppose that you would like to express that
the qualifier should be @B or less (that is, @B or @C). Some other things
become less convenient, such as having a @PolyNull method whose parameter
varies independently of the type parameter of the enclosing @PolyNull class
-- this is a common use case. You note as an advantage that "You don't

have to check the constraints on T to find out whether it's nullable or

not." However, you have to check the constraints on T to understand T in
any event, so this does not seem like a significant advantage.

All that said, it's true that the syntax

interface Something<@PolyNull T> { ... }

is not currently claimed by the Checker Framework and could possibly be
used for something. Thanks for the ideas about that.

-Mike