Add flow typing to doc

noti0na1 · noti0na1 · commit 49d550e1bd5a · 2019-12-04T15:25:42.000-05:00
diff --git a/docs/docs/internals/explicit-nulls.md b/docs/docs/internals/explicit-nulls.md
@@ -28,9 +28,6 @@ We change the type hierarchy so that `Null` is only a subtype of `Any` by:
 
 ## Java Interop
 
-TODO(abeln): add support for recognizing nullability annotations a la
-https://kotlinlang.org/docs/reference/java-interop.html#nullability-annotations
-
 The problem we're trying to solve here is: if we see a Java method `String foo(String)`,
 what should that method look like to Scala?
   - since we should be able to pass `null` into Java methods, the argument type should be `String|JavaNull`
@@ -43,25 +40,19 @@ At a high-level:
   - we do this in two places: `Namer` (for Java sources) and `ClassFileParser` (for bytecode)
   - whenever we load a Java member, we "nullify" its argument and return types
 
-The nullification logic lives in `JavaNullInterop.scala`, a new file.
-
-The entry point is the function `def nullifyMember(sym: Symbol, tp: Type)(implicit ctx: Context): Type`
-which, given a symbol and its "regular" type, produces what the type of the symbol should be in the
-explicit nulls world.
-
-In order to nullify a member, we first pass it through a "whitelist" of symbols that need
-special handling (e.g. `constructors`, which never return `null`). If none of the "policies" in the
-whitelist apply, we then process the symbol with a `TypeMap` that implements the following nullification
-function `n`:
-  1. n(T)              = T|JavaNull              if T is a reference type
-  2. n(T)              = T                       if T is a value type
-  3. n(T)              = T|JavaNull              if T is a type parameter
-  4. n(C[T])           = C[T]|JavaNull           if C is Java-defined
-  5. n(C[T])           = C[n(T)]|JavaNull        if C is Scala-defined
-  6. n(A|B)            = n(A)|n(B)|JavaNull
-  7. n(A&B)            = (n(A)&n(B))|JavaNull
-  8. n((A1, ..., Am)R) = (n(A1), ..., n(Am))n(R) for a method with arguments (A1, ..., Am) and return type R
-  9. n(T)              = T                       otherwise
+The nullification logic lives in `compiler/src/dotty/tools/dotc/core/JavaNullInterop.scala`.
+
+The entry point is the function
+`def nullifyMember(sym: Symbol, tp: Type, isEnumValueDef: Boolean)(implicit ctx: Context): Type`
+which, given a symbol, its "regular" type, and a boolean whether it is a Enum value definition,
+produces what the type of the symbol should be in the explicit nulls world.
+
+1. If the symbol is a Enum value definition or a `TYPE_` field, we don't nullify the type
+2. If it is `toString()` method or the constructor, or it has a `@NotNull` annotation,
+  we nullify the type, without a `JavaNull` at the outmost level.
+3. Otherwise, we nullify the type in regular way.
+
+See `JavaNullMap` in `JavaNullInterop.scala` for more details about how we nullify different types.
 
 ## JavaNull
 
@@ -73,32 +64,46 @@ val s: String|JavaNull = "hello"
 s.length // allowed, but might throw NPE
 ```
 
-`JavaNull` is defined as `JavaNullAlias` in `Definitions`.
+`JavaNull` is defined as `JavaNullAlias` in `Definitions.scala`.
 The logic to allow member selections is defined in `findMember` in `Types.scala`:
   - if we're finding a member in a type union
   - and the union contains `JavaNull` on the r.h.s. after normalization (see below)
   - then we can continue with `findMember` on the l.h.s of the union (as opposed to failing)
 
 ## Working with Nullable Unions
 
-Within `Types.scala`, we defined a few utility methods to work with nullable unions. All of these
+Within `Types.scala`, we defined some extractors to work with nullable unions:
+`OrNull` and `OrJavaNull`.
+
+```scala
+(tp: Type) match {
+  case OrNull(tp1) => // if tp is a nullable union: tp1 | Null
+  case _ => // otherwise
+}
+```
+
+These extractor will call utility methods in `NullOpsDecorator.scala`. All of these
 are methods of the `Type` class, so call them with `this` as a receiver:
-  - `isNullableUnion` determines whether `this` is a nullable union. Here, what constitutes
-     a nullable union is determined purely syntactically:
-       1. first we "normalize" `this` (see below)
-       2. if the result is of the form `T | Null`, then the type is considered a nullable union.
-          Otherwise, it isn't.
-  - `isJavaNullableUnion` determines whether `this` is syntactically a union of the form `T|JavaNull`
-  - `normNullableUnion` normalizes `this` as follows:
-      1. if `this` is not a nullable union, it's returned unchanged.
-      2. if `this` is a union, then it's re-arranged so that all the `Null`s are to the right of all
-         the non-`Null`s.
-  - `stripNull` syntactically strips nullability from `this`: e.g. `String|Null => String`. Notice this
-     works only at the "top level": e.g. if we have an `Array[String|Null]|Null` and we call `stripNull`
-     we'll get `Array[String|Null]` (only the outermost nullable union was removed).
-  - `stripAllJavaNull` is like `stripNull` but removes _all_ nullable unions in the type (and only works
-     for `JavaNull`). This is needed when we want to "revert" the Java nullification function.
+
+- `normNullableUnion` normalizes unions so that the `Null` type (or aliases to `Null`)
+  appears to the right of all other types.
+
+- `isNullableUnion` determines whether `this` is a nullable union.
+- `isJavaNullableUnion` determines whether `this` is syntactically a union of the form
+  `T|JavaNull`
+- `stripNull` syntactically strips all `Null` types in the union:
+  e.g. `String|Null => String`.
+- `stripAllJavaNull` is like `stripNull` but only removes `JavaNull` from the union.
+  This is needed when we want to "revert" the Java nullification function.
 
 ## Flow Typing
 
-TODO
+`NotNullInfo`s are collected as we typing each statements, see `Nullables.scala` for more
+details about how we compute `NotNullInfo`s.
+
+When we type an identity or a select tree (in `typedIdent` and `typedSelect`), we will
+call `toNotNullTermRef` on the tree before reture the result. If the tree `x` has nullable
+type `T|Null` and it is known to be not null according to the `NotNullInfo` and it is not
+on the lhs of assignment, then we cast it to `x.type & T` using `defn.Any_typeCast`. The
+reason to have a `TermRef(x)` in the `AndType` is that we can track the new result as well and
+use it as a path.
diff --git a/docs/docs/reference/other-new-features/explicit-nulls.md b/docs/docs/reference/other-new-features/explicit-nulls.md
@@ -192,7 +192,6 @@ Specifically, we patch
       final char CHAR = 'a';
 
       final String NAME_GENERATED = getNewName();
-      final int VALUE = 0 * 2;
     }
     ```
     ==>
