Do we need a non-nullable type operator (`T!`)?

[leafpetersen]

[EDIT] The resolution of this is that we're not taking this approach now. We could reconsider in the future if we have demand for it. A workup of the equational theory was done here.

This issue is for discussion of the question of whether we should add a type operator which strips off the nullability from a type. That is, if T is a type, then T! would be the non-nullable version of T.

class C<T> {
  T! foo(T x) {
     if (x == null) throw "Badness";
     return x;
  }
}
void test() {
  int x = new C<int?>().foo(3);
  int x = new C<int>().foo(3);
}

cc @lrhn @munificent @eernstg

[munificent]

My take, for the record, is that I don't know that we need it. I think the simplest option is to assume we don't and then see how migrating the core libraries go without it.

[leafpetersen]

Example from @lrhn where it would be good to have: places where you want to use null checks to promote to a non-nullable type.

// Note, non-nullable bound on type parameter
class Box<T extends Object> {
  T x;
  Box(this.x);
}
class F<T extends Object?> {
  Box<T!> box(T x) {
     if (x != null) return Box<T!>(x);
     throw "Something";
  }
}

Without the ! operator, there is nothing we can write for the type argument to the Box constructor, even though we have a non-null T.

[leafpetersen]

To explore this question further, I worked out a draft of the equational theory here. It seems to work out, but is a bit heavyweight.

For the most part, I think implementations could maintain a normal form that avoids having to deal with nesting of ! and ?. However, the ! would need to be represented at runtime, since FutureOr<int?>! is not otherwise representable. In principle, implementations could choose to break FutureOr down into the underlying union type, but then you have a type floating around at runtime for which we have no source level representation: Future<int?> | int. Error reporting with such types seems likely to be confusing.

[leafpetersen]

A couple of comments on other languages.

Kotlin doesn't seem to have an explicit version of this that I can find. However, it does seem to be able to represent non-nullable versions of type variables, either in the type system, or via some sort of parallel tracking. Example:

fun <S : Int?, T : S>testNullAssertion(x : T) {
    x.div(3);  // Errror
    if (x != null) {
        x.div(3); // Ok
    }
    var a = x!!; 
    a.div(3); // Ok
}

In Typescript, you can represent this directly using intersection types:

function check(s: String | null) {
  s.length; // Error
  checkNull(s).length; // No error
}
function checkNull<T>(x: T): T & Object {
  if (x == null) {
    throw "Null error";
  } else {
    return x;
  }
}

This is relevant to #196, since without this type operator we can't express the non-nullability of the result of a null assertion operator in the type system, and would have to do something separate (as Kotlin appears to do).

[munificent]

Ah, dang, you're right. Otherwise:

foo<S extends Int?, T extends S>(T value) {
  var checked = value!; // What is the type of checked?
  checked + 1; // How is this allowed?
}

We could conceivably restrict a bare ! to only be used in places where there is a context type so that we know what the resulting type is. And then special case !. to allow method calls on the underlying nullable type.

That feels pretty hokey to me, though.

What about:

foo<S extends Int?, T extends S>(T value) {
  if (value != null) {
    value + 1; // Allowed?
  }
}

Intuitively, I would expect this to promote and thus allow the +. Does the type system need ! to enable this?

[zoechi]

Just a thought. If this is only for rare cases perhaps a function (like identical()) would be a better option to not complicate Darts syntax unnecessarily.

[leafpetersen]

Does the type system need ! to enable this?

If we want to track it is part of the type system, yes. It's conceivable that we could specify the errors and warnings for method calls via a notion of nullability that incorporates (but supersedes) the type. More or less, I think this is mostly equivalent to having ! in the internal type system but not the external type system, but you could probably also think of it as just being an extra "bit" that you propagate on expressions. Feels a bit baroque though.

[leafpetersen]

Suppose x has nullable type FutureOr?

I'm not sure I see the issue. Is there something particular about FutureOr that I'm not seeing here? In general, the type system already has to be aware of the semantics of await. That is, if e has type T then we currently say that await e has type flatten(T), where flatten basically unwraps one level of Future or FutureOr. With NNBD, flatten will need to account for nullability, probably by adding a case that says that if T has the form S? then flatten(T) is flatten(S)?.

[leafpetersen]

There's a bit of a problem with the expression FutureOr<int?>?! though.

You do need to account for how ! interacts with the union as part of flattening, but I don't see it as a problem, at least not here. For your specific example, await e where e has that type should have type int?, FutureOr<int?>?! is the same as Future<int?> | int, and awaiting the latter can give you an int or Null. In general, I think if we have !, we have to extend flatten with a case that looks something like:

flatten(T!) = flatten!(T)

where

flatten!(T?) = flatten!(T)
flatten!(Future<T>) = T
flatten!(FutureOr<T>) = T
flatten!(T) = T!

I think that works out. FutureOr is definitely something that needs further exploration though. I'm not 100% convinced that there aren't subtyping judgements that we ought to be able to prove that we'll fail to prove because we can't distribute the ! over the union.

[leafpetersen]

My main concern with not having this feature is that it makes it hard to explain what the type of x! (the null assertion operator applied to an expression) is, and what the type of a promoted possibly nullable variable is. Thinking about this more today, I think there are actually some fairly reasonable choices that we can make.

For simple types, it's clear what we can do:

foo(int? value) {
  value!.isEven;  // value! has type int
  var x = value!;
  var l = [x]; // inferred as List<int>
  if (value != null) { // value is promoted to int
    value + 1; 
  }
}

We can extend this to type variables with concrete bounds by promoting the bound:

foo<T extends int?>(T value) {
  value!.isEven; // value! has type `T extends int` (or `T & int`)
  var x = value!;
  var l = [x];  // inferred as List<T>
  if (value != null) { // value is promoted to `T extends int` (or `T & int`) 
    value + 1; 
  }
}

This does have the same unfortunate issue that we have with existing promotion on type variables: namely that inference needs to strip off the promoted type, at least in reified positions. So note the inferred type of l in var l = [value] must be List<T>, which doesn't capture the fact that value is known to be non-null. If we had the ! type operator, we could infer this as List<T!>. This is already the case with other kinds of promotion, however, so it's not a new anomaly.

The trickier case is type variables with chained bounds. Consider the following example:

foo<S extends Int?, T extends S>(T value) {
  value!.isEven;
  var x = value!;
  var l = [x];
  if (value != null) {
    value + 1; 
  }
}

One answer is to simply say that this code is invalid: that is, we don't promote on these kind of type variables, and value! just doesn't work.

The latter is really unfortunate, so a second answer is to instead say that value! has type int when value has type T, since int? is the ultimate bound of T after chasing through the type variable indirections. This means that value = value! is now invalid and requires an explicit cast, since int is unrelated to T, but most of the time one is likely to do value! in order to call a method on value, and that should always work out.

A final possible answer is to allow promotion based on the ultimate bound after chasing through the chain of type variables. That is, in the intersection type terminology, treat value! as having type T & (S & int), or in the formulation where you treat this as bounds strengthening, view it as having type T extends (S extends int). That is, strengthen the bound of T to be a version of S which has had its bound strengthened.

This has the same unfortunate behavior around inference and reification. We would not be able to infer any type for var l = [x] other than List<T> since T & (S & int) is not a first class type in the language.

Overall though, this feels like a solution that covers a lot of ground, and the inference anomalies are at least consistent with how we deal with promotion.

cc @stereotype441