Pain points for explicit null checking

[odersky]

Compiler version

3.1.3 RC1 with -Yexplicit-nulls

Minimized example

When reviewing #14032, I observed some pain points for explicit null checking that we might be able to fix. In decreasing order of importance:

1. Flow typing does not extend to variables of enclosing methods or fields of enclosing classes. It's clearly more difficult to know when a nullability info needs to be invalidated in these cases. But there is one situation, which happens to be the most common one, where I think we should be able to check nullability: It's when we know that a variable is initially null and every assignment to the variable is a non-null value. In that case, there's nothing to invalidate: once we know a variable is non-null at some point, it will stay non-null forever. If we could exploit that knowledge, the vast majority of caches in dotty could be null-checked without needing .nn.

   The tricky bit is sequencing. To know that all assignments are non-null we need to type check the program. But that means we might have to type check dereferences to a nullable variable first. We could try to find a better phase ordering. Maybe delay flow-typing until after typer. During type checking, always proceed under the unsafeNulls assumption. During subsequent flow typing, remove inserted .nn calls if they are redundant according to flow typing rules. If any inserted .nn calls remain, issue errors unless unsafeNulls is imported.

2. Calls to Java methods. Super annoying to have to write System.err.nn.println(...) or str.substring(a, b).nn. We should consider erring more towards unsoundness here.

3. eq, and ne should also work for nullable types. We create a lot of complexity in comparisons since that's currently not the case.

[olhotak]

eq and ne were discussed heavily here: https://contributors.scala-lang.org/t/wip-scala-with-explicit-nulls/2761
The suggestion there was to use == and != instead, which are defined on Any, while eq and ne are defined only on AnyRef (and a null is not an AnyRef).

[odersky]

There's a semantic difference between == and eq so I don't see how that suggestion could make sense. eq and ne clearly have to work on nulls as well. I realize this is tricky since eq right now is a member of AnyRef, but nevertheless we have to make it work.

[noti0na1]

Can we simply add this to Predef.scala?

extension (inline x: AnyRef | Null)
  inline def eq(inline y: AnyRef | Null): Boolean =
    x.asInstanceOf[AnyRef] eq y.asInstanceOf[AnyRef]
  inline def ne(inline y: AnyRef | Null): Boolean =
    !(x eq y)

[odersky]

Can we simply add this to Predef.scala?

I think this should work.

[olhotak]

On point 1, if we never assign null to a variable, could we make its type non-nullable and initialize it to uninitialized instead of to null? We would not be allowed to compare it to null (to test dynamically whether it is still uninitialized), but perhaps we can find or add a workaround. Maybe if x == uninitialized instead of if x == null, but that might be adding too much magic, proliferating uninitialized a bit too much.

[olhotak]

Here's another possible solution for 1. The idea is to use an explicit type MonotoneNull to state that we might read null from a field but we cannot write null into it. The flow typing would then take advantage of that.

type MonotoneNull <: Null
val initialNull = null.asInstanceOf[MonotoneNull]

class C {
  private var field: String | MonotoneNull = initialNull
  if field == null then field = "foo" // OK
  field = null // error
} 

It's possible to implement initialNull without the cast with some additional complexity that could be put in a library. The cast is here to keep it simple and communicate the idea.

[dwijnand]

That looks nice. You could also call that type Uninitialized: var field: String | Uninitialized. I think it would convey your semantics to many readers.