Look up a type variable at a given superinterface

This feature is inspired by the discussion in this issue, where an example with the following structure is given as motivation:

Note that this proposal mentions both a syntax that will definitely work (ImplementsAtN<AType, ASuperinterface>) and a pseudo-syntax which is (possibly) more readable (AType@ASuperinterface.TheNthTypeVariable). The latter is used in commentary in order to provide an additional way to see what's going on.

Background, Motivation

We can declare generic classes like this:

class A<X, Y> {}  
class B<Z extends A<dynamic, Y>, Y> {}

class TestA extends A<String, String> {}
class TestB extends B<TestA, String> {}

However, this may be inconvenient because we'd actually just want to compute the value of Y based on the given value of Z. We could also pass the actual argument (as we actually do above when passing String as the second type argument to B in the declaration of TestB), but that seems redundant because TestA already has A<String, String> as a superinterface.

However, we typically have to pass that 2nd type argument to B, because it will otherwise be inferred as dynamic.

So why can't we write those declarations as follows?:

class A<X, Y> {}  
class B<Z extends A<dynamic, Y>> {}

class TestA extends A<String, String> {}
class TestB extends B<TestA> {}

The immediate answer is that we can't do that because it's a compile-time error.

This is because Y in the declaration of B is an unknown identifier. We really want to have the type variable Y (it would be needed in the body of B), but we don't want to ask the "call site" to pass that type argument explicitly. One proposal in response to this request is that we could use type patterns (#170) and then bind a value to Y using a variant of pattern matching:

class A<X, Y> {}  
class B<Z extends A<dynamic, final Y>> {}

The classes TestA and TestB are unchanged.

However, pattern matching on types may be a complex feature. This issue offers a proposal for a simpler mechanism:

Proposal: Compute a type argument at a type

