Type decomposition

[eernstg]

It can be useful to test whether a type satisfies certain constraints, and when more than one type satisfies them: how this particular type satisfied them. Here are a couple of examples:

In response to #40 about adding functionality to existing types, scoped static extension methods were proposed in #41. They call for a mechanism that will enable the specification of certain constraints on types as well as the ability to declare type variables that are bound to specific types as a result of the procedure whereby it is verified that the constraints are satisfied. The basic idea is that an extension is applicable to a given expression if the static type of that expression matches the extension, and the matching procedure can make such things as the type arguments of a class available for the extension methods. The specification of static extension methods is still under construction, but here's an example illustrating the idea:

// Example from scoped static extension method proposal.
extension ListFancy<T> on List<T> {
  List<T> copyReversed() => List<T>(this.length)..setAll(0, this.reversed);
}

In this example, the extension method mechanism could be specified such that the type variable T is bound to the value of the actual type argument to the dynamic type of the list denoted by this, which enables the creation of a list with the same type argument in the body of copyReversed. Alternatively, the mechanism could be specified such that T is the static type of the expression which is the receiver of the invocation of copyReversed.

The language team has previously discussed mechanisms for performing an 'existential open' operation (coming up, e.g., in https://github.com/dart-lang/sdk/issues/31953#issuecomment-364954189 and https://github.com/dart-lang/sdk/issues/33841#issuecomment-405109060), in which the ability to introduce new type variables and bind them to values obtained by inspecting the dynamic type of a given instance is the main purpose of the mechanism. Here is an example of how that mechanism could be used:

main() {
  List xs = ...; // Some non-trivial computation, such that the exact type is not known.
  if (xs is List<?X>) {
    // Here, `X` denotes the exact type argument of the
    // dynamic type of `xs` at `List`.
    List<X> ys = [];
    ys.add(xs[0]); // No dynamic check needed.
  }    
}

In this example, it is tested whether there exists a type S such that xs has type List<S>, and if this is true then the type variable X is introduced into the scope of the following block {}, bound to S.

The general point here is that it can be useful to perform a check, at compile time or at run time, of whether a given type satisfies some constraints which may be expressed in a form which is itself similar to a type, and also to introduce and bind certain type variables to types in order to provide information about how those constraints were satisfied.

[hpmv2]

This doesn't solve the problem but I thought it may be interesting to mention.

The type parameter can be extracted for arbitrary use if we add an instance function within List:

abstract class List<T> {
  // ...
  void forTypeArg(void Function<R>() func) => func<T>();
}

then example above can then be written as:

xs.forTypeArg(<T>() {
  List<T> ys = [];
  ys.add(xs[0]);
});

(except for dart2js local functions can't have type args)

[eernstg]

@hpmv2, it's true that we can use access to the target class to write a method that will almost serve as an existential open, but it is still not quite the same thing:

main() {
  Map map = e;
  if (map is Map<?X, X>) {
    // We now know that `map` is an instance of some `Map<X, Y>`
    // such that `Y <: X`.
    X x = map.values.first; // We just hope it isn't empty. ;)
    map[x] = x; // Safe.
  }
}

So the difference is both that we avoid the need to edit the target class, and also that we are able to introduce relationships between the type arguments above and beyond whatever we might know from the declared bounds of the corresponding formal type parameters. And the Safe statement is actually sound, not just compilable and possibly failing at run time.