@@ -203,7 +202,6 @@ Specifically, we patch
       val CHAR: Char('a') = 'a'
 
       val NAME_GENERATED: String | Null = ???
-      val VALUE: Int = ???
     }
     ```
 
@@ -289,12 +287,160 @@ val s2 = if (ret != null) {
 
 ## Flow Typing
 
-TODO
+We added a simple form of flow-sensitive type inference. The idea is that if `p` is a
+stable path or a trackable variable, then we can know that `p` is non-null if it's compared
+with the `null`. This information can then be propagated to the `then` and `else` branches
+of an if-statement (among other places).
+
+Example:
+
+```scala
+val s: String|Null = ???
+if (s != null) {
+  // s: String
+}
+// s: String|Null
+
+assert(x != null)
+// s: String
+```
+
+A similar inference can be made for the `else` case if the test is `p == null`
+
+```scala
+if (s == null) {
+  // s: String|Null
+} else {
+  // s: String
+}
+```
+
+`==` and `!=` is considered a comparison for the purposes of the flow inference.
+
+### Logical Operators
+
+We also support logical operators (`&&`, `||`, and `!`):
+
+```scala
+val s: String|Null = ???
+val s2: String|Null = ???
+if (s != null && s2 != null) {
+  // s: String
+  // s2: String
+}
+
+if (s == null || s2 == null) {
+  // s: String|Null
+  // s2: String|Null
+} else {
+  // s: String
+  // s2: String
+}
+```
+
+### Inside Conditions
+
+We also support type specialization _within_ the condition, taking into account that `&&` and `||` are short-circuiting:
+
+```scala
+val s: String|Null = ???
+
+if (s != null && s.length > 0) { // s: String in `s.length > 0`
+  // s: String
+}
+
+if (s == null || s.length > 0) // s: String in `s.length > 0` {
+  // s: String|Null
+} else {
+  // s: String|Null
+}
+```
+
+### Match Case
+
+The non-null cases can be detected in match statements.
+
+```scala
+val s: String|Null = ???
+
+s match {
+  case _: String => // s: String
+  case _ =>
+}
+```
+
+### Mutable Variable
+
+A mutable vriable is trackable with following restrictions:
+
+1. All the assignment must in the same closure as the definition (more strictly,
+  reachable by the definition).
+2. We only analyze the comparisons and use the facts in the same closure as
+  the definition.
+
+```scala
+class C(val x: Int, val next: C|Null)
+
+var xs: C|Null = C(1, C(2, null))
+// xs is trackable, since all assignments are in the same mathod
+while (xs != null) {
+  // xs: C
+  val xsx: Int = xs.x
+  val xscpy: C = xs
+  xs = xscpy // since xscpy is non-null, xs still has type C after this line
+  // xs: C
+  xs = xs.next // after this assignment, xs can be null again
+  // xs: C | Null
+}
+```
+
+```scala
+var x: String|Null = ???
+def y = {
+  x = null
+}
+if (x != null) {
+  // y can be called here
+  val a: String = x // error: x is captured and mutated by the closure, not tackable
+}
+```
+
+```scala
+var x: String|Null = ???
+def y = {
+  if (x != null) {
+    // not safe to use the fact (x != null) here
+    // since y can be executed at the same time as the outer block
+    val _: String = x
+  }
+}
+if (x != null) {
+  val a: String = x // ok to use the fact here
+  x = null
+}
+```
+
+Currently, we are unable to track `x.a` if `x` is mutable.
+
+### Unsupported Idioms
+
+We don't support:
+
+- flow facts not related to nullability (`if (x == 0) { // x: 0.type not inferred }`)
+- tracking aliasing between non-nullable paths
+  ```scala
+  val s: String|Null = ???
+  val s2: String|Null = ???
+  if (s != null && s == s2) {
+    // s:  String inferred
+    // s2: String not inferred
+  }
+  ```
 
 ## Binary Compatibility
 
 Our strategy for binary compatibility with Scala binaries that predate explicit nulls
 and new libraries compiled without `-Yexplicit-nulls` is to leave the types unchanged
 and be compatible but unsound.
 
-[More details](../../internals/intersection-types-spec.md)
+[More details](../../internals/explicit-nulls.md)
