Promoting type variables

[FMorschel]

Context

As I've commented on dart-lang/sdk#56028.

Consider:

mixin M {
  void m();
}

class M1 with M {
  const M1();
  @override
  void m() {}
}

class A<T> {
  const A(this.o);
  final T o;
}

class B<T extends M> extends A<T> with M {
  const B(super.o);
  @override
  void m() => o.m();
}

void foo<T>(T o) {
  late A<T> a;
  if (o is M) {
    a = B<T>(o); // 'T' doesn't conform to the bound 'M' of the type parameter 'T'. Try using a type that is or is a subclass of 'M'.
  } else {
    a = A<T>(o);
  }
}

Today this code has only "bad" solutions (the basic ways I could think of were not able to solve this and I could not think of another solution than the following), one which was proposed later on that same issue involves calling a helper function with (fn as Function)<T>(...). This is doable by the programmer but it's easier to get it wrong.

From @eernstg in dart-lang/sdk#56028:

void foo<T>(T o) {
  B<S> fooHelper<S extends M>(S o) {
    // In this body the type system knows that `S extends M`,
    // so we can create a `B<S>`.
    return B<S>(o);
  }
  
  late A<T> a;
  if (o is M && <T>[] is List<M>) {
    // At this time we know that `T extends M`. The type system
    // won't recognize that, but we can force it using a dynamic
    // invocation of a generic function.
    a = (fooHelper as Function)<T>(o);
  } else {
    a = A<T>(o);
  }
}

Request

I'd like to request/propose that type arguments could be tested for specific bounds.

That would not only return a true or false for the test expression, but it would also consider that in the inner context.

That would make it so that in this context:

void foo<T>(T o) {
  late A<T> a;
  if (T <: M) { // Trying to imitate your writings from previous issues but if I got it the wrong way around please disconsider
    a = B<T>(o); // Here `T` would then be considered as a subtype of `M` and could be used as the type parameter on `B`
  } else {
    a = A<T>(o);
  }
}

This would be more of a "help" for the language to type-solve harder contexts.

[lrhn]

Type variable promotion came up in a discussion about promoting this.

When you do if (this is C<int>) inside class C<T> you are asking whether T is a subtype of int. There's more than one reason we can't promote this, but this is one of them.

Let's just assume we introduce some way to test a type variable, strawman T1 <: T2.

First, the declared type of a type variable declaration with name X and bound B is X extends B.

If the current static type of X is X extends B, evaluation of X <: S gives true, and T2 it's a subtype of B, then the static type of X is promoted to X extends S on the true branch of the test.
As usual, the members available on X & B are those of B.

We also need to do something about promoted variables with a type of X & P. We used to know that P is a subtype of the bound of X, but if we have promoted the bound of X, that may no longer be true. The promoted variable's actual value's runtime type will be a subtype of the actual type of X, but if the type hierarchy have a diamond structure, we may have types on different branches.

So let's include the bound we promoted from in the intersection type, so it's X extends B & P, not just X & P.
Then a variable with type X extends B & P, P <: B, where the current static type of X is X extends S, S <: B, behaves as follows:

• it's a subtype of S, P and X. (Means assignable to any of S, P and X extends Z for any Z.)
• the interface used for member access is:
  • if S <: P, then S
  • otherwise P.

And if we promote T, then a this of type C<T> will get promoted too, since it's the same type variable.

  List<T> list = [];
  if (T <: int) list.add(2);

As usual, further promotion from X extends B & P needs to be with a subtype of P. If it ends up being with a subtype of P which is a supertype of S, we could just erase the intersection. Whether that's confusing needs a usability check, logically it should be sound.

(If we get contravariant type parameters, num <: X would promote X super int to X super num too. Variable promotion is always covariant, so will have to consider if there is something to worry about in that interaction.)

I said above that the scope was "on the true branch". There's a little more to flow analysis than that.
The main issue is joins, where two different promotions join, and we want to preserver as much as possible.
For promoted variables, we (IIRC) intersect the promotion chains and union the type-of-interest sets.
Type variables are immutable, so we don't need "types of interest" for assignment promotion. Maybe we do need promotion chains for gradual demotion. If we've established on one branch that X extends num and X extends int, and on the other that it extends num and double, we probably do want to remember that it extends num.

So, for each type variable, we retain the chain of types it has had so far, starting at the original bound X extends B, and every further promotion done after that.
At a join point, we take the intersection of those chains, which will always contain at least the original bound X extends B.
Then we try to do a little better, and take the UP of the most promoted types of each chain, and if that's better than (subtype of) the last type of the intersection chain, we add that to the chain. The promotion chain of X after the join is then that chain, meaning that its static type is the last entry of the chain. (The "UP if it's better" is like a context-bounded UP, it's never worse than what we already know, even if UP itself can sometimes be ... difficult.)
There is no worry about "types of interest" for a variable, we're joining types themselves.

Example:

