> From: "Kevin Bourrillion" <[email protected]> > To: "Remi Forax" <[email protected]> > Cc: "valhalla-spec-experts" <[email protected]> > 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:[email protected] | > [email protected] ] > 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
