Skip to content

Instantly share code, notes, and snippets.

@abeln

abeln/scala-explicit-nulls.md

Last active December 18, 2020 13:57
Show Gist options
  • Save abeln/9f79774bac111d99b3ae2cb9016a33e6 to your computer and use it in GitHub Desktop.
Save abeln/9f79774bac111d99b3ae2cb9016a33e6 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. abeln revised this gist Jan 24, 2019. 1 changed file with 3 additions and 1 deletion.
    4 changes: 3 additions & 1 deletion scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -14,7 +14,9 @@
    - [toString](#toString)
    - [Binary Compatibility](#binary-compatibility)
    - [Flow-Sensitive Type Inference](#flow-sensitive-type-inference)
    - [Examples](#examples)
    - [Non-Stable Paths](#non-stable-paths)
    - [Logical Operators](#logical-operators)
    - [Inside Conditions](#inside-conditions)
    - [Algorithm](#algorithm)
    - [Unsupported Idioms](#unsupported-idioms)
    - [Local Type Inference](#local-type-inference)
  2. abeln revised this gist Jan 24, 2019. 1 changed file with 20 additions and 28 deletions.
    48 changes: 20 additions & 28 deletions scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -396,39 +396,38 @@ o.foo(null.asInstanceOf[String]) // ok: cast will succeed at runtime
    ## Flow-Sensitive Type Inference

    We added a simple form of flow-sensitive type inference. The idea is that if `p` is a stable path, then we can know
    that `p` is non-null in the `then` branch of
    ```scala
    if (p != null) {
    // p is non-null here
    }
    // p might be null here
    ```
    A similar inference can be made for the `else` case if the test is `p == null`.
    that `p` is non-null if it's "compared" with the `null` literal. This information can then be propagated to the `then` and `else` branches of an if-statement (among other places).

    ### Examples
    Example:
    ```scala
    val s: String|Null = ???
    if (s != null) {
    // s: String
    }
    // s: String|Null

    ```
    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
    }

    class C {
    val s: String|Null = ???
    }

    val c: C = ???
    if (c.s != null) { // c.s is stable
    // c.s: String
    }
    ```

    What exactly is considered a comparison for the purposes of the flow inference:
    - `==` and `!=`
    - `eq` and `ne`
    - `isInstanceOf[Null]`. Only kicks in if the type test is against `Null`:
    ```scala
    val s: String|Null
    if (!s.isInstanceOf[Null]) {
    // s: String
    }
    ```
    If the test had been (`if (s.isInstanceOf[String])`), we currently don't infer non-nullness.

    ### Non-Stable Paths
    If `p` isn't stable, then inferring non-nullness is potentially unsound:
    ```scala
    var s: String|Null = "hello"
    @@ -437,6 +436,7 @@ if (s != null && {s = null; true}) {
    }
    ```

    ### Logical Operators
    We also support logical operators (`&&`, `||`, and `!`):
    ```scala
    val s: String|Null = ???
    @@ -455,6 +455,7 @@ if (s == null || s2 == null) {
    }
    ```

    ### Inside Conditions
    We also support type specialization _within_ the condition, taking into account that `&&` and `||` are short-circuiting:
    ```scala
    val s: String|Null
    @@ -469,15 +470,6 @@ if (s == null || s.length > 0) // s: String in `s.length > 0` {
    }
    ```

    Finally, we also support `eq`, `ne` and `isInstanceOf` as operators.
    `isInstanceOf` only kicks in if the type test is against `Null`:
    ```scala
    val s: String|Null
    if (!s.isInstanceOf[Null]) {
    // s: String
    }
    ```

    ### Algorithm

    Let `NN(cond, true/false)` be the set of paths (`TermRefs` in the compiler) that we can infer to be non-null if `cond` is `true/false`, respectively.
  3. abeln revised this gist Jan 22, 2019. 1 changed file with 10 additions and 1 deletion.
    11 changes: 10 additions & 1 deletion scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -455,7 +455,7 @@ if (s == null || s2 == null) {
    }
    ```

    Finally, we also support type specialization _within_ the condition, taking into account that `&&` and `||` are short-circuiting:
    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`
    @@ -469,6 +469,15 @@ if (s == null || s.length > 0) // s: String in `s.length > 0` {
    }
    ```

    Finally, we also support `eq`, `ne` and `isInstanceOf` as operators.
    `isInstanceOf` only kicks in if the type test is against `Null`:
    ```scala
    val s: String|Null
    if (!s.isInstanceOf[Null]) {
    // s: String
    }
    ```

    ### Algorithm

    Let `NN(cond, true/false)` be the set of paths (`TermRefs` in the compiler) that we can infer to be non-null if `cond` is `true/false`, respectively.
  4. abeln revised this gist Jan 22, 2019. 1 changed file with 6 additions and 7 deletions.
    13 changes: 6 additions & 7 deletions scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -161,9 +161,8 @@ We do the patching with a "nullification" function `nf` on types:
    4. nf(C[R]) = C[R]|JavaNull if C is Java-defined
    5. nf(C[R]) = C[nf(R)]|JavaNull if C isn't Java-defined
    6. nf(A => B) = nf(A) => nf(B)
    7. nf(A | B) = nf(A) | nf(B)
    8. nf(A & B) = nf(A) & nf(B)
    9. nf(T) = T otherwise (T is any other type)
    7. nf(A & B) = nf(A) & nf(B)
    8. nf(T) = T otherwise (T is any other type)
    ```
    `JavaNull` is an alias for `Null` with magic properties (see below). We illustrate the rules for `nf` below with examples.
    @@ -225,10 +224,10 @@ We do the patching with a "nullification" function `nf` on types:
    `Box[T|JavaNull]|JavaNull`. This is needed because our nullability function is only applied (modularly) to the Java
    classes, but not to the Scala ones, so we need a way to tell `Box` that it contains a nullable value.
    * Rules 6, 7, and 8 just recurse structurally on the components of the type.
    The implementation of rules 7 and 8 in the compiler are a bit more involved than the presentation above.
    Specifically, they make sure to add `| Null` only at the top level of a type:
    e.g. `nf(A | B) = A | B | JavaNull`, as opposed to `(A | JavaNull) | (B | JavaNull)`.
    * Rules 6 and 7 just recurse structurally on the components of the type.
    The implementation of rule 7 n the compiler are a bit more involved than the presentation above.
    Specifically, the implementation makes sure to add `| Null` only at the top level of a type:
    e.g. `nf(A & B) = (A & B) | JavaNull`, as opposed to `(A | JavaNull) & (B | JavaNull)`.
    ### JavaNull
    To enable method chaining on Java-returned values, we have a special `JavaNull` alias
  5. abeln revised this gist Jan 21, 2019. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -513,7 +513,7 @@ We don't support
    ```scala
    val s: String|Null = ???
    val s2: String|Null = ???
    if (s != null && s2 == s2) {
    if (s != null && s == s2) {
    // s: String inferred
    // s2: String not inferred
    }
  6. abeln revised this gist Jan 18, 2019. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -21,7 +21,7 @@

    ## What is This?

    This proposal and the accompanying pull request describe a modification to the Scala type system
    This proposal and the accompanying [pull request](https://github.com/lampepfl/dotty/pull/5747) describe a modification to the Scala type system
    that makes reference types (anything that extends `AnyRef`) _non-nullable_.

    This means the following code will no longer typecheck
  7. abeln revised this gist Jan 18, 2019. 1 changed file with 12 additions and 31 deletions.
    43 changes: 12 additions & 31 deletions scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -44,31 +44,12 @@ we're _before_ or _after_ erasure.
    Before erasure, `Null` is no longer a subtype of all reference types.
    Additionally, `Null` is a subtype of `Any` directly, as opposed to `AnyRef`.

    ![type hierarchy before erasure](https://user-images.githubusercontent.com/1782179/51209862-43749c00-18df-11e9-9466-2f252dce15ad.png)
    ![type hierarchy before erasure](https://user-images.githubusercontent.com/1782179/51210362-9bf86900-18e0-11e9-9485-f40dc9061527.png)

    ```
    +--- Null -----------------------------------+
    | +
    Any ---+--- AnyRef ---+--- String ------------------+
    | +--- List[Int] ---------------+
    | +--- ... (reference types) ---+--- Nothing
    | +
    +--- AnyVal ---+--- Bool --------------------+
    +--- Int ---------------------+
    +--- ... (value types) -------+
    ```
    After erasure, `Null` remains a subtype of all reference types (as forced
    by the JVM).
    ```
    Any ---+--- AnyRef -- +--- String ------------------+
    | +--- List --------------------+
    | +--- ... (reference types) ---+--- Null ---+
    | +--- Nothing
    | +
    +--- AnyVal ---+--- Bool --------------------+ +
    +--- Int ---------------------+------------+
    +--- ... (value types) -------+
    ```

    ![type hierarchy after erasure](https://user-images.githubusercontent.com/1782179/51210554-175a1a80-18e1-11e9-91a1-ca2188108e30.png)

    ## Unsoundness

    @@ -509,20 +490,20 @@ NN(cond, _) = {} otherwise
    ```

    To type `If(cond, then, else)`
    - compute `NN(cond, true)` and `NN(cond, false)`
    - type the `then` branch with the knowledge that the paths in `NN(cond, true)`
    1. compute `NN(cond, true)` and `NN(cond, false)`
    2. type the `then` branch with the knowledge that the paths in `NN(cond, true)`
    are non-nullable
    - ditto for the `else` branch and the paths in `NN(cond, false)`
    3. ditto for the `else` branch and the paths in `NN(cond, false)`

    To propagate nullability facts _within_ a condition, when typing `A && B`
    - type `A`
    - compute `NN(A, true)`
    - type `B` augmented context with the facts in `NN(A, true)`
    1. type `A`
    2. compute `NN(A, true)`
    3. type `B` augmented context with the facts in `NN(A, true)`

    Similarly, when typing `A || B`
    - type `A`
    - compute `NN(A, false)`
    - type `B` in an augmented context with the facts in `NN(A, false)`
    1. type `A`
    2. compute `NN(A, false)`
    3. type `B` in an augmented context with the facts in `NN(A, false)`

    ### Unsupported Idioms
    We don't support
  8. abeln revised this gist Jan 18, 2019. 1 changed file with 34 additions and 13 deletions.
    47 changes: 34 additions & 13 deletions scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -44,13 +44,31 @@ we're _before_ or _after_ erasure.
    Before erasure, `Null` is no longer a subtype of all reference types.
    Additionally, `Null` is a subtype of `Any` directly, as opposed to `AnyRef`.

    ![type hierarchy before erasure](https://user-images.githubusercontent.com/1782179/51210362-9bf86900-18e0-11e9-9485-f40dc9061527.png)
    ![type hierarchy before erasure](https://user-images.githubusercontent.com/1782179/51209862-43749c00-18df-11e9-9466-2f252dce15ad.png)

    ```
    +--- Null -----------------------------------+
    | +
    Any ---+--- AnyRef ---+--- String ------------------+
    | +--- List[Int] ---------------+
    | +--- ... (reference types) ---+--- Nothing
    | +
    +--- AnyVal ---+--- Bool --------------------+
    +--- Int ---------------------+
    +--- ... (value types) -------+
    ```
    After erasure, `Null` remains a subtype of all reference types (as forced
    by the JVM).

    ![type hierarchy after erasure](https://user-images.githubusercontent.com/1782179/51210554-175a1a80-18e1-11e9-91a1-ca2188108e30.png)

    ```
    Any ---+--- AnyRef -- +--- String ------------------+
    | +--- List --------------------+
    | +--- ... (reference types) ---+--- Null ---+
    | +--- Nothing
    | +
    +--- AnyVal ---+--- Bool --------------------+ +
    +--- Int ---------------------+------------+
    +--- ... (value types) -------+
    ```

    ## Unsoundness

    @@ -286,6 +304,9 @@ val s2 = if (ret != null) {
    def foo(s: String|Null) = ???
    foo(s) // allowed, but within `foo` we have to work with the strict `Null`
    ```
    - When looking for an implicit conversion from `A|JavaNull` to `B`, if we
    can't find it, then also look for an implicit conversion from `A` to `B`.
    This is done for ease of interop with Java.
    ### Improving Precision
    @@ -488,20 +509,20 @@ NN(cond, _) = {} otherwise
    ```

    To type `If(cond, then, else)`
    1. compute `NN(cond, true)` and `NN(cond, false)`
    2. type the `then` branch with the knowledge that the paths in `NN(cond, true)`
    - compute `NN(cond, true)` and `NN(cond, false)`
    - type the `then` branch with the knowledge that the paths in `NN(cond, true)`
    are non-nullable
    3. ditto for the `else` branch and the paths in `NN(cond, false)`
    - ditto for the `else` branch and the paths in `NN(cond, false)`

    To propagate nullability facts _within_ a condition, when typing `A && B`
    1. type `A`
    2. compute `NN(A, true)`
    3. type `B` augmented context with the facts in `NN(A, true)`
    - type `A`
    - compute `NN(A, true)`
    - type `B` augmented context with the facts in `NN(A, true)`

    Similarly, when typing `A || B`
    1. type `A`
    2. compute `NN(A, false)`
    3. type `B` in an augmented context with the facts in `NN(A, false)`
    - type `A`
    - compute `NN(A, false)`
    - type `B` in an augmented context with the facts in `NN(A, false)`

    ### Unsupported Idioms
    We don't support
  9. abeln revised this gist Jan 15, 2019. 1 changed file with 9 additions and 9 deletions.
    18 changes: 9 additions & 9 deletions scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -488,20 +488,20 @@ NN(cond, _) = {} otherwise
    ```

    To type `If(cond, then, else)`
    - compute `NN(cond, true)` and `NN(cond, false)`
    - type the `then` branch with the knowledge that the paths in `NN(cond, true)`
    1. compute `NN(cond, true)` and `NN(cond, false)`
    2. type the `then` branch with the knowledge that the paths in `NN(cond, true)`
    are non-nullable
    - ditto for the `else` branch and the paths in `NN(cond, false)`
    3. ditto for the `else` branch and the paths in `NN(cond, false)`

    To propagate nullability facts _within_ a condition, when typing `A && B`
    - type `A`
    - compute `NN(A, true)`
    - type `B` augmented context with the facts in `NN(A, true)`
    1. type `A`
    2. compute `NN(A, true)`
    3. type `B` augmented context with the facts in `NN(A, true)`

    Similarly, when typing `A || B`
    - type `A`
    - compute `NN(A, false)`
    - type `B` in an augmented context with the facts in `NN(A, false)`
    1. type `A`
    2. compute `NN(A, false)`
    3. type `B` in an augmented context with the facts in `NN(A, false)`

    ### Unsupported Idioms
    We don't support
  10. abeln revised this gist Jan 15, 2019. 1 changed file with 2 additions and 1 deletion.
    3 changes: 2 additions & 1 deletion scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -49,7 +49,8 @@ Additionally, `Null` is a subtype of `Any` directly, as opposed to `AnyRef`.
    After erasure, `Null` remains a subtype of all reference types (as forced
    by the JVM).

    ![type hierarchy after erasure](https://user-images.githubusercontent.com/1782179/51210019-a6663300-18df-11e9-8613-cb89b1c08bfc.png)
    ![type hierarchy after erasure](https://user-images.githubusercontent.com/1782179/51210554-175a1a80-18e1-11e9-91a1-ca2188108e30.png)


    ## Unsoundness

  11. abeln revised this gist Jan 15, 2019. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -44,7 +44,7 @@ we're _before_ or _after_ erasure.
    Before erasure, `Null` is no longer a subtype of all reference types.
    Additionally, `Null` is a subtype of `Any` directly, as opposed to `AnyRef`.

    ![type hierarchy before erasure](https://user-images.githubusercontent.com/1782179/51209862-43749c00-18df-11e9-9466-2f252dce15ad.png)
    ![type hierarchy before erasure](https://user-images.githubusercontent.com/1782179/51210362-9bf86900-18e0-11e9-9485-f40dc9061527.png)

    After erasure, `Null` remains a subtype of all reference types (as forced
    by the JVM).
  12. abeln revised this gist Jan 15, 2019. 1 changed file with 2 additions and 21 deletions.
    23 changes: 2 additions & 21 deletions scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -46,29 +46,10 @@ Additionally, `Null` is a subtype of `Any` directly, as opposed to `AnyRef`.

    ![type hierarchy before erasure](https://user-images.githubusercontent.com/1782179/51209862-43749c00-18df-11e9-9466-2f252dce15ad.png)

    ```
    +--- Null -----------------------------------+
    | +
    Any ---+--- AnyRef ---+--- String ------------------+
    | +--- List[Int] ---------------+
    | +--- ... (reference types) ---+--- Nothing
    | +
    +--- AnyVal ---+--- Bool --------------------+
    +--- Int ---------------------+
    +--- ... (value types) -------+
    ```
    After erasure, `Null` remains a subtype of all reference types (as forced
    by the JVM).
    ```
    Any ---+--- AnyRef -- +--- String ------------------+
    | +--- List --------------------+
    | +--- ... (reference types) ---+--- Null ---+
    | +--- Nothing
    | +
    +--- AnyVal ---+--- Bool --------------------+ +
    +--- Int ---------------------+------------+
    +--- ... (value types) -------+
    ```

    ![type hierarchy after erasure](https://user-images.githubusercontent.com/1782179/51210019-a6663300-18df-11e9-8613-cb89b1c08bfc.png)

    ## Unsoundness

  13. abeln revised this gist Jan 15, 2019. No changes.
  14. abeln revised this gist Jan 15, 2019. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -44,7 +44,7 @@ we're _before_ or _after_ erasure.
    Before erasure, `Null` is no longer a subtype of all reference types.
    Additionally, `Null` is a subtype of `Any` directly, as opposed to `AnyRef`.

    ![type hierarchy before erasure](https://imgur.com/a/MRzHjRs)
    ![type hierarchy before erasure](https://user-images.githubusercontent.com/1782179/51209862-43749c00-18df-11e9-9466-2f252dce15ad.png)

    ```
    +--- Null -----------------------------------+
  15. abeln revised this gist Jan 15, 2019. 1 changed file with 2 additions and 0 deletions.
    2 changes: 2 additions & 0 deletions scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -44,6 +44,8 @@ we're _before_ or _after_ erasure.
    Before erasure, `Null` is no longer a subtype of all reference types.
    Additionally, `Null` is a subtype of `Any` directly, as opposed to `AnyRef`.

    ![type hierarchy before erasure](https://imgur.com/a/MRzHjRs)

    ```
    +--- Null -----------------------------------+
    | +
  16. abeln revised this gist Jan 15, 2019. 1 changed file with 3 additions and 1 deletion.
    4 changes: 3 additions & 1 deletion scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -11,7 +11,7 @@
    - [Nullification Function](#nullification-function)
    - [JavaNull](#javanull)
    - [Improving Precision](#improving-precision)
    - [toString](#tostring)
    - [toString](#toString)
    - [Binary Compatibility](#binary-compatibility)
    - [Flow-Sensitive Type Inference](#flow-sensitive-type-inference)
    - [Examples](#examples)
    @@ -583,6 +583,8 @@ Explicit nullability interacts with local type inference in a few ways:

    ### Kotlin

    TODO

    ## TODOs
    - Bootstrap Dotty with the new type system
    - Port the standard library to the new type system
  17. abeln revised this gist Jan 15, 2019. 1 changed file with 2 additions and 2 deletions.
    4 changes: 2 additions & 2 deletions scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -11,7 +11,7 @@
    - [Nullification Function](#nullification-function)
    - [JavaNull](#javanull)
    - [Improving Precision](#improving-precision)
    - [toString](#toString)
    - [toString](#tostring)
    - [Binary Compatibility](#binary-compatibility)
    - [Flow-Sensitive Type Inference](#flow-sensitive-type-inference)
    - [Examples](#examples)
    @@ -305,7 +305,7 @@ val s2 = if (ret != null) {
    ### Improving Precision
    Our nullification function is sometimes too conservative. For example, consider the `toString`
    Our nullification function is sometimes too conservative. For example, consider the `trim`
    method in `java.lang.String`:
    ```java
    /** Returns a copy of the string, with leading and trailing whitespace omitted. */
  18. abeln revised this gist Jan 15, 2019. 1 changed file with 40 additions and 0 deletions.
    40 changes: 40 additions & 0 deletions scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -6,6 +6,7 @@
    - [New Type Hierarchy](#new-type-hierarchy)
    - [Unsoundness](#unsoundness)
    - [Equality](#equality)
    - [Working with Null](#working-with-null)
    - [Java Interop](#java-interop)
    - [Nullification Function](#nullification-function)
    - [JavaNull](#javanull)
    @@ -120,6 +121,45 @@ class AnyRef extends Any with RefEq
    class Null extends Any with RefEq
    ```

    ## Working with Null

    To make working with nullable values easier, we propose adding a few utilities to the standard library.
    So far, we have found the following useful:
    - An extension method `.nn` to "cast away" nullability
    ```scala
    implicit class NonNull[T](x: T|Null) extends AnyVal {
    def nn: T = if (x == null) {
    throw new NullPointerException("tried to cast away nullability, but value is null")
    } else {
    x.asInstanceOf[T]
    }
    }
    ```
    This means that given `x: String|Null`, `x.nn` has type `String`, so we can call all the usual methods
    on it. Of course, `x.nn` will throw a NPE if `x` is `null`.
    - Implicit conversions from/to nullable arrays
    ```scala
    implicit def fromNullable1[T](a: Array[T|Null]): Array[T] = a.asInstanceOf[Array[T]]
    implicit def toNullable1[T](a: Array[T]): Array[T|Null] = a.asInstanceOf[Array[T|Null]]
    // similar methods for matrices and higher dimensions: e.g. `toNullable{2, 3, ...}`
    ```
    These are useful because Java APIs often return nullable arrays. Additionally, because `Array` is
    invariant neither `Array[T] <: Array[T|Null]` nor the other way, so to go from one to the other we need
    casts. For example, suppose we want to write a function that sorts arrays
    ```scala
    def sort[T <: AnyRef : Ordering](a: Array[T]): Array[T] = {
    // error: `copyOf` expects an `Array[T|Null]` and returns an `Array[T|Null]`
    val a2: Array[T] = java.util.Arrays.copyOf(a, a.length).nn
    scala.util.Sorting.quickSort(a2)
    a2
    }
    ```
    To fix the error we use the implicit conversions above, which turn the third line into
    ```scala
    val a2: Array[T] = fromNullable1(java.util.Arrays.copyOf(toNullable1(a), a.length)).nn
    ```
    Of course, this is also unsound and `a2` could end up with a `null` value in it.

    ## Java Interop

    The compiler can load Java classes in two ways: from source or from bytecode. In either case, when a Java class is loaded, we "patch" the type of its members to reflect that Java types remain implicitly nullable.
  19. abeln revised this gist Jan 15, 2019. 1 changed file with 2 additions and 2 deletions.
    4 changes: 2 additions & 2 deletions scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -2,7 +2,7 @@
    # Scala with Explicit Nulls

    ## Contents
    - [What is this?](#what-is-this?)
    - [What is This?](#what-is-this)
    - [New Type Hierarchy](#new-type-hierarchy)
    - [Unsoundness](#unsoundness)
    - [Equality](#equality)
    @@ -18,7 +18,7 @@
    - [Unsupported Idioms](#unsupported-idioms)
    - [Local Type Inference](#local-type-inference)

    ## What is this?
    ## What is This?

    This proposal and the accompanying pull request describe a modification to the Scala type system
    that makes reference types (anything that extends `AnyRef`) _non-nullable_.
  20. abeln revised this gist Jan 15, 2019. 1 changed file with 18 additions and 0 deletions.
    18 changes: 18 additions & 0 deletions scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -2,6 +2,7 @@
    # Scala with Explicit Nulls

    ## Contents
    - [What is this?](#what-is-this?)
    - [New Type Hierarchy](#new-type-hierarchy)
    - [Unsoundness](#unsoundness)
    - [Equality](#equality)
    @@ -17,6 +18,23 @@
    - [Unsupported Idioms](#unsupported-idioms)
    - [Local Type Inference](#local-type-inference)

    ## What is this?

    This proposal and the accompanying pull request describe a modification to the Scala type system
    that makes reference types (anything that extends `AnyRef`) _non-nullable_.

    This means the following code will no longer typecheck
    ```scala
    val x: String = null // error: found `Null`, but required `String`
    ```

    Instead, to mark a type as nullable we use a [type union](https://dotty.epfl.ch/docs/reference/new-types/union-types.html)
    ```
    val x: String|Null = null // ok
    ```

    Read on for details.

    ## New Type Hierarchy

    There are two type hierarchies with respect to `Null`, depending on whether
  21. abeln revised this gist Jan 15, 2019. 1 changed file with 13 additions and 1 deletion.
    14 changes: 13 additions & 1 deletion scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -9,6 +9,7 @@
    - [Nullification Function](#nullification-function)
    - [JavaNull](#javanull)
    - [Improving Precision](#improving-precision)
    - [toString](#toString)
    - [Binary Compatibility](#binary-compatibility)
    - [Flow-Sensitive Type Inference](#flow-sensitive-type-inference)
    - [Examples](#examples)
    @@ -67,6 +68,7 @@ Enforcing sound initialization is a non-goal of this proposal. However, once we
    we can use a sound initialization scheme like the one proposed by @liufengyun and @biboudis in [https://github.com/lampepfl/dotty/pull/4543](https://github.com/lampepfl/dotty/pull/4543)
    to eliminate this particular source of unsoundness.


    ## Equality

    Because of the unsoundness, we need to allow comparisons of the form `x == null` or `x != null` even when `x` has a non-nullable reference
    @@ -266,7 +268,17 @@ Currently, the whitelist is hard-coded in Dotty, but the plan is to use an annot
    of the Java JDK with nullability annotations produced by the [Checker Framework](https://checkerframework.org/)
    (hat tip to @liufengyun and Werner Dietl for suggesting this).


    ### toString

    The `toString` method is a special case where we chose to trade away soundness for precision and usability.
    `toString` is special because even though it lives in `scala.Any`, it actually comes from
    `java.lang.Object` and it could, in principle, be overriden to return `null`.

    However, changing `toString`'s signature to return `String|JavaNull` would break too much
    existing Scala code. Additionally, our assumption is that `toString` is unlikely to return null.

    This means the signature of `toString` remains `def toString(): String`.

    ## Binary Compatibility

    Our strategy for binary compatibility with Scala binaries that predate explicit nulls
  22. abeln revised this gist Jan 15, 2019. 1 changed file with 20 additions and 0 deletions.
    20 changes: 20 additions & 0 deletions scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -245,6 +245,26 @@ val s2 = if (ret != null) {
    ### Improving Precision
    Our nullification function is sometimes too conservative. For example, consider the `toString`
    method in `java.lang.String`:
    ```java
    /** Returns a copy of the string, with leading and trailing whitespace omitted. */
    public String trim()
    ```

    A vanilla application of nullification will turn the above into `def trim(): String|JavaNull`.
    However, inspecting the function contract in the javadoc reveals that if `s` is a non-null string
    to begin with, then `s.trim()` should in fact never return `null` (if `s` is null, then `s.trim()` should throw).
    From the point of view of Scala it is then preferable to have a more precise signature
    for `trim` where the return type is `String`.

    In general, this is a problem for _many_ methods in the Java standard library: in particular, methods
    in commonly-used classes like `String` and `Class`. We address this by maintaining a _whitelist_ of
    methods that need "special" treatment during nullification (e.g. nullify only the arguments, or only the return type).

    Currently, the whitelist is hard-coded in Dotty, but the plan is to use an annotated [version](https://github.com/typetools/checker-framework/tree/master/checker/jdk/nullness)
    of the Java JDK with nullability annotations produced by the [Checker Framework](https://checkerframework.org/)
    (hat tip to @liufengyun and Werner Dietl for suggesting this).


    ## Binary Compatibility
  23. abeln revised this gist Jan 15, 2019. 1 changed file with 14 additions and 5 deletions.
    19 changes: 14 additions & 5 deletions scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -112,11 +112,15 @@ Specifically, we patch

    We do the patching with a "nullification" function `nf` on types:
    ```
    1. nf(R) = R|JavaNull if R is a reference type (a subtype of AnyRef)
    2. nf(R) = R if R is a value type (a subtype of AnyVal)
    3. nf(T) = T|JavaNull if T is a type parameter
    4. nf(C[R]) = C[R]|JavaNull if C is Java-defined
    5. nf(C[R]) = C[nf(R)]|JavaNull if C isn't Java-defined
    1. nf(R) = R|JavaNull if R is a reference type (a subtype of AnyRef)
    2. nf(R) = R if R is a value type (a subtype of AnyVal)
    3. nf(T) = T|JavaNull if T is a type parameter
    4. nf(C[R]) = C[R]|JavaNull if C is Java-defined
    5. nf(C[R]) = C[nf(R)]|JavaNull if C isn't Java-defined
    6. nf(A => B) = nf(A) => nf(B)
    7. nf(A | B) = nf(A) | nf(B)
    8. nf(A & B) = nf(A) & nf(B)
    9. nf(T) = T otherwise (T is any other type)
    ```

    `JavaNull` is an alias for `Null` with magic properties (see below). We illustrate the rules for `nf` below with examples.
    @@ -178,6 +182,11 @@ We do the patching with a "nullification" function `nf` on types:
    `Box[T|JavaNull]|JavaNull`. This is needed because our nullability function is only applied (modularly) to the Java
    classes, but not to the Scala ones, so we need a way to tell `Box` that it contains a nullable value.

    * Rules 6, 7, and 8 just recurse structurally on the components of the type.
    The implementation of rules 7 and 8 in the compiler are a bit more involved than the presentation above.
    Specifically, they make sure to add `| Null` only at the top level of a type:
    e.g. `nf(A | B) = A | B | JavaNull`, as opposed to `(A | JavaNull) | (B | JavaNull)`.

    ### JavaNull
    To enable method chaining on Java-returned values, we have a special `JavaNull` alias
    ```scala
  24. abeln revised this gist Jan 15, 2019. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -454,7 +454,7 @@ Explicit nullability interacts with local type inference in a few ways:
    def foo2(): String|Null = "hello"
    val x = foo2() // x: String|Null inferred
    ```
    Otherwise, the nullable type `String|Null` would be collapsed to `AnyRef`, which loses too much information.
    Otherwise, the nullable type `String|Null` would be collapsed to `Any`, which loses too much information.

    - Nullable unions in prototypes: the compiler currently doesn't allow unions in prototypes
    ```scala
  25. abeln revised this gist Jan 15, 2019. 1 changed file with 1 addition and 1 deletion.
    2 changes: 1 addition & 1 deletion scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -471,7 +471,7 @@ Explicit nullability interacts with local type inference in a few ways:
    The problem is that the compiler sees a prototype of `Array[String|Int]|Int`, and because
    the outer type is a union it discards the prototype and switches to synthesis.

    See [here](https://github.com/lampepfl/dotty/commit/8067b952875426d640968be865773f6ef3783f3c) for
    See [https://github.com/lampepfl/dotty/commit/8067b952875426d640968be865773f6ef3783f3c](https://github.com/lampepfl/dotty/commit/8067b952875426d640968be865773f6ef3783f3c) for
    why this was done.

    We've changed this behaviour so that nullable unions can be used in prototypes
  26. abeln revised this gist Jan 14, 2019. 1 changed file with 4 additions and 0 deletions.
    4 changes: 4 additions & 0 deletions scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -234,6 +234,10 @@ val s2 = if (ret != null) {
    foo(s) // allowed, but within `foo` we have to work with the strict `Null`
    ```
    ### Improving Precision
    ## Binary Compatibility
    Our strategy for binary compatibility with Scala binaries that predate explicit nulls
  27. abeln revised this gist Jan 14, 2019. 1 changed file with 0 additions and 3 deletions.
    3 changes: 0 additions & 3 deletions scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -8,7 +8,6 @@
    - [Java Interop](#java-interop)
    - [Nullification Function](#nullification-function)
    - [JavaNull](#javanull)
    - [Override Checks](#override-checks)
    - [Improving Precision](#improving-precision)
    - [Binary Compatibility](#binary-compatibility)
    - [Flow-Sensitive Type Inference](#flow-sensitive-type-inference)
    @@ -235,8 +234,6 @@ val s2 = if (ret != null) {
    foo(s) // allowed, but within `foo` we have to work with the strict `Null`
    ```
    ### Override Checks
    ## Binary Compatibility
    Our strategy for binary compatibility with Scala binaries that predate explicit nulls
  28. abeln revised this gist Jan 14, 2019. 1 changed file with 50 additions and 1 deletion.
    51 changes: 50 additions & 1 deletion scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -3,6 +3,7 @@

    ## Contents
    - [New Type Hierarchy](#new-type-hierarchy)
    - [Unsoundness](#unsoundness)
    - [Equality](#equality)
    - [Java Interop](#java-interop)
    - [Nullification Function](#nullification-function)
    @@ -48,9 +49,57 @@ Any ---+--- AnyRef -- +--- String ------------------+
    +--- ... (value types) -------+
    ```

    ## Unsoundness

    The new type system is unsound with respect to `null`. This means there are still instances where an expressions has a
    non-nullable type like `String`, but its value is `null`.

    The unsoundness happens because uninitialized fields in a class start out as `null`:
    ```scala
    class C {
    val f: String = foo(f)
    def foo(f2: String): String = if (f2 == null) "field is null" else f2
    }
    val c = new C()
    // c.f == "field is null"
    ```

    Enforcing sound initialization is a non-goal of this proposal. However, once we have a type system where nullability is explicit,
    we can use a sound initialization scheme like the one proposed by @liufengyun and @biboudis in [https://github.com/lampepfl/dotty/pull/4543](https://github.com/lampepfl/dotty/pull/4543)
    to eliminate this particular source of unsoundness.

    ## Equality

    // TODO: talk about both "==" and "eq". Mention `RefEq`.
    Because of the unsoundness, we need to allow comparisons of the form `x == null` or `x != null` even when `x` has a non-nullable reference
    type (but not a value type). This is so we have an "escape hatch" for when we know `x` is nullable even when the type says
    it shouldn't be.
    ```scala
    val x: String|Null = null
    x == null // ok: x is a nullable string
    "hello" == null // ok: String is a reference type
    1 == null // error: Int is a value type
    ```

    ### Reference Equality

    Recall that `Null` is now a direct subtype of `Any`, as opposed to `AnyRef`. However, we also need to allow
    reference equality comparisons:
    ```scala
    val x: String = null
    x eq null // ok: could return `true` because of unsoundness
    ```

    We implement this by moving the `eq` and `ne` methods out of `AnyRef` and into a new trait `RefEq` that is extended
    by both `AnyRef` and `Null`:
    ```scala
    trait RefEq {
    def eq(that: RefEq): Boolean
    def ne(that: RefEq): Boolean
    }

    class AnyRef extends Any with RefEq
    class Null extends Any with RefEq
    ```

    ## Java Interop

  29. abeln revised this gist Jan 11, 2019. 1 changed file with 9 additions and 11 deletions.
    20 changes: 9 additions & 11 deletions scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -3,8 +3,7 @@

    ## Contents
    - [New Type Hierarchy](#new-type-hierarchy)
    - [Before Erasure](#before-erasure)
    - [After Erasure](#after-erasure)
    - [Equality](#equality)
    - [Java Interop](#java-interop)
    - [Nullification Function](#nullification-function)
    - [JavaNull](#javanull)
    @@ -16,31 +15,26 @@
    - [Algorithm](#algorithm)
    - [Unsupported Idioms](#unsupported-idioms)
    - [Local Type Inference](#local-type-inference)
    - [Equality](#equality)

    ## New Type Hierarchy

    There are two type hierarchies with respect to `Null`, depending on whether
    we're _before_ or _after_ erasure.

    ### Before Erasure
    Before erasure, `Null` is no longer a subtype of all reference types.
    Additionally, `Null` is a subtype of `Any` directly, as opposed to `AnyRef`.

    TODO: explain why `Null` is a subtype of `AnyRef`, as opposed to `Any`.
    ```
    Any ---+--- AnyRef ---+-------------------+--- Null +
    | +--- String|Null ---+ +
    | +--- ...|Null ---+
    | | +
    | +--- String ------------------+
    +--- Null -----------------------------------+
    | +
    Any ---+--- AnyRef ---+--- String ------------------+
    | +--- List[Int] ---------------+
    | +--- ... (reference types) ---+--- Nothing
    | +
    +--- AnyVal ---+--- Bool --------------------+
    +--- Int ---------------------+
    +--- ... (value types) -------+
    ```
    ### After Erasure
    After erasure, `Null` remains a subtype of all reference types (as forced
    by the JVM).
    ```
    @@ -54,6 +48,10 @@ Any ---+--- AnyRef -- +--- String ------------------+
    +--- ... (value types) -------+
    ```

    ## Equality

    // TODO: talk about both "==" and "eq". Mention `RefEq`.

    ## Java Interop

    The compiler can load Java classes in two ways: from source or from bytecode. In either case, when a Java class is loaded, we "patch" the type of its members to reflect that Java types remain implicitly nullable.
  30. abeln revised this gist Jan 10, 2019. 1 changed file with 44 additions and 3 deletions.
    47 changes: 44 additions & 3 deletions scala-explicit-nulls.md
    View file
    Original file line number Diff line number Diff line change
    @@ -387,9 +387,50 @@ We don't support
    ```

    ## Local Type Inference
    Explicit nullability interacts with local type inference in a couple of ways:
    - Nullable SAM types
    - Non-widening `T|Null`
    Explicit nullability interacts with local type inference in a few ways:
    - Suppor for SAM types: if `S` is a SAM type, then we consider `S|Null` as a SAM type as well. This allows
    ```scala
    trait S {
    def foo(x: Int): Int
    }
    val s: S|Null = (x: Int) => x
    ```
    - Inferred nullable unions: Dotty currently never infers a union type; instead, the union is eagerly widened.
    (see [#4687](https://github.com/lampepfl/dotty/issues/4867)).
    ```scala
    def foo(): Int|String = 42
    val x = foo() // x: Any inferred
    ```
    We changed the inference rules so that unions of the form `T|Null` are inferred:
    ```scala
    def foo2(): String|Null = "hello"
    val x = foo2() // x: String|Null inferred
    ```
    Otherwise, the nullable type `String|Null` would be collapsed to `AnyRef`, which loses too much information.

    - Nullable unions in prototypes: the compiler currently doesn't allow unions in prototypes
    ```scala
    def bar(a: Array[String|Int]|Int) = ()
    bar(Array(42))

    4 | bar(Array(42))
    | ^^^^^^^^^
    | found: Array[Int]
    | required: Array[String | Int] | Int
    ```
    Notice that the type of `Array(42)` is synthesized as `Array[Int]`, even though the
    (correct) type `Array[String|Int]` could be inherited.
    The problem is that the compiler sees a prototype of `Array[String|Int]|Int`, and because
    the outer type is a union it discards the prototype and switches to synthesis.

    See [here](https://github.com/lampepfl/dotty/commit/8067b952875426d640968be865773f6ef3783f3c) for
    why this was done.

    We've changed this behaviour so that nullable unions can be used in prototypes
    ```scala
    def bar(a: Array[String|Null]|Null) = ()
    bar(Array("hello")) // ok: inferred type parameter via prototype is String|Null`
    ```

    ## Other Languages