List<T> foo<T extends Object>(T value) {
  List<T> result;
  if (T <: num) {
    // Promotion chain `T extends Object`, `T extends num`
    if (T <: int) { 
      // Promotion chain `T extends Object`, `T extends num`, `T extends int`
       result = Uint32List(1)..[0] = value; 
    } else if (T <: double) { 
      // Promotion chain `T extends Object`, `T extends num`, `T extends double`
      result = Float32List(1)..[0] = value; 
    } else {
      throw ArgumentError.value(T, "T", "Must be concrete type if number");
    }
    // Promotion chain `T extends Object`, `T extends num` (intersection)
    // and `T extends UP(int, double)` = `T extends num` was already there.
    // T is still `num`-bounded.
  }
  // Back to `T extends Object`.
  result ??= <T>[value];
  return result;
}

One thing that worries me a little is that there is no way to demote, other than leaving the scope of the promotion.
If one has promoted a final variable from A to B, and I want to check if its value is also a C (with the classical diamond type hierarchy A :> (B <!> C) :> D, "<!>" meaning B and C are unrelated), then I can assign the value to a different variable of type A and check that. The value is separate from the variable that was promoted, and can be alised.

A type variable with bound A promoted to bound B gives no way to check and promote to C as well, because we don't have local type variables, no way to alias a type variable before we promote it, or create a demoted version of it after. I can't give the same "value" a new name and starting type, and start from scratch. (Or I can, but it requires introducing a local function with type arguments, and if I do anything remotely interesting in the function body, it will probably break normal variable promotion for the variables it uses.)
The usual suggestion here is to treat IIFEs as if they were inlined, or introduce a similar let construct, but then it a let construct should also be able to bind type variables.

If I could do, say, typevar Y extends A = X; if (Y <: C) ... and promote Y to ... well, something then ... something.(Why is Y not Y extends (X extends B) to begin with. Should I use typevar Y extends X = X;? Which difference would it make? Would we need "types of interest" anyway to avoid the initial promotion? Would we want local type variables to be assignable? Whoa, mind blown!)

If we start treating type variables more like variables than like anonymous types, then we might end up wanting to treat them more like variables! (But still, never ever convert a Type object back to a real type. The values of type variables is still limited to the types that actually occur as type arguments somewhere in the program, where typevar X = T; means T counts as a type argument.)

[FMorschel]

That's a lot to think about, I'll take some time to answer more things as I fully comprehend them.

Just one thought that occurred to me, about what you said

[...] we don't have local type variables, no way to alias a type variable before we promote it, or create a demoted version of it after. I can't give the same "value" a new name and starting type, and start from scratch. (Or I can, but it requires introducing a local function with type arguments, and if I do anything remotely interesting in the function body, it will probably break normal variable promotion for the variables it uses.)

This could be thought about creating something along the lines of:

void fn<T>() {
  if <T2 extends T>(T <: S) {
    // In here we would have `T2` as a new type variable that means the above.
  } 
}

The syntax is similar to the rest and we could think about allowing this only inside if blocks (maybe switch as well?) and not in for/while blocks since at least for me it doesn't make much sense.

[eernstg]

Cool stuff! Here's a fun consequence of promoting a type variable:

// --- Library 'looks_innocent.dart'.

extension E on A<num> {
  void bar() => print('In E.bar!');
}

// --- Library 'my_program.dart'.
import 'looks_innocent.dart';

class A<X> {
  void foo() {
    if (X <: num) {
      bar();
    }    
  }
}

The ability to call bar arises because of the promotion of X that allows us to conclude that it is a subtype of num, and then because the type of this is A<X>, and then because of the extension with on-type A<num>.

It's probably not much harder to keep track of this than a number of other situations in Dart, but it does give rise to some new causal connections.

It is also worth noting that we might want to get even more control:

List<T> foo<T extends Object>(T value) {
  List<T>? result;
  if (T <: int) {
    result = (Uint32List(1)..[0] = value) as List<T>;
  }
  result ??= <T>[value];
  return result;
}

The cast to List<T> is necessary because T could be Never (or any other type which is not a supertype of int). So we might well want to promote T to satisfy an equality constraint, or at least a lower bound.

[mateusfccp]

The cast to List<T> is necessary because T could be Never (or any other type which is not a supertype of int). So we might well want to promote T to satisfy an equality constraint, or at least a lower bound.

Couldn't we do something like (consider > as "is a supertype of"):

List<T> foo<T extends Object>(T value) {
  List<T> result;
  if (T <: int && T > Never) { // T is subtype of int but can't be Never
    result = Uint32List(1)..[0] = value;
  }
  result ??= <T>[value];
  return result;
}

[lrhn]

What you want is probably to ask whether T implements the interface int, which Never doesn't, it's "just" a subtype.

Checking T is a proper supertype of Never is one way to do that, because today bottom types are the only subtypes that don't implement their supertype, but who knows what tomorrow will give us 😁
It's better to ask about precisely the thing you want to know, rather than something that is (currently) correlated with it.

But Never <: T && !(T <: Never) should be exactly "T is a proper supertype of Never" (and the first test is trivially true when the type you compare to is Never).

[FMorschel]

