NNBD Design

This are intended as a "full" NNBD design.

The Type System

Dart types already include, in both the static and runtime type system, the following type kinds:

C<T₁...T_n>: Class types (including generics, including Null).
FutureOr<T>
T₀ Function(...T₁...T_n...): Function types with various kinds of parameter signatures. In the type part of this document, we'll mainly care about the individual parameter types, not whether they are positional or named. Optional parameters will need to be addressed separately.

For NNBD we will also introduce bottom as an expressible type, both static and at runtime, and nullable types of the form T?.

We also already have the following static type system-only types:

dynamic (static only variant of Object?)
void (another static only variant of Object?).
X (type variable)
X & T (promoted type variable)

For NNBD we will introduce the statically unsafe nullable types T* as a static only variant of T?, the "unsafe nullable type" which allows invocations and assignment from the type as if it was not nullable, and assignment to the type as if it is nullable. This type arises from unmigrated code.

The T* type will not occur at runtime because enabling NNBD runtime semantics requires treating the entire program as migrated.

We may also introduce an non-expressible top type that both Null and Object implement, but it's only a specification tool to specify allowed member invocations on Object?. It should have no effect on the rest of this document.

Subtyping

We define subtyping as usual for the existing types:

Class types: Based on super-interfaces and covariant type parameters, except Null is no longer a subclass of Object. They are both parallel "top types" with no superclass.
FutureOr<T> is least supertype of T and Future<T> (supertype of both, subtype of any type that is also a supertype of both), covariant type parameter.
Function types with the same structure are invariant on type parameter bounds, covariant on return type and contravariant on parameter types, and subtypes can also allow more optional parameters. Also <: Object.
dynamic is equivalent to Object? for subtyping.
void is equivalent to Object? for subtyping.
bottom is a subtype of all types.
X, a type variable, is a subtype of its bound.
X & T, a promoted type variable, is a subtype of its bound and of T.

We add the following rules for the new types T? and T*, where T* is equivalent to T? for subtyping, and T? is a least supertype of T and Null, so:

Null <: T?
T <: T?
T <: S & Null <: S ⇒ T? <: S

And also idempotence:

T ?? <: T?

(From those rules we can derive covariance, T <: S ⇒ T? <: S?)

And finally, we have reflexivity and transitivity:

T <: T
R <: S & S <: T ⇒ R <: T

Promotion To Non-Nullable

We can promote some static types to non-nullable static types as defined by the PRO function:

PRO(Null) = bottom
PRO(C<T₁, ... , T_n>) = C<T₁, ... , T_n> for class C other than Null
PRO(FutureOr<T>) = FutureOr<T> -- no promotion, even if T is nullable, sorry.
PRO(T₀ Function(...T₁...T_n...)) = T₀ Function(...T₁...T_n...)
PRO(bottom) = bottom
PRO(dynamic) = dynamic
PRO(void) = void
PRO(X) = X & PRO(B), where B is the bound of X.
PRO(X & T) = X & PRO(T)
PRO(T?) = PRO(T)
PRO(T*) = PRO(T)

One tricky case is dynamic. We do not promote because it would make code like:

dynamic foo = someListOrString;
if (foo != null) return foo.length;

no longer work. If you check a dynamic object for null, it's because you are going to call something on it. If the check promoted the variable to type Object, it would remove the ability to do that call, which is counter-productive.

A check like if (dynamicThing is String) would promote to String, but pure non-null promotion, where there is no explicit type to cast to, does not affect the dynamic type.

The opposite argument goes for void, where only an is check can be used (sadly we allowed that), and on the negative branch of if (voidVariable is Null), you should still not be allowed to use the variable.

Assignability

We remove implicit down-casts from anything but dynamic, so assignability is almost the same as subtyping, except from dynamic or where an unsafe nullable type, T*, occurs in the type.

The T* type in the static type system is a variant of T?, and with the same subtyping rules as T?, but different assignability/override rules.

Define COV(type) as:

COV(C<T₁,...,T_n>) = C<COV(T₁),...,COV(T_n)> -- n may be zero for non-generic types
COV(FutureOr<T>) = FutureOr<COV(T)>
COV(T₀ Function(...T₁...T_n...)) = COV(T₀) Function(...CON(T₁)...CON(T_n)...)
COV(bottom) = bottom
COV(dynamic) = dynamic
COV(void) = void
COV(X) = X
COV(X & T) = X & COV(T)
COV(T?) = COV(T)?
COV(T) = COV(PRO(T))

and CON(type) as

CON(C<T₁,...,T_n>) = C<CON(T₁),...,CON(T_n)> -- n may be zero for non-generic types
CON(FutureOr<T>) = FutureOr<CON(T)>
CON(T₀ Function(...T₁...T_n...)) = CON(T₀) Function(...COV(T₁)...COV(T_n)...)
CON(bottom) = bottom
CON(dynamic) = dynamic
CON(void) = void
CON(X) = X
CON(X & T) = X & CON(T)
CON(T?) = CON(T)?
CON(T*) = CON(T)?

These transformations convert T* to either T or T? depending on whether the T* occurs covariantly or contravariantly.

Then S is assignable to T written S <<: T, if COV(S) <: CON(T), or if S is dynamic.

For overrides, we require the function type of the override to be assignable to the signatures it overrides in all superinterfaces (plus the normal covariant tweaks).

Normalization

We define type normalization as:

NORM(Null) = bottom?
NORM(C<T₁,...,T_n>) = C<NORM(T₁),...,NORM(T_n)> for class C other than Null.
NORM(FutureOr<T>) = FutureOr<NORM(T)>
NORM(T₀ Function(...T₁...T_n...)) = NORM(T₀) Function(...NORM(T₁)...NORM(T_n)...)
NORM(bottom) = bottom
NORM(dynamic) = dynamic
NORM(void) = void
NORM(X) = X
NORM(X & T) = X & NORM(T)
NORM(T?) = case NORM(T)
- of FutureOrⁿ<R?>, n >= 0, then FutureOrⁿ<R?>
- of FutureOrⁿ<R*>, n >= 1, then FutureOrⁿ<R*>
- of R* then R?
- of S then S?
NORM(T*) = case NORM(T)
- of FutureOrⁿ<R*>, n >= 0, then FutureOrⁿ<R*>
- of FutureOrⁿ<R?>, n >= 1, then FutureOrⁿ<R?>
- of R? then R*
- of S then S*

After normalization, there is never a type of the form T??, T?*, T*? or T**, in all cases the last modifier wins.

Normalization is congruent with the other functions so:

NORM(PRO(T)) = NORM(PRO(NORM(T)))
NORM(CON(T)) = NORM(CON(NORM(T)))
NORM(COV(T)) = NORM(COV(NORM(T)))

Also, for all types T:

T <: NORM(T)
NORM(T) <: T
T <<: NORM(T)
NORM(T) <<: T

(Caveat: I haven't actually proven any of this yet)