Flow-sensitive type inference

[abeln]

As per our last meeting, we need to support the following kinds of idioms: (easier)

// s: String|Null
if (s != null) {
  // s: String
}

and (harder)

if (s != null && s.length > 0 /*s: String in second test. Need to use the fact that && is short-circuit*/) {
}

[nafg]

1. Wouldn't it be easier to use pattern matching, which already can narrow a type (or does that already work)?

   s match {
   case null => ???
   case s1: String => ???
   }

2. If we're going to implement flow-sensitive typing, why not generalize it? If we look at Null as essentially the singleton type of null, is it any harder to also support this?

   if(i == 1) {
   // i has singleton type 1
   }

   Also

   if(i != 1) ??? else {
   // i has singleton type 1
   }

   I guess that's some form of type "substraction." How about the following?

   (??? : Int) match {
   case i if i != 1 => ???
   case i => // i has singleton type 1
   }

Once you have some support for machinery of "expression => infer type intersection or subtraction," you can implement that with the bare minimum of singleton (in)equality, but how far you take it is pretty open, as you say for instance how do you model &&. I'm sure there are many other ways to expand it.

[abeln]

1. Pattern matching already works.
2. Thanks for the suggestions. We're still deciding how general the flow sensitivity will be.

[abeln]

Implemented the following algorithm in https://github.com/abeln/dotty/commit/740790e2d21c251980ea3acf167f4db53ba2e801

Let NN(cond, true/false) be the set of TermRefs that we can infer to be non-null in cond if cond is true/false, respectively.

Then define NN by (basically De Morgan's laws)

• NN(x == null, true) = {x} if x is stable
• NN(x == null, false) = {}
• NN(x != null, true) = {}
• NN(x != null, true) = {x} if x is stable
• NN(A && B, true) = \union(NN(A, true), NN(B, true))
• NN(A && B, false) = \intersect(NN(A, false), NN(B, false))
• NN(A || B, true) = \intersect(NN(A, true), NN(B, true))
• NN(A || B, false) = \union(NN(A, false), NN(B, false))
• NN(!A, true) = NN(A, false)
• NN(!A, false) = NN(A, true)

Then to type If(cond, then, else), compute NN(cond), and type then and else with NN(cond, true) and NN(cond, false) in the context, respectively.

In the Typer, when typing either an Ident or Select, look up the TermRef in the context, and, if it's there, refine the type of the tree so that its denotation is always non-nullable.

[abeln]

We can type all of https://github.com/abeln/dotty/blob/explicit-null/tests/pos/explicit-null-flow.scala We still need to propagate the new type information inside the conditional:

val x: String|Null = ???
if (x != null && x.length > 0) { // need to know that x is non-null by this point
}

[abeln]

Another TODO: support for the feature in TASTy.

[abeln]

We still need to propagate the new type information inside the conditional: This is now done in https://github.com/abeln/dotty/commit/74039292ea9e10fbc23639ffcf5afee00585adf6

So we can now additionally support

val x: String|Null = ???
if (x != null && x.length > 0) {}

and

if (x == null || x.length == 0) {}

[abeln]

https://github.com/abeln/dotty/issues/7#issuecomment-445057335 is still a TODO. Another TODO: make sure that the error message mentions the refined type and not the symbol type. e.g.

  2 class Foo {
  3   class S {
  4     val s: String|Null = ???
  5   } 
  6   
  7   val s: S|Null = ???
  8   if (s != null && s.s != null && s.s.s != null) {
  9   } 
 10 } 

We get

-- [E008] Member Not Found Error: kk.scala:8:36 --------------------------------
8 |  if (s != null && s.s != null && s.s.s != null) {
  |                                                   ^^^
  |                            value `s` is not a member of Foo.this.S | Null

which refers to the type of s.s as Foo.this.S|Null, but we know is Foo.this.S (notice that S contains a String, not another S).

[abeln]

Algorithm for propagating nullability inside a condition:

When typing `A && B`
- type `A`
- compute NN(A)
- type B in the context augmented with NN(A, true)

Similarly, when typing `A || B`
- type `A`
- compute NN(A)
- type in B in the context with NN(A, false)

[abeln]

We now also support inference within blocks. See https://github.com/abeln/explicit-null-docs/blob/master/migration.md#non-local-control-flow-and-blocks for details.

This allows to handle cases like

def foo(x: String|Null): String = {
  if (x == null) return ""
  x.toLowerCase
}

Instead of return, we could've also used throw new NPE or any helper method that returns Nothing