We introduce a built-in generic type ImplementsAtN for each natural number N (so we'll have ImplementsAt1, ImplementsAt2, and so on as needed).

This is a "magic" type, just like FutureOr and dynamic are types that we can't express using a Dart declaration. They are a built-in property of the language.

Let t be a term derived from <type> of the form ImplementsAtN<T, G> where T and G are derived from <type>.

A compile-time error occurs unless G is an identifier or a qualified identifier (like prefix.MyClass) that resolves to a generic type declaration. A compile-time error occurs unless G has N or more type parameters.

Finally, a compile-time error occurs unless T implements G.

When no error occurred we know that there exist actual type arguments S1 .. Sk such that T implements G<S1 .. Sk>. In this case, ImplementsAtN<T, G> denotes the type SN. For instance, ImplementsAt2<T, G> denotes S2.

Using the pseudo syntax we would write T@G.X rather than ImplementsAtN<T, G>, where X is the name of the N'th type parameter in the declaration of G. You could read this as follows: "Starting from the type T, search the superinterface graph to find a type S of the form G<...>. Assume that X is the name of the N'th type parameter of G. Then this term denotes the N'th type argument of S.

The compile-time subtype relationships for ImplementsAtN<T, G> are determined by computing the statically known value of the type denoted by this term.

This is a computation which is already done for member invocations. For example:

abstract class G<X, Y> { Y get g; }
abstract class C extends G<int, String> {}

void f<Z extends G<num, num>>(Z z) {
  ImplementsAt2<Z, G> y = z.g; // Pseudo syntax: "Z@G.Y y = z.g;"
  y = 1.5; // Error.
}

In this situation, ImplementsAt2<C, G> has the value String, which is the result we would also need to find in order to type x.g where x has type C. Similarly, ImplementsAt2<Z, G> is considered to be a fresh type variable Y extends num, and z.g is known to have return type Y. On the other hand, we can't know that ImplementsAt2<Z, G> is a supertype of double, so y = 1.5 doesn't type check.

At run time, the type denoted by ImplementsAtN<T, G> is the Nth actual type argument of the actual value of T at G. This determines the dynamic subtype relationships.

Optional Type Parameters

We could use this feature together with another new feature: Type parameters could be made optional by ending the type parameter declaration in = T where T is a type:

class A<X, Y> {}  
class B<Z extends A<dynamic, Y>, Y = ImplementsAt2<Z, A>> {}

This would make it possible to use B<SomeType> and have the second type argument computed as ImplementsAt2<SomeType, A>, but it would also allow B<SomeType, AnotherType>, as long as the declared bounds are satisfied (so we'd require SomeType <: A<dynamic, AnotherType>).

Usage

In order to address the original example, we first expand it slightly such that the type variable originally named Y is being used in the body of the class.

class A<X, Y> {
  final Y y;
  A(this.y);
}

class B<Z extends A<dynamic, Y>, Y> {
  final Z z;
  B(this.z);
  Y get g => z.y;
}

We can eliminate the type parameter Y and still preserve the desired typing as follows:

// A is unchanged.

class B<Z extends A> {
  final Z z;
  B(this.z);
  ImplementsAt2<Z, A> get g => z.y; // Pseudo syntax: "Z@A.Y get g => z.y;".
}

Expressive Power

This feature might appear to subsume an existential open operation. Similarly, it's worth considering whether we have the opposite relationship, namely that this feature might be subsumed by an existential open mechanism. Turns out that neither is true.

Here is the standard example where we assume that we have an existential open operation (using the syntax xs is List<final X>) which introduces a new type variable (or several) into a scope (here: X), and the evaluation of that operation will bind those type variables to the actual values:

void f(List xs, Object? o) {
  if (xs is List<final X>) {
    if (o is X) xs.add(o); // Accepted at compile time, safe at run time.
  }
}

The point in this example is that we have somehow lost information about the actual type argument of the list and the type of the object o (in this case it's just because we've used some overly general parameter types, but the same kind of situation arises in real life for much more complex reasons). Still, we are able to check whether or not it is safe to add that object to that list. In other words, xs.add(o) is guaranteed to succeed.

We could invoke f using f(<num>[1.5], 2) where add would be invoked, or f(<double>[1.5], true) where it would be skipped.

We could make an attempt to achieve the same level of safety using the mechanism proposed here:

void g<X extends List>(X xs, Object? o) {
  void h<Y extends List<Z>, Z>(Y xs, Object? o) {
    if (o is Z) xs.add(o);
  }

  h<X, ImplementsAt1<X, Iterable>>(xs, o); // Pseudo syntax: "h<X, X@Iterable.E>(xs, o);".
}

This would be equally safe as f in some ways: We could invoke g as g<num>(<num>[1.5], 2) (or we could use type inference, which would choose the same type argument) where add would again be invoked, or g<double>(<double>[1.5], true) where add would be skipped.

However, g<List<Object>>(<num>[1.5]. true) would invoke add, and it would throw. The reason for this is that the type argument List<Object> causes the list to be typed as List<Object>, which causes the value of Z in the invocation of h to be Object, and then o is Z is the same thing as o is Object, so we proceed.

The reason why the plain existential open operation is more powerful than this mechanism (for this purpose) is that the existential open operation allows us to denote the actual value of the type argument of xs, whereas the mechanism proposed here is able to look up the same kind of information in the type argument X, but there is no guarantee that X is the most specific type of the form List<S> such that the run-time type of xs is a subtype of List<S>. So we "may have the wrong S", and hence we can't establish a guarantee that the add operation will succeed.

(OK, even with the existential open the type system can't promise that it will succeed, but the semantics will actually provide the required guarantee as long as we don't assign a new value to xs or do other nasty things ;-).

Conversely, the existential open also doesn't subsume the mechanism proposed here:

(X, ImplementsAt1<X, Iterable>) withFirst<X extends Iterable>(X xs) => (xs, xs.first);

void main() {
  List<num> list = [1, 2.5];
  Set<String> set = {'a', 'b', 'c'};

  var (list2, i) = withFirst(list);
  var (set2, s) = withFirst(set);
}

This declares a function which accepts an iterable and returns a pair of the iterable itself and its "first" element. The crucial point is that we're able to use just one type argument (and we will in general be able to get a useful type argument from type inference), and we are also able to preserve the nature of the iterable (whether it's a List or a Set), and finally we're able to give the element a useful type (taken from the type argument of X at Iterable).

An existential open is an expression, and this means that it wouldn't be able to express signature-level dependencies like this.

So this illustrates that neither of these two mechanisms is subsumed by the other one.

Edits

• Oct 10, 2023: Added pseudo-syntax SomeType@SomeSuperinterface.ATypeVariable as commentary. This syntax may not fit well into the grammar (so we'll have to fiddle with it if we actually want to use it), but it is arguably more readable.

Start with the linked language discussion in issue 620 and the Dart specification section referenced by this proposal. Determine whether the ImplementsAtN semantics and optional type-parameter changes are accepted and where the specification should be updated; the issue names no implementation files or tests, so an agreed design is needed before coding.