Null restricted type and JSpecify

[forax at univ-mlv.fr]

> From: "Kevin Bourrillion" <kevinb at google.com>
> To: "Remi Forax" <forax at univ-mlv.fr>
> Cc: "valhalla-spec-experts" <valhalla-spec-experts at openjdk.java.net>
> Sent: Wednesday, November 23, 2022 8:23:22 PM
> Subject: Re: Null restricted type and JSpecify

> There were some offline musings related to this but no actual "proposal". Not
> sure what Brian will come up with.

yes, sorry, 

> I'm very glad for more awareness of our work obviously... but I don't want to
> overstate how directly applicable it is to Valhalla. The relationship between
> the two could be more complex; I'm only interested that we can see some path
> toward future unification, and we can convince ourselves we're not stepping off
> that path.

That was my idea too, the question is not to make JSpecify be to driver of Valhalla or whatever but to be sure that Vahalla does not impede the existence of JSpecify. 

> On Wed, Nov 23, 2022 at 5:04 AM Remi Forax < [ mailto:forax at univ-mlv.fr |
> forax at univ-mlv.fr ] > wrote:

>> - there is no @NonNull, a lack of @Nullable inside a @NullMarked scope encodes
>> the fact that a type is non null.
> (Well, we did eventually add it; the [
> https://jspecify.dev/docs/api/org/jspecify/annotations/NonNull.html | javadoc ]
> explains why. Sorry the spec isn't current. The javadoc and design faq are much
> more so.)

I see, for the case where a user want a non null type argument of a parameterized type declared with a nullable type parameter. 

>> JSpecify is specified in term of subtyping relationship not in term of
>> boxing/unboxing rules.
> From our reading of the JLS, this was just the most convenient way to do it. If
> it goes wrong somehow, we missed that.

I think i prefer the boxing relationship, even ignoring Valhalla, because it allows unsafe casting by example from a List<@Nullable T> to a List<@NonNull T> and vice versa. 
So adding a @Nullable / @NonNull is something that can always be done afterward to fix a mistake in how the code was nullified (== generified for null). 

Rémi 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/valhalla-spec-observers/attachments/20221130/a9f33929/attachment.htm>