<html><body><div style="font-family: arial, helvetica, sans-serif; font-size: 12pt; color: #000000"><div><br></div><div><br></div><hr id="zwchr" data-marker="__DIVIDER__"><div data-marker="__HEADERS__"><blockquote style="border-left:2px solid #1010FF;margin-left:5px;padding-left:5px;color:#000;font-weight:normal;font-style:normal;text-decoration:none;font-family:Helvetica,Arial,sans-serif;font-size:12pt;"><b>From: </b>"Kevin Bourrillion" <kevinb@google.com><br><b>To: </b>"Remi Forax" <forax@univ-mlv.fr><br><b>Cc: </b>"valhalla-spec-experts" <valhalla-spec-experts@openjdk.java.net><br><b>Sent: </b>Wednesday, November 23, 2022 8:23:22 PM<br><b>Subject: </b>Re: Null restricted type and JSpecify<br></blockquote></div><div data-marker="__QUOTED_TEXT__"><blockquote style="border-left:2px solid #1010FF;margin-left:5px;padding-left:5px;color:#000;font-weight:normal;font-style:normal;text-decoration:none;font-family:Helvetica,Arial,sans-serif;font-size:12pt;"><div dir="ltr"><div>There were some offline musings related to this but no actual "proposal". Not sure what Brian will come up with.</div></div></blockquote><div><br></div><div>yes, sorry,<br data-mce-bogus="1"></div><div><br data-mce-bogus="1"></div><blockquote style="border-left:2px solid #1010FF;margin-left:5px;padding-left:5px;color:#000;font-weight:normal;font-style:normal;text-decoration:none;font-family:Helvetica,Arial,sans-serif;font-size:12pt;"><div dir="ltr"><br><div>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.</div></div></blockquote><div><br></div><div>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.<br data-mce-bogus="1"></div><div><br data-mce-bogus="1"></div><blockquote style="border-left:2px solid #1010FF;margin-left:5px;padding-left:5px;color:#000;font-weight:normal;font-style:normal;text-decoration:none;font-family:Helvetica,Arial,sans-serif;font-size:12pt;"><div dir="ltr"><br><br><div>On Wed, Nov 23, 2022 at 5:04 AM Remi Forax <<a href="mailto:forax@univ-mlv.fr" target="_blank">forax@univ-mlv.fr</a>> wrote:<br></div><div dir="ltr"><br></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">- there is no @NonNull, a lack of @Nullable inside a @NullMarked scope encodes the fact that a type is non null.</blockquote><br><div>(Well, we did eventually add it; the <a href="https://jspecify.dev/docs/api/org/jspecify/annotations/NonNull.html" target="_blank">javadoc</a> explains why. Sorry the spec isn't current. The javadoc and design faq are much more so.)</div></div></div></blockquote><div><br></div><div>I see, for the case where a user want a non null type argument of a parameterized type declared with a nullable type parameter. <br data-mce-bogus="1"></div><div><br data-mce-bogus="1"></div><blockquote style="border-left:2px solid #1010FF;margin-left:5px;padding-left:5px;color:#000;font-weight:normal;font-style:normal;text-decoration:none;font-family:Helvetica,Arial,sans-serif;font-size:12pt;"><div dir="ltr"><div class="gmail_quote"><br><br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">JSpecify is specified in term of subtyping relationship not in term of boxing/unboxing rules.</blockquote><br><div>From our reading of the JLS, this was just the most convenient way to do it. If it goes wrong somehow, we missed that.</div></div></div></blockquote><div><br></div><div>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.<br data-mce-bogus="1"></div><div>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).<br data-mce-bogus="1"></div><div><br data-mce-bogus="1"></div><div>Rémi<br></div><div><br data-mce-bogus="1"></div></div></div></body></html>