One more thing. This would also help in "breaking up" type variables into "new" (inner) ones.

E.g.:

void foo<T extends Object?>(T obj) {
  if <E extends Object?>(T <: Iterable<E>) {
    // In here we know that `T` is an `Iterable` and we can work with `E` as the type for all elements in it.
  }
}

Today we can almost do this. There are some limitations but:

extension Ext<E extends Object?> on Iterable<E> {
  // Here we have a way to work with the type `E`
}

If we use the above extension, testing that obj is Iterable<Object?> should allow us to use any method that we add here. Then that if test mentioned before could do the same as having this extension scope.

It would be much more convenient to define the predicate T <: int so that Never doesn't satisfy it. The verbal equivalent of T <: int is "T implements int".
If you want to isolate Never, you can explicitly write if (T == Never). Type comparison via == and != works today, so no new syntax is necessary. You should be able to write if (T == String), write a switch statement over T, etc. I figure that it's relatively easy to implement: the compiler can pass along some hidden boolean arguments (one per each type comparison in the method body, evaluated at the call site - which is possible because at the call site, the compiler statically knows what T is).

[eernstg]

@lrhn wrote:

What you want is probably to ask whether T implements the interface int, which Never doesn't, it's "just" a subtype.

That wouldn't suffice in examples like the one I mentioned: We're returning a Uint32List(1)..[0] in a function whose return type is List<T>, and we can only know that this is type correct if we know that int <: T.

(int is special because we don't have any .. official .. types that are proper subtypes of int and not bottom types, so checking that T is not a bottom type would suffice. But the same example with class A {} and class B extends A{} rather than num and int would show that this is not enough.)

So we'd need to handle int <: T.

"OK, no big deal?"

Well, I considered that to be a separate feature. In a context where we are talking about "promotion" of type variables: We don't have anything similar for promotion of value variables, which will establish that the value of a promotable variable has a type which is a supertype of anything, we can only establish that it is a subtype. So if we only support promotion of type variables then we'd only support T <: SomeType, and SomeType <: T would be a separate feature.

"No big deal again?"

Suppose we allow type variable "promotions" to be established using a more general form S <: T where S and T are types. For example, if X and Y are type variables then we could test Map<List<X>, X> <: Map<Iterable<Y>, Comparable<X>>. We would then know that X <: Y (because otherwise that subtype relationship couldn't possibly hold), and also that X <: Comparable<X>.

This is all sound and fine, but it is not obvious to me that we can easily characterize the exact set of conclusions that we can draw from a general test of the form S <: T. Are we going to go on an endless hunt for additional cases where we can squeeze out some more inequalities?

I think it's at least worth considering a simple model where we only support "promotions" of type variables in very specific ways. For example, only the left operand is "promoted" (so it must be a type variable), and we can test lower and upper bounds, as in X <: T and X :> T, where X is the type variable which is subject to "promotion" and T is a type (T could even be a type variable, but it won't be "promoted").

[eernstg]

@tatumizer wrote:

It would be much more convenient to define the predicate T <: int so that Never doesn't satisfy it.

How would that be useful in the more general case X <: S where X is a type variable and S is a type? Why do you care whether the value of X is actually a subtype of S which is not Never, or X is a subtype of S and it might be Never? What is it that you can do if X is not Never, but you couldn't do it if X might be Never?

As far as I can see, the Dart type system just doesn't have a way to express this kind of knowledge. We may know that a type variable has a specific upper bound, but we never know that it doesn't satisfy that upper bound by having the value Never. I can't see how this knowledge could be used to type an expression that couldn't be typed just as well without the knowledge that X != Never.

If it is not about the typing but only about what to do next then we can test X == Never directly.

if (X <: int) {
  if (X == Never) throw "Impossible type encountered!";
  // `Never != X <: int` is now known to us,
  // but the type system only knows `X <: int`.
}

[eernstg]

@FMorschel wrote:

This would also help in "breaking up" type variables into "new" (inner) ones.

Right, that's the "existential open" operation, which can also be seen as an application of type patterns (#170). But the ability to introduce fresh type variables and bind them during a type test is a feature in its own right.

What was the reason for NOT introducing a type parameter for Type? (I remember some discussions years ago, but I don't remember the rationale).
With a type parameter, we could just check if (T is Type<num>) without introducing any new syntax, at the same time (hopefully) resolving confusion about Never. (Unless Never is Type<num> will return true. Will it?)

[lrhn]

One argument against a generic Type was that if we ever got an "existential open" or "type parameter pattern" (which I personally hope we will), it allows you to convert a Type object to a type parameter, which is bad for tree-shaking.
If anyone does o.runtimeType in one place, and case Type<var X>: ... in another, the AoT compiler may have to retain a lot more runtime type information, where today it only needs that kind of information for types that are actually used as type arguments in at least one place.

Also ,Never is Type<num> would be true, because Type<T> would definitely be covariant in T.

[eernstg]

We should be acutely aware of issues like less effective tree shaking, but I do not believe it is known to be an unavoidable (or even likely) consequence of adding a type argument to Type. So #2090 can still happen.