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

[lrhn]

I think being consistent with promotion is important (and probably a requirement of a consistent system).

We should be able to define expr! as equivalent to let v = expr in v != null ? v : throw CastError(...), and so we'll definitely have expressions with promoted types.

The edge cases are obviously the tricky ones.

• void! (and void?)
• dynamic! (and dynamic?).
• Object! if Object is nullable.
• Null!
• T! where T has a nullable bound, or is constrained to be nullable.

The ground rules I imagine are:

• A type T is nullable iff T == T? (where == is mutual sub-type or whatever equivalence we use on types).
• If T is not nullable, then T! should be T, and T?! == T

Since void? is void and dynamic? is dynamic, they are nullable. However, it's not clear that there is a non-nullable subtype T so that T? is dynamic or void, so I'd probably go with dynamic! == dynamic and void! == void.

An alternative is dynamic! == Object, which removes the dynamism, but is also predictable and useful, and fits that dynamic is Object? with a "dynamic" flag. (Or we could introduce the dynamic flag on all types, dynamic T for any type T, then (dynamic T)! would be dynamic (T!)). I don't see a similar equivalence for void. I don't see void as Object? with a flag (or maybe rather, I don't see it as a flag that you can safely loose). Again, if we introduce void T for any T, which is something that accepts any T, and you still can't use it, then (void T)! could be void (T!). So, in both cases, if we generalize the flags, then we can move the ! inside the flag. If not, we don't have a good option.

If Object is nullable, then Object! should be Object too. Object is probably not going to be nullable.

Null is nullable, so Null! should be something. Probably bottom, because Null == bottom?, so bottom?! should be bottom.

That leaves type variables.

If T is a type variable X with a non-nullable bound, or T is X & B where B is not nullable, then I don't know what X? is. It's probably just X | Null, because we don't allow raising the bound, but it's different from X, so T is not nullable and T! is T.

Otherwise, if the type T is a type variable X with a nullable bound (or constrained to be nullable) and X & B with a nullable B, then T? == T is probably true.

• If T is X, then T! is X & (bound of X)!
• if T is X & B, then T! is X & B!.

That is exactly what we would get if we actually promoted X x to that non-nullable type.

(We probably also want to allow promotions to non-nullable thorough is Object, assuming Object is non-nullable, so:

num? x = ...;
if (x is Object) {
   // x is num? & Object = (num & Object)(?&!) = num
   ...
}
num y = ...l
if (y is int?) {
  // y is num & int? = (num & int)(!&?) = int
}

That is: treat nullability and type as different and independent axes, so even if Object is not a subtype of num?, we still promote along nullability, and even though int? is not a subtype of num, we still promote along the type hierarchy.)

[munificent]

I don't claim to understand all of this, but at a high level it sounds reasonable to me.

num y = ...l
if (y is int?) {
  // y is num & int? = (num & int)(!&?) = int
}

I think this roughly parallels this code:

Future<num> y = ...
if (y is FutureOr<int>) {
  // ...
}

In principle, you could imagine promoting to Future<int> inside this because I think that's how the algebra of FutureOr works out. As far as I can tell, we simply don't promote at all.

Given that, can we just not support promoting around nullability in similar cases too?

[leafpetersen]

• A type T is nullable iff T == T? (where == is mutual sub-type or whatever equivalence we use on types).
• If T is not nullable, then T! should be T, and T?! == T

This doesn't work. A type variable X is not nullable by this definition (X? <: X does not hold), but it is definitely not the case that X! is the same as X.

[leafpetersen]

dynamic! == dynamic and void! == void

Well, this is an odd fit with the interpretation of T! as T & Object. We can probably make it work out, but... it's weird.

It's also weird that:

T! foo<T>() => (null as T!)
var x = foo<dynamic>();

is valid dart code that succeeds, and binds x to null.

Null is nullable, so Null! should be something. Probably bottom, because Null == bottom?, so bottom?! should be bottom.

This is an axiom in the intersection type interpretation I proposed here

[lrhn]

Type variables ... are indeed annoying because X, X? and X! are three different types. It's like X is the dual of X* - allow as little as possible, instead of as much as possible.

The way I think of type equality is in terms of a normal form reduction. I should try to complete writing that down. I would have reduction rules like:

• T?! ~> T!
• T!? ~> T?
• T!! ~> T!
• T?? ~> T?
• classType! ~> classType
• functionType! ~> functionType
• Null! ~> bottom
• Null? ~> Null

etc. In that setting, X? does not ~> to X, so X is not nullable. But it's also no non-nullable, because X! does not ~> to X. So, my attempt to summarize the rules introduced a false dichtonomy. I want that:

• If X? ~> X then X is nullable.
• if X! ~> X then X is non-nullable.

and then I want some consistent view of which types are nullable and which are non-nullable, and type variables (and only type variables, potentially promoted) can actually be neither.

About the dynamic! ~> dynamic idea: I'm not sure that

T! foo<T>() => (null as T!)
var x = foo<dynamic>();

succeeds because there is no dynamic at run-time. The run-time behavior, after inference, could then be:

T! foo<T>() => (null as T!)
Object? x = foo<Object?>();

If we replace Object? for T, we get Object?! foo() => (null as Object?!). If that has a meaning, it will throw.

So, as usual, we will need to distinguish the static type system and the run-time type system, where void and dynamic only exists in the static type system, and are replaced by Object? in the run-time type system.

The static inference of the first example above succeeds because T is treated as having Object? as bound. The static type of x becomes dynamic! which is dynamic. At run-time, that becomes Object?, and the rest stays the same.

I do think that we should be careful about promoting dynamic! to Object because it might happen inadvertently:

foo(dynamic something) {
  if (something != null) { something.floo(); }
}

Here the check != null should promote something to dynamic!. If that is Object, then we lose the dynamism just because we check for null.

We do allow promoting dynamic, so if (something is String) ... will remove the dynamism, so it's not entirely unprecedented, I just think it is likely to be wrong to lose the dynamism over a null-check. Maybe we just need to special case the promotion rules to avoid promoting, then we can say that dynamic! is Object in general.

I'm more worried about void! because making that Object seems completely wrong and counter to the intent of writing void.

[leafpetersen]

Question: are operations "?" and "!" designed to be associative?

no.

[leafpetersen]

So, as usual, we will need to distinguish the static type system and the run-time type system, where void and dynamic only exists in the static type system, and are replaced by Object? in the run-time type system.

This makes no sense to me whatsoever. You are proposing that dynamic! == dynamic statically, but you want dynamic! == Object?! == Object at runtime. This means that the static type system and the dynamic type system are enforcing different things, and that's just bad. That means, for example, that:

dynamic! x = null;  // Statically accepted, because dynamic! == dynamic
var x = (null as dynamic!); // Statically accepted, blows up at runtime because dynamic! == Object

There is a clean, simple, interpretation, which works out entirely consistently. That interpretation is that dynamic and void are nullable, and the ! version of them are non-nullable. Object either is or isn't. If you really need to be able to think about these in terms of underlying objects, think of the type system as having:

• TrueDynamic true non-nullable dynamic
• typedef dynamic == TrueDynamic?

and the same for void. We just happen to use the name dynamic for nullable dynamic, and dynamic! for TrueDynamic but it's just spelling.

[leafpetersen]

The way I think of type equality is in terms of a normal form reduction.

That's (perhaps) fine, but you need to understand that you are performing reduction on open terms. For closed terms, you can generally get all of the equations that you want by reducing to a normal form, and comparing. But that is not necessarily the case for open terms. Some systems do have the property that you can define the equational theory in terms of "normalize and compare", but others just flat out don't. I really don't think that you can use normalization to avoid reasoning about the equational theory of !.

[leafpetersen]

you get associativity automatically (if desired),

It's not desired. In fact, it's... completely wrong. :) int?! is a non-nullable int. int!? is a nullable int. They're just different.

