Null restricted type and JSpecify

[Remi Forax]

Hi all,
i've taken a look to JSpecify [1] to see how it works with the recent proposal from Brian, seen value types as null restricted types.

Obviously, i'm not an expert in the details of JSpecify so feel free to correct me.

I really like JSpecify, the specification is simple and lean but yet at the same time guides users towards a null safe Java.

JSpecify specifies two annotations, @NullMarked and @Nullable. @NullMarked (on a class, a package or a module) says that any types in that scope is not null (NO_CHANGE) by default. @Nullable indicates that a type is nullable (UNION_NULL), inside a @NullMarked scope or not.
A type outside the the @NullMarked scope and not marked as @Nullable is unspecified (UNSPECIFIED) [2].

Compared to the null restricted type proposal, there are IMO two major differences,
- the fact that JSpecify uses annotations implies that adding nullness information is a binary backward compatible change.
- there is no @NonNull, a lack of @Nullable inside a @NullMarked scope encodes the fact that a type is non null. 

The former suggests that we should investigate erasing Q-type to L-type inside method/field descriptors. The later suggests that either we should embrace this approach too and only provides '?' or we should allow both '!' (NO_CHANGE) and '?' (UNION_NULL) but it makes the transition from actual Java to a null safe Java less clear.

The other difference, which was noted by Kevin during our meeting last week, JSpecify is specified in term of subtyping relationship not in term of boxing/unboxing rules. For me, boxing/unboxing rules are less specific that subtyping in assignments but more specific in case of overriding, so i've no idea if this is an issue or not.

regards,
Rémi

[1] https://jspecify.dev/
[2] there is a 4th state which is MINUS_NULL but it's for type variable, so not something which is directly related to value types.