Null restricted type and JSpecify

[forax at univ-mlv.fr]

----- Original Message -----
> From: "John Rose" <john.r.rose at oracle.com>
> To: "Remi Forax" <forax at univ-mlv.fr>
> Cc: "valhalla-spec-experts" <valhalla-spec-experts at openjdk.java.net>
> Sent: Wednesday, November 30, 2022 6:01:42 PM
> Subject: Re: Null restricted type and JSpecify

> Kevin & co won’t like this maybe, but I think this design and our Valhalla
> design do not conflict, precisely because they make completely distinct sets of
> assertions, and yet the assertions (taken together) are consistent.
> 
> What we are talking about here is X! on non-type-vars.  That means we are adding
> a state EXPLICIT_MINUS_NULL, which (a) has an obvious relation to the other
> states in JSpec., and (b) can have a semantic weight different from anything in
> JSpec.; it can and should translate to a different Q-descriptor.

if it's L-descriptor in descriptors but Q-descriptor in TypeRestriction + bytecodes, yes !

I think being able to add a '!' if you have overlook one should be an option.

Rémi

> 
> On 23 Nov 2022, at 5:03, Remi Forax wrote:
> 
>> 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.