bottom? = Null (if it makes sense).

This is an admissible axiom given my proposed rules (if by equality you mean mutual subtype), but it doesn't give you associativity. Why do you think it does?

[leafpetersen]

@tatumizer You're right - I misread what you were saying. This is getting a bit noisy, can we drop the topic, or take it offline, or to a separate topic specific issue? To summarize the properties that we do want (and I believe do get with my proposed rules):

• What you are calling commutativity: no (and we don't want it). int?! is different from int!?
• "Cancellation": yes. int?! = int!, and int!? = int?
• Idempotence: yes. int!! = int!, and int?? = int?

I believe that all of these properties are satisfied by the rules I have proposed. See in particular the application of the distributivity of intersection over union in the development of the algorithmic rules.

If you believe that I've made a mistake there (this is very possible!) and some of these equations are not derivable, can you file a separate issue with a concrete example of the missing derivation? For the purposes of this issue, let's take it as a given that we can make the type theory work so that we can focus on the question of the utility of the operator.

[lrhn]

If we look at the type promotion, we already introduce intersection types in some cases.

I expect if (x != null) to promote the static type of x like:

• If it's a subtype of Object, do nothing (assuming non-nullable Object). Perhaps give a warning since the test cannot fail.
• If it's a type variable X with bound B, then it becomes X&(non-null promotion of B).
• If it's a type variable intersection X&B, then it becomes X&(non-null promotion of B).
• If it's T? then it becomes the non-null promotion of T.
• For FutureOr, we have the known problem. We may want to introduce FutureOr<T> & U as an intermediate promotion result.
• If it's dynamic or void, then ... dynamic & Object is Object, so maybe just that. But it would remove the ability to do dynamic invocations.

A problem with having an explicit ! operator is that it makes these intersection types expressible. We already have the problem that we don't want to reify these intersection types:

foo<T extends Widget>(T x) { 
   if (x is SubWidget) {
     var w = x;  // static type of w is *not* T&SubWIdget, just T, but perhaps known to be T&SubWidget
   }
}

Doing the same for non-null:

foo<T extends Object?>(T x) { 
   if (x is Object) {
     var w = x;  // static type of w is `T`, but not `T & Object`
   }
}

would still allow us to avoid reifying the intersection type. If the user can write:

foo<T extends Object?>(T x) { 
  T! w = x!
}

then either that doesn't do what they expect, or it reifies the intersection type. Both are bad. Not doing a perfect implicit promotion is easier to defend than not doing what was explicitly asked for.

[eernstg]

@leafpetersen, @lrhn, @munificent, are we gravitating in the direction of "no, we won't have this feature"?

[leafpetersen]

Not planned.

[ajmalk]

Are there any plans to add something like this? I ran into wanting this today to add a simple extension function to Stream. What I wanted to do was (something like) this:

extension NullableStreamHelpers<T extends Object?> on Stream<T> {
  Stream<T!> ignoreNulls() => where((event) => event != null).map((event) => event!);
}

As far as I know, this isn't possible in dart? I've seen this kind of thing used to great effect in Swift.

Apologies is this has been answered elsewhere but it's been more than a year and I'd figure I'd bump this again. 😊

PS: I'm not sure the NullableStreamHelpers<T extends Object?> correctly either but I guess that would be a different feature?

[mateusfccp]

@ajmalk You can use T extends Object instead.

[Levi-Lesches]

@ajmalk You can use T extends Object instead.

You can't, becuase he wants to allow the extension to be used on streams of nullable types, to ignore those nulls. He wants a way to say "allow this on a stream of nullables, but this method only returns the non-nullable version of that type". I think that's pretty reasonable.

[munificent]

What you want is probably:

extension NullableStreamHelpers<T> on Stream<T?> {
  Stream<T> ignoreNulls() => whereType<T>();
}

[Levi-Lesches]

Well whereType isn't defined for Streams, so I had to do it myself, but I see your point is that we should use a non-nullable type, and then add ?, instead of the other way around -- using nullable types and then adding a !. Here's my code for the Stream example, now working.

extension NullableStreamHelpers<T> on Stream<T?> {
  /// Making [R] a subtype of [T?], avoids cases where there can't be a match, like `int?` -> `String`
  Stream<R> whereType<R extends T?>() => where((event) => event is R).cast<R>();
  Stream<T> ignoreNulls() => whereType<T>();
}

[lrhn]

We have whereNotNull for iterables in package:collection. We could add similar methods to Stream in package:async.

[dickermoshe]

@mateusfccp

You can use T extends Object instead.

This doesn't work for extension types :(, they aren't objects

[mateusfccp]

@mateusfccp

You can use T extends Object instead.

This doesn't work for extension types :(, they aren't objects

@dickermoshe I don't know exactly what you are trying to do, but extension types can implement Object:

extension type Id(int _id) implements Object {
  // Makes the extension type non-nullable.
  static Id? tryParse(String source) => int.tryParse(source) as Id?;
}