Improve painpoint in -Yexplicit-nulls: Recognize a field is monotonically non-null

Language Design
1

Let’s start with motivating example. Here is a field that starts as null, but once it is set, it can never again become null again.

object A {
  private var s: String | Null = null

  def setA(newS: String): Unit =
     s = newS

  def doWork: Unit =
     if (s != null) println(s.toUpperCase) // does not compile now, but it should
}

In this case, the flow checker can know that after a null check the access if safe, even in multi-threaded environment.

This proposal would be limited to only private var fields, and possibly local variables that are passed into lambdas, for example map / foreach or other closures. In both of these cases, it is a feasible effort to check all the assignments and conclude that none of them are null reassignments.

Previous references

There are previous efforts that tried to introduce an new “Unitialized” keyword, which I believe is a wrong solution. The flow typing checker is already inspecting the code, so this can work outside the box without introducing new language concepts (beyond what already exists).

Also tagging @olhotak here.

1 Like
2

I don’t understand the example, wouldn’t this just be flow-typing ?

val s: String | Null = null // can be a var or def as well

if s != null then
  // in this scope, s can have type String, since we know it's not null
  println(s.toUpperCase)

The issue with lateinit-like systems like you are proposing is that they are a soundness hole
“Eventually not null” is useful documentation for a programmer, but the compiler cannot act on it unless it knows which events (e.g. calling setA) makes the field non-null
And then it needs to prove that for a certain location (e.g. s.toUpperCase), all paths leading up to it do contain one of those events:

class LatePair:
  private var x: Int | Null = null
  private var y: Int | Null = null
  private var is_initialized: Boolean = false

  def init(x: Int, y: Int): Unit =
    this.x = x
    this.y = y
    this.is_initialized = true

  def sum(): Int =
     if is_initialized then
       // we can intuitively see this is safe, but hard to automatically prove !
       this.x + this.y
     else
       0

This is undecidable, so you would need a syntactical heuristic

Which goes back to path typing, the nice thing is that it’s fully syntactical: does the if’s condition check if the thing is not-null ? If yes, can remove Null from its type

3

I would very much like that, but I don’t think it’s feasible.

In order to decide whether any rhs is nullable, you need to typecheck it. But to typecheck it, you need to typecheck what comes before, and that could require the type of s. A direct-though-contrived example is:

def doWork(): Unit = {
  if (s != null)
    s = s // is this a nullable rhs or not?
}

Realistically, this is going to be more complicated, but it shows that you can’t a priori decide which rhs’es will be nullable or not. Since you cannot typecheck method bodies without deciding which fields are monotonic, and you can’t decide which fields are monotonic without typechecking method bodies, you’re stuck.

A possible escape to that would be similar to @stableNull. You explicitly annotate relevant fields with @monotonicNull. Then you can typecheck method bodies assuming they are indeed monotonic. And they you can check afterwards that it was indeed monotonic. That could work, I think.

It might even make @stableNull much more niche, if useful at all. It would be nice to get rid of that one, because it’s unsafe (by design).

2 Likes
4

I really like your idea of safe @stableNull and the approach to achieve it.

The current one is easy to shoot yourself in the foot with. Is it too late to deprecate / remove it and have a safe solution instead?

Also, does stable null only work on class fields? What about local variables, something like this exaple:

def f: String = {
   var a: String | Null = null
   list.foreach { _ => a = "exists" }
   if (a != null) a.toUpperCase else "EMPTY"
}
5

As @sjrd explained in detail, the flow-sensitive analysis needs to happen during typing, when the compiler does not yet know the types of other expressions and therefore does not know whether assignments may write null into the variable.

The technical core of the earlier solution was to use type bounds to give the variable a type that is nullable when the variable is read but non-null when the variable is written. Such a type would then allow the flow-sensitive analysis to conclude that, once it has already observed a non-null value in the variable, that value will not then be overwritten with null in the future.

This was achieved in the earlier solution by a declaration type Uninitialized <: Null. In the scope of such a declaration, using String as an example, we have String <: String | Uninitialized <: String | Null. Thus, a variable of type String | Uninitialized then has exactly the desired property needed by the analysis: a value read from it is know to have type String | Null, but a value written to it is required to have type String. If the variable is ever observed to contain a non-null value, the analysis can conclude that it will continue to remain non-null and narrow the type read from it to String.