----- Original Message ----- > From: "John Rose" <[email protected]> > To: "Remi Forax" <[email protected]> > Cc: "valhalla-spec-experts" <[email protected]> > 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.
