"MINUS_NULL" and the future of explicit nulls

Language Design
1

Hello,
I was talking in the Make Null a subclass of AnyVal under -Yexplicit-nulls and things may be getting a little bit off topic, so I want to separate out my topic.

As a recap, the primary issue I’m declaring with this proposal is java interop, specifically with this problem from the Kotlin KEEP definitely non-nullable types proposal:

public interface JBox {
    <T> void put(@NotNull T t);
}

Basically, in Kotlin implementing this type required some way to say “T but without null”. Kotlin didn’t have user facing intersection types (they were always part of the spec but never user denotable). They had to add T & Any as an option to remove null.

We in Scala DO have intersection types and can currently express this like so:
T & (AnyRef | AnyVal). Of course this is very scuffed and not really intended or officially supported by the compiler, that being obvious with the new proposal.

What this topic is about if, in the future, we do say Null <:< AnyVal in explicit nulls (and eventually, all worlds as explicit nulls becomes the only type system, with the only variance being if the compiler reports these null errors), how will Scala correctly represent the above type?

What we need is some way to “cast away null” at the type level, and as well the compiler should correctly produce these kinds of types when @NonNull is explicitly used, instead of just skipping it. This ties into my idea to support jSpecify NullMarked and NullUnmarked annotations. The jSpecify spec is quite a good guide as a baseline for any implementation of null checking. Of course we don’t need to follow it to the letter, we aren’t actually tooling for java so we come first. However, for augmented types (basically, types that also have a nullness operator on them), they have some good rules.

Its rules more or less match the current rules scala uses when parsing java code:

  • If the type usage is annotated with @Nullable and not with @NonNull, its nullness operator is UNION_NULL

    In scala, this is T | Null or NullMode.Explicit

  • If the type type usage is annotated with @NonNull and not with @Nullable, its nullness operator is MINUS_NULL

    This is different from Scala, which instead uses NO_CHANGE, or NullMode.Skip

  • If the type usage is the parameter of equals(Object) in a subclass of java.lang.Record then its nullness operator is UNION_NULL

    This is some jank to prevent sadness with autogenerated record classes in null-marked scopes, as bytecode doesn’t mark the generated equals method as generated, meaning any manually written ones are can’t be seen as actually manually written. Scala doesn’t do anything with this info, this is purely some jSpecify jank.

  • If the type usage appears in a null-marked scope, its nullness operator is NO_CHANGE

    In the above linked PR this is indeed the behavior observed. The default mode in a null-marked scope is NullMode.Skip

  • By default, its nullness operator is UNSPECIFIED

    In Scala with flexible types, this is the same as T? or NullMode.Flexible

There’s an extra important aside that jSpecify has in their spec:

If tool authors prefer, they can safely produce MINUS_NULL in any case in which it is equivalent to NO_CHANGE. For example, there is no difference between Foo NO_CHANGE and Foo MINUS_NULL for any class type Foo (nor for any array type or the null type). The difference is significant for intersection types, type variables, and union types.

There is no difference between Foo NO_CHANGE and Foo MINUS_NULL for any class type Foo (or any array type or the null type). The difference is significant for intersection types, type variables and union types.

I think that Scala’s type system can handle this equivalence already, without any special casing. So I don’t really think there’s any harm in changing the @NonNull case from NullMode.Skip to a new NullMode.MinusNull, that adds an intersection with a type that holds all types except null. In current scala that type is AnyVal | AnyRef and in the future with the AnyVal Null proposal it will need to be a new type (my strawman type for this will be NotNull, defined as Any except for Null)

I don’t think Null can ever leave the type tree, for the simple fact that it needs to extend Matchable for c match { case null => ??? } to work. I personally wouldn’t like NotNull to be a magic compiler difference type but if that’s the only magic in explicit nulls world compared to null being the bottom type in non-explicit nulls then I could tolerate it.

Of course this MINUS_NULL business only really matters in a few select cases, but I think its worth keeping in mind. Something else that’s important is jSpecify’s rules also apply to type bounds, so we have to make sure to correctly transform a type parameters bounds.

I know this is quite a large post but I have a lot to say about this feature - I work very heavily with Minecraft mods which the whole deal there is interoping with Java, so any tiny imperfection is something I run into countless times. Some are easily fixable with shim libraries, but with explicit nulls it’s more of a fundamental issue. This isn’t a dig at explicit nulls, it’s greatly improved over the years (I remember ye old days of trying to use it and every thing in Minecraft being X | Null) and I suggest anyone using pure Scala use it.

If anyone has any additional feedback, I’d love to hear it. Thanks for reading this monster of a topic.

1 Like
2

You discarded the using erased NotGiven[Null <:< T] from the other thread but that seems to be a pretty idiomatic way to prevent that T is Null at the type level?

In general, I think Scala current behaviour of allowing put[Null](null) seems to be good design, as an unbounded generic should work with any type. It seems that the intent of @NonNull would be to prevent put[Object](null)which is prevented by default with explicit nulls in Scala.

If you don’t want to allow T to be null, then maybe def put[T <: AnyRef](t: T)would be what you want (or back to the using clause).

Or in other words, to me it seems that @NonNull T is meant to say „for any reference type that you might substitute for T, make sure that the concrete type does not allow for null“. Which is the default for explicit nulls.

Maybe I am not really understanding your usecase. Do you have any examples for behaviours you would like to prevent that are currently not expressible?

3

I like the idea of a `NullMode.MinusNull` (or maybe NullMode.NonNull) type that contains everything but null. It seems easy to understand, and unproblematic to use with existing type machinery.

4

the NullMode is a reference to compiler internals, so it’s not a literal type for Scala apps. Maybe I should have been more explicit about that. Scala would end up getting a type like NonNull

Kotlin currently uses the upper bound T: Any to do something like that. That guard is useful but it could complicate signatures coming from java (although afaik because its erased that mean it doesnt really matter)
That may be a useful way of declaring that a type can’t contain null, but right now erased is afaik experimental so maybe we don’t want to couch this bound behind an experimental gate.
Besides, why I discarded it there was because for that specific code snippet it was wrong.

public interface JBox {
    // code was slightly incorrect copied from the KEEP, so I'm fixing it here
    <T extends @Nullable Object> void put(@NonNull T t);
}

In a null marked scope, this is the canonical jSpecify representation of this code:

public interface JBox {
  <T extends Object UNION_NULL> void put(T MINUS_NULL t);
}

Again for almost every thing MINUS_NULL is the same as NO_CHANGE but for type parameters that’s not true.

The main use case is interop. That’s the reason Kotlin implemented this. Of course one may say “who cares about interop” but there are cases where a NonNull type would be useful and if that type existed then a MINUS_NULL mode could naturally fall out of that with T & NonNull.