Look up a type variable at a given superinterface

[eernstg]

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.

[mateusfccp]

Although I feel #620 should be solved, I would rather have it solved by a simpler way.

First of all, I think Dart should walk in direction of a more consistent type system, not including new "special" types and, if possible, removing the old ones (for dynamic, we have #3192. For FutureOr, we could replace it with a language-level union type system, or even come up with another solution).

Secondly, I think this approach is quite confusing, and it's going to add unnecessary complexity to Dart.

I would rather have #170 implemented instead, even if it delays more.

[eximius313]

@eernstg,
I think I dont fully understand, so I want to ask:
why invent such constructs like:

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

or

  ImplementsAt2<Z, A> get g => z.y;

and not just treat X in:

class A<X> {}

the same as X in:

class B<Z extends A<X>> {}

?
I mean "everything right after < is declared type variable and it doesn't have to be very first <"

[eernstg]

@mateusfccp wrote:

I would rather have #170 implemented instead, even if it delays more.

This would cause a bigger delay because #170 is more complex than this feature. Basically, if we want to support type patterns (and that was part of the 'patterns' proposal for a while, but it was deemed too complex to be included) then we need to have all the capabilities associated with this proposal at first, and then some.

This also means that we could consider this proposal as a stepping stone to type pattern support.

I think this approach is quite confusing

It's about type level computations, and that's a more well-known concept in the functional programming community than in the communities of most other programming paradigms.

However, I'll try to present the idea in a way which may be more readable (especially from an object-oriented point of view). This syntax isn't what I would actually recommend as concrete syntax in Dart—the syntax I'm using here will probably break the grammar because of rampant ambiguities. However, I think it could be quite helpful in order to understand what's going on.

[Edit Oct 10 2023: This alternative syntax is now mentioned in the proposal, denoted as the 'pseudo syntax' because we don't yet have a set of working grammar rules for it.]

So let's think about a type T. Assume that T is an interface type (i.e., a class, mixin, etc, but not a function type, not void, not a bunch of other special types). Assume that G denotes a generic class/mixin declaration, and assume that G declares some type variables <X extends Iterable<X>, Y extends num>.

The proposed mechanism is then that we can write T@G.X to (1) use the type T, to (2) search the superinterfaces of T and find G, and then (3) look up the actual value of the type variable X which is declared by G.

So, for instance, we would be able to talk about the element type of a given list:

// An example using current Dart.
void f<X extends List<Y>, Y>(X xs, Object? o) {
  print('X: $X, Y: $Y'); // 'X: List<double>, Y: dynamic'.
  Y y = xs.first; // OK at compile time, and safe.
  if (o is Y) xs.add(o); // OK at compile time, throws.
}

// An example using the proposed feature, using the pseudo-syntax mentioned above.
void g<X extends List>(X xs, Object? o) {
  print('X: $X, X@List.E: ${X@List.E}'); // 'X: List<double>, X@List.E: double'.
  X@List.E anElement = xs.first; // OK at compile time, and safe.
  if (o is X@List.E) xs.add(o); // OK at compile time, and does not throw.
}

void main() {
  f(<double>[1.5], true);
  g(<double>[1.5], true);
}

A couple of crucial points:

• The invocation of f takes two type arguments, and we generally have to provide them explicitly because the second type argument would otherwise always be inferred as dynamic.
• The invocation of f throws, because Y differs from the actual element type of the list, it is just guaranteed to be a supertype (and add will check at run time whether the given object has a type which is a subtype of the element type of the list, and that fails when we try to add a bool to a List<double>). The type test o is Y is useless, because it means o is dynamic at run time, which is true no matter what.
• The invocation of g takes a single type argument. It is inferred as List<double> and this is actually sufficient to give the information that we wanted to provide using two type arguments in f. In the body of g we can denote the type argument of X at List using the syntax X@List.E (because the class List declares a type parameter named E).

We still have the property that it is safe to extract the first element of the list and store it in a local variable, but whereas the value of Y in f is dynamic, the corresponding term X@List.E in g has the value double. This means that the check o is X@List.E will actually detect that it isn't safe to add a bool object to this list, so we choose the else branch and there is no run-time error.

In short, g will help us maintain a non-covariant typing of the list, and we avoid having two type arguments (where nothing will stop us if we choose a too-general value for Y, and inference will always do just that).

Here is the example from the section 'Usage' again, using the pseudo-syntax:

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

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

Again, the point is that B needs two type arguments in current Dart, but only one type argument in this version using the new feature, and the type expression that denotes the actual type argument Z@A.Y is as precise as it can be, based on the structural contents of that type argument.

[eernstg]

@eximius313 wrote:

I mean "everything right after < is declared type variable and it doesn't have to be very first <"

That wouldn't be possible, because there are lots of situations where that term right after a < is not a type variable which is being declared at that point:

class B<Z extends A<int>> {}

In this case, we can't know whether int is supposed to be a reference to a type whose name is in scope, or it should be considered to be a fresh name for a type variable which is being declared (and that name will shadow an existing declaration which is being imported from 'dart:core`).

We could have a rule along the lines of "an identifier which does not resolve to a type declaration in scope is considered to be a fresh type variable", but that would be really error-prone:

class B<Z extends List<MaterialInputDefaultvalueAccessor>> {}

// That would be the same thing as this:
class B<Z extends List<X>> {}

In any case, support for type patterns is a bigger feature than support for looking up a specific type argument at a specific supertype.

[eximius313]

@eernstg ,

"an identifier which does not resolve to a type declaration in scope is considered to be a fresh type variable"

sounds perfectly reasonable (and I believe it's simmilar to what Java does). Why do you think that "that would be really error-prone"?

[eernstg]

The word MaterialInputDefaultvalueAccessor is very similar to the name of a class that might be in scope, so perhaps it wasn't intended to be a fresh type variable.

[eernstg]

I believe it's simmilar to what Java does

No, I'm afraid I'll have to disagree about that for several reasons.

Java generics are not reified, which means that Java could never support a mechanism whereby the actual value of a type argument is queried and the result is bound to a name in the program. So it can't possibly be similar to the mechanism proposed here.

In general, the bound of a type parameter is supposed to be a type (not a construct that introduces any new declared names, just a construct that specifies a type using names that are already declared somewhere else).

It is possible to use type variables in those types, but they must be defined in the same list of type variables.

// Java code, should go into two separate files.
public class A<X extends A<X, Y>, Y extends B<X, Y>> {}
public class B<X extends A<X, Y>, Y extends B<X, Y>> {}

This shows that it is possible for a bound like A<X, Y> to contain a type variable (such as X), but this is not because the type variable is being declared at that point, it is declared in the enclosing type parameter declaration (12 characters earlier, right after class A<), and this means that X and Y are in scope when we check the correctness of A<X, Y> as a bound.

[eximius313]

@eernstg, thanks for the explanation