Feature spec of explicit variance

[eernstg]

This is a first draft version of the feature specification of explicit variance support in Dart: (1) Explicit variance modifiers out/inout/in that generic type declarations can use on their type parameters, and (2) an explicit invariance modifier exactly on type arguments that client code can use in order to obtain statically safe use of legacy classes (using the current kind of covariance which requires dynamic checks).

It is rather permissive, in the sense that it allows for things like class B<out X> extends A<X> {} where A is a legacy class (say, class A<X> { foo(X x) {}}), which means that we can have a variable b of type B<num>, and we can call b.foo(1.23), and it will throw at run-time.

We could also say that the method foo is inaccessible in B (just like Java wildcards: we could "filter" out the part of the API whose member signatures violate the given variance). But I suspect that it will work better in practice to catch such cases with a lint.

Member declarations involving type parameters that have explicit variance modifiers are checked strictly (so class B<out X> { void foo(X x) {...}} is a compile-time error), but it is of course always possible to check such properties in the body and throw (void foo(Object? o) { X x = o as X; ...}), and, with that, I saw no reason to prohibit covariant parameters.

[leafpetersen]

Should there be a case here for when T is C<exactly B> and S appears in B?

[eernstg]

I do not think we should do that. It would imply that other type variables could not occur in B, and that's exactly one of the cases where exactly can be used on both the receiver type and the member signature to obtain a type with exactly known type arguments.

We would then rely on the erasure step to preserve soundness.

So, basically we would allow exactly even in the case where it is applied to a type in a member signature which is not known to be invariant, but then we're erasing it whenever we cannot show that it is invariant, when that member is used.

[leafpetersen]

What about the case that X does not occur in the RHS?

[eernstg]

So far we have considered such a type variable to have no variance. This may mean that no cases are applicable at some point during instantiation to bound, and this means that the i2b fails with an error. Dmitry put in an explicit representation of "not having any variance" in order to make it work this way. I think it's a meaningful choice, but we could of course switch over to use some default value for an unused type variable.

[leafpetersen]

Either way, this definition needs to account for it. As written, there's a contradiction between the parenthetical comment in the last sentence and the rest of the last sentence: the non-parenthetical part says "Otherwise we say that X is invariant", but the parenthetical part says "when X... occurs invariantly or both covariantly and contravariantly". The bi-variant case is covered by the first, but not the second.

[leafpetersen]

Do we need something around bounds? It feels like we should.

[eernstg]

I'm relying on existing checks for being regular-bounded / well-bounded.

Note that I removed the support for super bounds (lower bounds), which means that even an in type variable can only have an upper bound. That is still meaningful, because (e.g.) an instance method accepting an argument of type X (where we have the declarationin X extends T) still needs to be useful in the body of that instance method.

But what else do you think we should say about bounds here?

[leafpetersen]

I need to think about this more. It feels slightly risky to me (I think it's sound, but am not sure), and a little under-motivated. It would help to have some solid examples motivating why this is a useful feature to have (instead of just not allowing it at all).

[eernstg]

The main point is that it allows for exactly on a receiver type to propagate through a member access. So if Iterable<T>.toList() returns a List<exactly T> then the caller of toList can preserve the exact knowledge about the type argument with this rule, and otherwise there would be a downcast.

Added a comment to emphasize this point, just before the section Dynamic Semantics.

[eernstg]

Review response. Resolved several threads (please reopen if needed); a couple of threads are still open.

I haven't made any changes in the direction of supporting other variances than invariance in the use-site part, I'd expect that to be handled in another iteration.

[eernstg]

The main point is that it allows for exactly on a receiver type to propagate through a member access. So if Iterable<T>.toList() returns a List<exactly T> then the caller of toList can preserve the exact knowledge about the type argument with this rule, and otherwise there would be a downcast.

Added a comment to emphasize this point, just before the section Dynamic Semantics.

[eernstg]

So far we have considered such a type variable to have no variance. This may mean that no cases are applicable at some point during instantiation to bound, and this means that the i2b fails with an error. Dmitry put in an explicit representation of "not having any variance" in order to make it work this way. I think it's a meaningful choice, but we could of course switch over to use some default value for an unused type variable.

[eernstg]

I'm relying on existing checks for being regular-bounded / well-bounded.

Note that I removed the support for super bounds (lower bounds), which means that even an in type variable can only have an upper bound. That is still meaningful, because (e.g.) an instance method accepting an argument of type X (where we have the declarationin X extends T) still needs to be useful in the body of that instance method.

But what else do you think we should say about bounds here?

[leafpetersen]

We should probably make it explicit that this covers setters as well. Same for line 202.

[leafpetersen]

We also should make it explicit that covariant on a field covers the setter, but not the getter. So we have that:

class C<in T> {
   covariant C<T> f1; // Error, the C<T> appears in an invalid position in the getter
   final covariant C<T> f2; // Error as above
}

class D<out T> {
  covariant D<T> f1; // Ok: the getter is properly covariant, and the setter is covered by the covariant annotation.
}

cc @kallentu

[plammens]

With this specification, is there a way to manually "override" or ignore (in the sense of doing a dynamic type cast) a wrong in/out position?

For example, consider the following class:

class Filter<in E> {
  Filter(this.predicate)

  final bool Function(E) predicate;

  Iterable<E> apply(Iterable<E> items) => items.where(predicate);
} 

Ideally the type parameter should be contravariant, because a Filter<Fruit> should be a Filter<Apple>, because if the predicate accepts fruits it certainly accepts apples.
But as written above it would be illegal according to the spec because E appears in an out position in the return type of the apply method.

However, we know that the apply method will never alter the actual runtime type of the given elements, as it is just a filter, so indeed a Filter<Fruit> would return Apples with apply if you give it Apples, and not any other type of Fruit.
This is probably not something the type checker can determine, so, would there be a way of ignoring this illegal "out" position, allowing E to be contravariant?

---

With the current experiment enabled, I can get rid of this error by wrapping the return type of the method in a single-element record, but I doubt this is intended.

[plammens]

Also I think MyClass<SomeTypeArgument> should always be a subtype of MyClass<dynamic>, regardless of variance of the type parameter, because dynamic is not some kind of root supertype but instead it just means disable static type checking for this parameter.

With the current variance experiment, I can't assign for instance a Filter<int> to a Filter<dynamic>.

[lrhn]

because dynamic is not some kind of root supertype

It is, actually. The dynamic type is a top type, so it's a supertype of all Dart types.

If you have class Filter<in T> { void add(T value) {}}, and we allowed assigning a Filter<int> to Filter<dynamic>, then we get unsoundness:

var f1 = Filter<int>();
Filter<dynamic> f2 = f1; // Not allowed today, and isn't sound.
Filter<Object?> f3 = f2; // Definitely valid, not way to disallow.
Filter<String> f4  = f3; // Allowed because of contravariance.
f4.add("banana"); // Not sound.

The point of sound variance is to allow a call like f4.add("banana") to not do extra runtime type checks, because soundness ensures that any value assigned to Filter<String> will definitely accept a String as argument to add.

[plammens]

It is, actually. The dynamic type is a top type, so it's a supertype of all Dart types.

Yes, yes, my bad, I realized this later.

In any case the type system is still unsound because of covariant type parameters by default 😅