Feature: Statically checked declaration-site variance

dart-lang / language

Design of the Dart language

Other

2.65k stars 202 forks source link

Feature: Statically checked declaration-site variance #524

Open eernstg opened 5 years ago

eernstg commented 5 years ago

This is the tracking issue for introducing a statically checked mechanism for declaration-site variance in Dart.

Background: The original request motivating this kind of feature is dart-lang/sdk#213; the initial proposal for declaration-site invariance is dart-lang/sdk#213. The initial proposal for the related feature known as use-site invariance is dart-lang/sdk#229, and the corresponding tracking issue is dart-lang/sdk#753.

Note that this issue does come up in practice. Here are a few examples gathered since April 2023:

The text below describes properties of this feature which are good candidates for being adopted. Many things can still change, and a full feature specification will be written and used to manage the discussions about the final design.

Variance in Dart Today

As of Dart 2.4 or earlier, every type variable declared for a generic class is considered covariant. The core meaning of this is that a parameterized type C<T2> is a subtype of C<T1> whenever T2 is a subtype of T1. Other subtype rules can then be used to show subtype relationships like List<int> <: Iterable<dynamic> and Map<String, String> <: Map<Object, Object> <: dynamic.

This type rule is not sound; that is, in order to maintain heap soundness it is necessary to check certain types dynamically. This means that a program with no compile-time errors can fail with a type error at run time.

For instance, with the declaration List<num> xs and some expression e with static type num, it is necessary to check during evaluation of xs.add(e) that the value of e actually has the type which is required by xs: It is possible that it is a List<int> or even a List<Never>, and it would then be a dynamic type error if the value of e is a double, even though the expression had no type errors at compile-time.

Dynamically checked covariance enables many software designs that would be rejected by a traditional statically checked approach to variance (e.g., as in Java or C#). This allows developers to make a trade-off between more flexible types (e.g., a variable of type List<num> is allowed to refer to a List<int>) in return for accepting the potential dynamic type errors (a List<int> will work safely under the type List<num> in a lot of ways, just not all).

We want to enable a statically checked typing discipline for variance as well (rejecting more programs, but providing a compile-time guarantee against the run-time type errors described above). This feature is concerned with the provision of support for that.

Declaration-site Variance

Declaration-site variance can be used to declare a strict and statically checked treatment of variance for each type variable of a generic class.

Syntactically, declaration-site variance consists in allowing each type parameter declaration of a generic class declaration to include one of the following modifiers: out, in, or inout. We say that such a type parameter has explicit variance.

The use of type parameters with explicit variance in the body of the enclosing class is restricted. It is a compile-time error for a type variable marked out to occur in a non-covariant position in the signature of a member declaration; and for a type variable marked in to occur in a non-contravariant position. For example:

abstract class Good<out X, in Y, inout Z> {
  X get m1;
  void set m2(Y value);
  Z m3<U extends Z>(List<Z> zs);
}

class Bad<out X, in Y> {
  Y get m1; // Error.
  void set m2(X value); // Error.
  Y m3<U1 extends X, U2 extends Y>(List<X> xs); // Error.
}

Here are some core properties of declaration-site variance:

We obtain the following subtype relationships: Let C be a generic class with one type parameter X. Assume that S is a subtype of T. If X is marked out then C<S> <: C<T>; if X is marked in then C<T> <: C<S>. Note that there is no subtype relationship between C<S> and C<T> if X is marked inout, unless S == T.

A type parameter with explicit variance can be used in the specification of a superinterface. For example:

class A<out X, in Y, Z> {
  X get m;
}

class B<out X, inout Y, in Z> implements A<X, Y, Z> {}

Soundness is ensured via a number of rules like the following: It is a compile-time error if a type parameter X marked out occurs in a non-covariant position in an actual type argument for a superinterface D when the corresponding type parameter of D is marked out; and if X occurs in a non-contravariant position in an actual type argument for D when the corresponding type parameter is marked in; and if X occurs at all in an actual type argument for D when the corresponding type parameter is marked inout.

The interaction with dynamically checked covariant type parameters is similarly guarded: It is a compile-time error if a type parameter X marked out occurs in a non-covariant position in an actual type argument for a superinterface D when the corresponding type parameter of D has no explicit variance.

In return for all these restrictions, we get static safety: For a class where all type parameters have explicit variance, every (non-dynamic) member access which is statically type correct is also dynamically safe (no type checks on parameter types etc. are needed at run time).

In general, declaration-site variance can be used for classes which are intended to be strictly type checked with respect to variance everywhere.

eernstg commented 5 years ago

First draft of feature specification at PR dart-lang/sdk#557.

lrhn commented 5 years ago

The "exact" type already exists in Dart in certain places - the type of a literal or object creation expression may have an exact type, which is why List<int> l = <num>[1]; is a compile-time error instead of a run-time downcast failure. I assume those cases can be subsumed by exact types and still behave the same.

For use-site invariance, we will have both List<Foo> and List<exact Foo> as instantiations, with the latter being a subtype of the former. We don't actually introduce a nww type called exact Foo, just new syntactic forms for type arguments, and a suitably expanded type relation between instantiated generic types. We can say that we introduce exact Foo, but it's not a type, just a type pattern.

As stated, the type arguments can only be used in type pattern expressions (type annotations), not class expressions or literals. That is, you can write List<exact Foo> x; as a type annotation, but not class C extends Iterable<exact int> or new List<exact int>(). Those make no sense, they are always "exact" in that they are run-time invocations with a single value.

The following should be allowed:

List<exact String> foo(List<exact int> list) => (list..add(42)).map((x) => "$x").toList();

It is meaningful and useful.

What about:

class C<T> {
  List<exact T> mkList() => <T>[];
}

Is this meaningful? Maybe. If you have a C<num> c, then you only know that the result of c.mkList is List<num>. If you have C<exact num> d; then the static type of d.mkList is (or should be) List<exact num>. If the code had not written exact T in the return type, then it would not have been true. The method:

  List<T> mkList() => <T>[];

will never have a static return type of List<exact anything>, not even for D<exact num>.mkList().

So, we need some substitution rules for type arguments to make this work. exact T[exact S/T] -> exact S exact T[S/T] -> S T[exact S/T] -> S (?)

It also suggests that a lot of platform libraries should be changed to have exact in their return type, because they are really intended to be exact. Take: Set<T>'s Set<T> union(Set<T> other). Here we should make it Set<exact T> union(Set<T> other), so that if I have a Set<exact num> then the union returns another Set<exact num>. (I just realized that I have written exact instead of exactly everywhere. I'm not particularly fond of all these keywords, but shorter seems better :)

That suggests a migration issue. If we change some platform libraries to return, say, List<exact String>, then any existing implementation of the same interface will no longer be valid when it returns merely List<String>, a super-type of the required return type. We may want to have an NNBD-like migration process where legacy libraries are accepted for a while, until everybody has migrated.

If we need migration anyway, then we don't need to make the syntax backwards compatible, and we could do something else, like:

class C<+T , -S, =U> {  // out T, in S, inout U
   List<+T> mkList() => <T>[]; // not exact T
   List<U> mkList() => <U>[]; // exact U
}

We do get the inherent complexity of a two-tier type system where it matters whether you write exact int or int on every type argument in your API. You have to get it right, otherwise you make lock yourself out of possible later changes. If you say foo(List<exact num> arg) then you can't add elements to arg later, and you prevent anyone with merely a List<num> from calling you. They'll have to do list.cast<exactly num>() to convert their list.

I expect exact types in arguments to be rare (you really do need to do modification), and for them to be common in return types.

For declarations site variance, we already have something similar for function types. For those, the variance is automatically computable from the co-/contra-variance of the occurrences of the type arguments. We could do the same for class parameters, but that would break all our existing unsafely covariant classes. We could do it anyway, and require migration which would effectively mean that all existing type arguments become covariant, and we write an explicit covariant on all existing contravariant occurrences (well, the ones in parameters, we can't help the ones in function return types).

eernstg commented 5 years ago

The "exact" type already exists

Right. The notion of an exact type is not specified, but it is used in some cases by our tools (even to raise an error for certain "impossible" casts).

The notion of a type argument which is known exactly is a different concept (an object can have dynamic type List<exactly T> even though it is an instance of some proper subtype of List). I just checked the text above to make sure that it doesn't ignore that distinction, and adjusted a couple of sentences.

For use-site invariance, we will have both List<Foo> and List<exact Foo> as instantiations

Both of those are instantiations of the generic type List (where instantiation of a generic type means providing actual type arguments), but we will not have an object whose dynamic type is List<Foo>. If the dynamic type T of a given object o is such that List<Foo> is one of the superinterfaces of T then o has type List<exactly Foo>. In general, every type argument in the dynamic type of an object is exactly something, and the superinterfaces will carry this property with them.

class A<X, Y> {}
class B<X> implements A<X, int> {}

With that, B<String>() has dynamic type B<exactly String>, and it is also of type A<exactly String, exactly int>.

We may or may not want to let Type.toString() reveal this bit, but it must be present in the dynamic representation of types in order to maintain soundness.

we introduce exact Foo, but it's not a type, just a type pattern

I'd prefer to say that a type accepts type arguments, each of which may have the modifier exactly, which also implies that exactly Foo is not a type.

the type arguments can only be used in type pattern expressions (type annotations), not class expressions or literals.

exactly can be used on type arguments, e.g., <List<exactly num>>[], but not on types, and we need to make the distinction that "type arguments" given prescriptively are types. So List<exactly num> is OK as a type annotation, but List<exactly num>() as an instance creation is not, and <exactly num>[] is not; but when exactly is nested one level deeper then it is again a type argument, which is the reason why <List<exactly num>>[] is OK.

class C<T> {
  List<exactly T> mkList() => <T>[];
}

That can be allowed, and would be safe, but the computation of the member access type must take into account that the statically known value of T is just an upper bound.

main() {
  C<num> c = C<int>();
  List<num> xs = c.mkList(); // Static type of `c.mkList()` is `List<num>`.
  List<exactly num> ys = c.mkList(); // Error (downcast).
}

Of course, with class C<inout T> we would have an uninterrupted chain of exactness, and c.mkList() would have static type List<exactly num>.

we need some substitution rules

I believe the most straightforward way to get this right is to consider the types of member accesses, with a case for each variance of the type parameters of the class. Type parameters with no variance modifier are the most complex ones, of course, because they are allowed to occur in any position in a member signature.

We may want to have an NNBD-like migration process where legacy libraries are accepted for a while

Indeed.

we don't need to make the syntax backwards compatible

Right, but C<=X, -Y> x; may not be optimally readable (and in, out, inout isn't all that verbose). In any case, that's probably not more breaking than the keywords.

do get the inherent complexity of a two-tier type system where it matters whether you write exact int or int on every type argument in your API

I think that wouldn't ideally be such a common situation: The declaration site variance modifiers are required to match the usage (so if you have a type parameter out E then it just can't be the type annotation of a method parameter), and a subtype receiver will have a subtype member (including: less specific parameter types and more specific return types).

The use of exactly in a member signature would be specifically concerned enhancing the type safety in the management of legacy types (with type parameters that have no variance modifiers).

I would expect the reasonable trade-off to be somewhere between just using the legacy types as they are (with the current level of type safety, which has been used in practice for years without complete panic) and teasing out the very last drop of static type safety, by adding exactly as many places as possible. In any case, there are rules for eliminating exactly from interface type members such that the resulting typing is sound.

He-Pin commented 4 years ago

I more like the +T and -T syntax in Scala

He-Pin commented 4 years ago

The current in out looks like a primary student and verbose. Kotlin and C# is using in and out too，but reads badly.

leafpetersen commented 4 years ago

Is it the AUTHOR of the Bad class, or the USER of said class? Sure, user will benefit, too, if the author makes fewer mistakes, but other than that?

The primary beneficiary is the USER. The List class is one of the primary examples of something that should be invariant, but is instead unsoundly covariant. We have numerous users who are frustrated that this results in unexpected runtime errors that could have been caught at compile time. Enclosed below is an innocuous looking test program that fails at runtime instead of at compile time. Sound variance allows users who strongly prefer to rule these errors out at compile time to do so.

void addToList<T>(List<T> target, List<T> src) {
  for(var x in src) {
    target.add(x);
  }
}

void test(List<num> nums) {
  addToList(nums, [3, 4, 5]);
}
void main() {
  List<double> doubles = [3.5];
  test(doubles);
}

leafpetersen commented 4 years ago

Question 2: you seem to be leaning towards the use of "inout" as a synonym of "exact", but I have difficulty understanding the reasoning leading from "inout" to "exact".

Reading between the lines of this question, I think you are missing the primary effect of this feature, which is that it changes the subtyping relation between types. Describing inout as exact is sensible because given class Invariant<inout X> ... we know that any variable of type Invariant<num> contains only objects that were allocated as Invariant<num> or a direct subclass thereof. Specifically, it will never contain an Invariant<int>, nor an Invariant<Object>. In this sense then, it contains objects whose generic parameters are exactly as described by the type. Hence exact. Does that help?

mockturtl commented 4 years ago

Describing inout as exact is sensible

I think tatumizer is suggesting exact will make a better (easier to understand) syntax for invariance. (Compare: "let xy mean neither x, nor y.")

leafpetersen commented 4 years ago

I find the word inout confusing. It's difficult to see how this word may carry the meaning of "exact".

Ah, sorry, I misunderstood your question. Here's the intution:

a type variable labelled in may only be used to pass things in to methods
- void add (T x)
a type variable labelled out may only be used to pass things out of methods
- T get first
a type variable labelled inout may be used to pass things in to and out of methods
- T swap(T x)

Does that help?

(By the way, what combination of "in" and "out" characterizes the current default behavior in dart?)

Neither. Classes are allowed to use type variables everywhere in a method, which corresponds most closely to inout, but subtyping is covariant, which corresponds to out.

Let's consider your example with addToList. What will our new program look like to prevent this bad outcome? Where "in", "out" and "inout" should be added? And what line in the code will be flagged statically after we do these changes?

For completeness, here is the example rewritten to use an example of an invariant implementation of List. The call to test on the second line of main is statically rejected.

import 'dart:collection';

class Array<inout T> extends ListBase {
  List<T> _store;
  int get length => _store.length;
  void set length(int i) => _store.length = i;
  T operator[](int index) => _store[index];
  void operator[]=(int index, T value) => _store[index] = value;
  Array.fromList(List<T> this._store);
}

void addToList<T>(Array<T> target, Array<T> src) {
  for(var x in src) {
    target.add(x);
  }
}

void test(Array<num> nums) {
  Array<num> ints = Array.fromList([3, 4, 5]);
  addToList(nums, ints);
}
void main() {
  Array<double> doubles = Array.fromList([3.5]);
  test(doubles);
}

leafpetersen commented 4 years ago

@tatumizer I think this is getting a bit far afield - variance is definitely a confusing subject, but I don't think we're going to fix that here. Is it fair to summarize your general take here as being that you find + - = more intuitive than out in inout? Or are you expressing a preference for something different than that?

He-Pin commented 4 years ago

repeat the in 、out and inout here and there make me looks like a fool; why not make use of inputParameter T outputParameterR?

He-Pin commented 4 years ago

@leafpetersen I think the - and + style are more concise and the in and out style are more easy to understand.

Hixie commented 4 years ago

Having experienced this feature in Kotlin I strongly recommend we never go there. It is completely impenetrable to most developers. If you need to know type algebra to be able to use a feature then that feature doesn't, IMHO, belong in Dart.

leafpetersen commented 4 years ago

@Hixie Just to be sure we're on the same page: Kotlin has two different kinds of variance - this kind (declaration-site) which is what C# uses, and which I don't usually think of as requiring a lot of type algebra and use-site variance which is what Java uses, and which does require introduce some serious type algebra. And the combining the two, yeah, that gets pretty wild pretty quick. Are you specifically commenting on declaration site variance (marking type parameters classes as usable as in, out, or inout), or on the Kotlin style combination?

Hixie commented 4 years ago

The declaration-site version.

lambda-fairy commented 3 years ago

It looks like this has been implemented by @kallentu (behind an experimental flag):

https://medium.com/dartlang/dart-declaration-site-variance-5c0e9c5f18a5

eernstg commented 3 years ago

That is true, but parts of the implementation need to be updated (many other things happened in Dart since then), so there's some work to do before it is ready to be released.

Levi-Lesches commented 3 years ago

Hi, @eernstg + @leafpetersen, any updates on this? I see a lot of issues about variance-related problems a lot, and was wondering what the timeline could look like.

eernstg commented 3 years ago

No ongoing work on this right now, but the feature is certainly on the radar, and I'm not the only one who keeps wanting it. ;-)

Silentdoer commented 3 years ago

If this feature is implemented, List<T> will become List<inout T> in declare by default? it can use like following code: ?

List<out num> list = <int>[1,3,5];
// ok
var ele = list[0];
// compiler error
list.add(9);

lrhn commented 3 years ago

With declaration site variance, you can't write List<out num> list = .... That's use-site variance.

If List is declared as List<inout num> then it's invariant, so List<num> list = <int>[1, 3, 5]; would be a compile-time error.

It's undecided whether List can be migrated to List<inout T> or it has to stay the original unsafe List<T>. That depends on how migration will work, and how iteraction between old code and new variance declarations work, and whether we actually want to make List be invariant in practice.

We have a large number of old classes which were not designed with potential invariance in mind. (My personal worry is that we can't convert those to using variance without breaking a lot of code, not unless we introduce use-site variance as well).

Levi-Lesches commented 3 years ago

My two cents: Favor large breaking changes that make the APIs cleaner in the long run over smaller changes that ease migration. I specifically have Iterable.firstWhere and DropdownMenuItem.value in mind from null safety, which are harder to use now than they should be because they were made backwards-compatible in a time where devs were anyway going over their code to make sweeping changes. That and all the issues on here about bugs when running in mixed null safety mode, it sounds like for features as big as variance, they may just be worth a breaking version change (or if they're opt-in, no mixed mode).

List is obviously widely used, and it seems that modifying it in any way will cause breakage, but I'd rather lists be easier and safer to use in the future than worry about how to update existing apps to a new version of Dart (which is always going to take time and effort). Especially if having stricter variance can point out some potential problems during migration.

Silentdoer commented 3 years ago

I have another question, if List is List<inout T>, List can use covariant keyword in parameter? such as:(Suppose List is declared as List<inout T>)

// in class Fruit
void test(List<num> fruits) {
}

// in class Apple (extends Fruit)
@override
void test(covariant List<int> apples) {
}

lambda-fairy commented 3 years ago

@Levi-Lesches I can't speak for the Dart team, but I don't think that's practical with the sheer amount of code that's already written. At the scale we're working at – millions of lines of code – every change needs to be incremental and automated. Clean breaks simply aren't feasible.

Silentdoer commented 3 years ago

My two cents: Favor large breaking changes that make the APIs cleaner in the long run over smaller changes that ease migration. I specifically have Iterable.firstWhere and DropdownMenuItem.value in mind from null safety, which are harder to use now than they should be because they were made backwards-compatible in a time where devs were anyway going over their code to make sweeping changes. That and all the issues on here about bugs when running in mixed null safety mode, it sounds like for features as big as variance, they may just be worth a breaking version change (or if they're opt-in, no mixed mode).

List is obviously widely used, and it seems that modifying it in any way will cause breakage, but I'd rather lists be easier and safer to use in the future than worry about how to update existing apps to a new version of Dart (which is always going to take time and effort). Especially if having stricter variance can point out some potential problems during migration.

Agree, I sincerely hope that dart can have a clean, clear and consistent syntax

lrhn commented 3 years ago

@Silentdoer I'd say that the covariant example would not be allowed. The covariant keyword allows a parameter to (unsoundly) be a subtype of the superclass method's parameter. It's unsound relative to the covariant generics of the class. (Which is why it has to insert a run-time if (arg is! paremeterType) throw TypeError(...); check.)

If List (or any other generic class) is declared as List<inout T>, then it's invariant. That means that List<int> is not a subtype of List<num>.

On thing I don't know whether has been define yet is whether you can use covariant inside the class itself. Can List be declared as

abstract class List<out T> {
 T operator[](int index);
 void add(covariant T value);
 ...
}

The T in add occurs contravariantly, which is should be disallowed for a covariant ("out") type parameter. Does the covariant allow overriding that? And if so, would "class is covariant, every covariant occurrence in a parameter is covariant" be a compatible description of the current behavior? (It's not, we can also have contravariant type variable occurrences in return types).

Silentdoer commented 3 years ago

if List is declared as List<inout T>, List is implements Iterable;and if Iterable is declared Iterable<out T>, then List<inout T> implements Iterable<T> is allowed, right? Based on the above assumption, the following code is ok?

// in class Fruit, When calling it, the argument is List<Fruit> object
void test(Iterable<Fruit> fruits) {
}

// in class Apple (extends Fruit), When calling it, the argument is List<Apple> object
@override
void test(covariant Iterable<Apple> apples) {
}

lrhn commented 3 years ago

@Silentdoer It's not yet specified what happens to existing classes, or whether variance is applied implicitly. It may be possible to keep classes "unsafely covariant" (like now). If not, the List interface does have "out" uses of the type parameter, so if it must be variance annotated it'll probably have to be inout (unless we do something for the "out" uses like marking them covariant, and allowing that to keep breaking safety).

(There is no full spec for this feature yet, so some things are still undecided).

Silentdoer commented 3 years ago

@Silentdoer It's not yet specified what happens to existing classes, or whether variance is applied implicitly. It may be possible to keep classes "unsafely covariant" (like now). If not, the List interface does have "out" uses of the type parameter, so if it must be variance annotated it'll probably have to be inout (unless we do something for the "out" uses like marking them covariant, and allowing that to keep breaking safety).

(There is no full spec for this feature yet, so some things are still undecided).

thanks for your reply

eernstg commented 3 years ago

The feature spec proposal at https://github.com/dart-lang/language/pull/1230 does consider the use of the modifier covariant on an instance method parameter (see line 312 for an example), and I don't think we need to introduce any special rules about this modifier.

As @lrhn mentions, and assuming that the rules will be similar to that feature spec, we can't do covariant List<int> here, because List<int> is not a subtype and not a supertype of List<num>.

But this is fine, assuming class Iterable<out E> ...:

class Fruit {
  void test(Iterable<Fruit> fruits) {}
}

class Apple extends Fruit {
  void test(covariant Iterable<Apple> apples) {}
}

The semantics is unchanged: Apple.test must perform a dynamic type check on the actual argument, such that the type error of (Apple() as Fruit).test([Fruit()]) is detected.

However, I wouldn't actually expect class List<inout E> to happen, because that's a breaking change if there ever was one...

lrhn commented 3 years ago

However, I wouldn't actually expect class List<inout E> to happen, because that's a breaking change if there ever was one...

Well, only if we don't also introduce use-site variance as well, so you can write List<out num> numList = intList;. :imp:

Hixie commented 2 years ago

FWIW, I continue to think that the benefits here (more expressive language) don't outweigh the costs (more complicated language). The main thing driving me to this conclusion is that I've never seen a description of this feature (for any language that has it) that is clear and complete but doesn't use terms that require a background in type theory to understand (like "soundness" or "variance"). In contrast, for example, I can explain subtyping and even generics to someone who understands only imperative programming. Pattern matching makes sense to people once they can get past the size of the feature. Function calls are easy to explain. But covariance and contravariance and inout type parameters are things that for some reason I've never seen explained in such a way (and I've certainly never managed to explain it myself in such a way).

lrhn commented 2 years ago

The problem we have is that we don't have soundness. The reasoning behind that can be hard to explain, but it does bit people occasionally, and they do understand "unsound".

I'm not sold on declaration-site variance. (I honestly can't remember which is which of "in" and "out", I find Java's ? extends an ? super more readable, which is really scary!) It does provide a way to get soundness that we don't currently have, without the restrictions of simply being invariant.

But let's try an explanation, just for the challenge:

You understand subtyping, right? An int is a num. The reasoning behind subtyping is that a value of the subtype can be used everywhere a value of the supertype is expected. Anything you can do with a num, you can do with an int. Anything that needs a num can be given an int. This doesn't necessarily scale to larger types containing num or int, though. Take a List<num> vs. a List<int>. You can't safely use a List<int> everywhere you can expect a List<num>.

If you expect a List<num> and someone gives you a List<int>, and all you do is read from the list, then it's safe, because the list gives you an int out where you expect a num, and an int is safe where you expect a num. All is well.

However, if you expect to be given a List<num>, then you might try to add a num, even a double, to the list. When given a List<int>, that must fail, you cannot add a double to a List<int>, because then it's no longer a list of integers. A List<int> limits what you can put into the data structure in a way that a List<num> doesn't. It's the List<int> which expects an int, and you who must satisfy its expectation, not the other way around. That's why most programming languages do not allow a (mutable) List<int> to be used where a List<num> is expected. Dart does, and Dart class generics is unsound for precisely this reason.

The purpose of this feature is to mark generic type parameters, like the E in class List<E> ..., with either out, int or inout,
saying whether it's safe and sound to take values of the type out, put values of the type in, or even to do both. Then we change the subtype rules, so you can only use a MyClass<int> where a MyClass<num> is expected, or vice-versa, if that's actually sound.

For example, we can declare class Future<out T> with an out parameter. That would make Future<int> a valid subtype of Future<num>, meaning that a Future<int> can be used where a Future<num> is expected. All a future can do is to eventually provide you with a value of that type. The value comes out, and it being an int is fine when a num is expected.

And we can declare class Sink<in T> with an in parameter, because all you can do with the type is to call add to put values into the sink. If you expect a Sink<int>, someone giving you a Sink<num> is safe and sound, because you can still put int values into it. Then Sink<num> is a subtype of Sink<int>.

And class List<inout E> would ... just not be safe in either direction, so it would disallow you from using it incorrectly. If you expect a List<int>, the only type satisfying that would be an actual List<int>. Then List<num> and List<int> would just not be related to each other, and you can't assign one to the other. That would be a very big breaking change, and that's a reason we will probably keep the current "out + unsafe in" behavior as well, and let List keep being unsound. New classes can choose to use inout, but migrating old classes is going to be hard.

Hope it makes sense. No use of "covariance" or "contravariance" :)

Levi-Lesches commented 2 years ago

In addition to "covariant/contravariant" and "in/out" language, which may be new concepts to many, it can also be explained in terms of and "supertype/subtype". I'll adapt @lrhn's explanation but replacing in with super, out with sub, and inout with exact (I know this conversation has been had before so I'm not necessarily advocating for using these keywords, just the ideas for use in the documentation):

Subtyping is relatively straightforward: you declare class A extends B to make A a subtype of B. Subtypes are just another way of saying "A is a type of B". An int is a type of num. Now you can use the subtype anywhere the supertype is expected: anything you can do with a num you can do with an int, and anything that needs a num can be given an int.

This doesn't necessarily scale to larger types with generics, though. Compare a List<num> to a List<int>. You can't safely use a List<int> everywhere you can expect a List<num>. If you expect a List<num> and someone gives you a List<int>, then you can safely read values from the list, since an int can always be used in place of a num. However, if you try to add a num (like a double), to a List<int>, that will fail since it's no longer a list of integers.

The purpose of this feature is to mark generic type parameters as either sub, super, or exact, which denotes which types are safe to use. For example, class Future<sub T> means a Future<int> can be used wherever a Future<num> is expected. This is safe since all a future does is provide a value and we know an int is always safe to use when a num is expected (because it's a subtype).

Conversely, class Sink<super T> means you can use a Sink<num> when a Sink<int> is expected (remember, num is a supertype of int). That's safe since all anyone can do is add ints to it, and we know an int is always safe to use when a num is expected. However, you cannot use a Sink<num> in place of a Sink<int>, since that would allow you to add a double to a collection of ints.

But there are some cases where you can't accept a subtype or a supertype. Think back to List. If we used class List<sub E>, then someone could use a List<int> instead of a List<num>, but that would mean you can no longer add other types of nums to the list, like a double. If we used class List<super E>, then someone could use List<num> instead of a List<int>, which means they could give a double when an int is expected. This is where exact comes in: class List<exact E> would only allow you to use the exact type, so List<int> means List<int> and List<num> means List<num>. This allows users to safely put values in the list, while also allowing them to safely read values from this list.

Hopefully, this doesn't use any language or concepts that are too complex. IMO, this level of detail is something I could reasonably expect to see in a Medium article or in the dart.dev documentation. Granted, in/out/inout does give a level of intuition that makes it easy to reason about the flow of types in your programs, but the supertype and subtype logic can be explained without introducing any new ideas.

Quijx commented 2 years ago

I think these explanations are great and the average dart user is able to understand the use of in, out and inout (or whatever they will be named) after reading them. However I believe that one does not even need to understand them to use and benefit from this feature. For example if someone tries to return a generic type that is declared in, the compiler will complain. And as long as the message is something helpful along the lines of

The generic type T is declared in and can therefore only by used as a method argument to be passed into the class. Mark it as inout to allow it as a return type.

, the user could just blindly follow the instruction and usually get what they want and also what is the correct behavior.

Users may not always know ahead of time if the type should be in, out or inout, but they know what types they want to return or use as parameters.

Likewise if a generic type is declared for example inout but the class only uses that type as return type, the analyzer could show a warning:

The generic type inout T is only used as a return type and should therefore be declared as out T.

And again, just blindly following that instruction usually yields the correct result.

lrhn commented 2 years ago

Just to nitpick myself: Future cannot be declared as Future<out T> because ... Future<num> f = futureOfInt; (await futureNum.asStream().toList()).add(3.14); creates an List with the same type as the future, and List cannot be declared as covariant. (And out T declaration means that T can only soundly be passed as argument to other out T type parameters.)

That very much makes me worry that declaration-site variance will never be able to apply to even the most obvious of existing types. If it cannot apply to Iterable or Future, the two most covariant types I can think if, what is left? If we cannot variance-annotate the platform libraries, and have to keep them unsafely covariant, then any soundness other classes build on top of that will be on a shaky foundation.

(At least for List, we can do abstract class List<out E> ... { void add(covariant E element); ... }. That moves the unsoundness from the class itself to only the unsafe methods. Can't do that for Future.asStream since covariant only works for parameters, not return types. Or we can just let list stay unsafely covariant, and allow any type variable to be used in an unsafe position.)

eernstg commented 2 years ago

Future cannot be declared as Future<out T>

This is a known issue: Soundness of the api of a class like Future does not magically extend to soundness of types used in the instance member signatures of said class, or types reachable through two or more such steps.

So if C uses dynamically checked covariance of its type parameter in a member m then an instance of C will potentially throw when m is invoked, because one or more typing requirements fail to be satisfied. In particular, a list may throw when add is invoked, because that method uses the type parameter E as the type of its actual argument, and E has no explicit variance (so it's the old-fashioned kind of covariant where soundness is enforced by dynamic checks), and this is true no matter how we got hold of that list.

Let's assume that List won't be changed to class List<inout E> ... (which is basically a given). In this situation we need to support a use-site mechanism in order to impose sound usage. Use-site invariance is a minimal model which will enable this kind of post-hoc static soundness for classes where dynamically checked covariance is still used:

void main() {
  List<exactly num> xs = [1];
  // xs = <int>[2]; // Compile-time error.
  xs[0] = 1.5; // Statically checked, will never give rise to a type error at run time.
}

So we can keep List and other widely used classes unchanged (to avoid the massive breakage), and we can still introduce statically checked variance at each usage point by using an invariant type.

This is more verbose, and it is less convenient than having a class List<inout E> ... in the first place, but it does allow for the static soundness to be introduced gradually. Note that we can perform tests like if (myList is List<exactly T>) ... for any given T, which will allow us to safely confirm (or disprove) invariance, even in the case where a list has been obtained with the type List<S> for some S (which could be any supertype of T). This is helpful in the situation where the invariant treatment of lists has been introduced in parts of a system, and not in other parts.

leafpetersen commented 2 years ago

But covariance and contravariance and inout type parameters are things that for some reason I've never seen explained in such a way (and I've certainly never managed to explain it myself in such a way).

Nonetheless, people seem to manage to use Kotlin, Java, C#, Rust and many other languages which have variance.

I do understand the concern, but I do not agree with the conclusion. Variance is hard, but it's a fact of life - it's just a mathematical property of the underlying structures that they behave that way. You can pretend otherwise, but that just pushes the problem off to runtime. So, you can deal with it statically, or you can deal with it at runtime. It's not clear to me that the runtime error there is any easier to explain, and it's certainly harder to debug and fix.

In general, most programmers most of the time won't need to deal with variance, just as they most of the time don't need to now. But the inability to actually express the correct variance in the cases where you need to is a major shortcoming in the language.

I'll also note that this comes up whenever I talk to people about Dart in the context of education.

munificent commented 2 years ago

In contrast, for example, I can explain subtyping and even generics to someone who understands only imperative programming.

My experience is that you can correctly explain a subset of subtyping and generics to someone who understands only imperative programming, but that many programmers don't fully grok it and yet are able to program profitably most of the time. Many times in my life, I have had to explain the difference between virtually-dispatched overriding versus statically-dispatched overloading in C++/C+/Java to programmers that are otherwise quite sophisticated.

Once your language has function types, you are in a world of contravariance and covariance whether you want to be or not. Many programmers can program just fine using first-class functions and static types without ever realizing that return types are covariant and parameter types are contravariant. By the same token, many programmers can use generic types correctly that have declaration-site variance without fully understanding what those annotations do.

Dart already forces users to deal with variance. Variance is in the language and always has been. All generics are covariant. Users may not know that Dart has covariance, but they will find out the hard way the first time they accidentally write code like:

List<Object> things = <String>[];
things.add(123);

The only thing Dart currently lacks is the ability for a generic class to request anything other than covariance and the ability to ensure that a class's variance is statically correct.

eernstg commented 2 years ago

I think sound declaration-site variance can have an effect on Dart software development which goes considerably beyond actively writing variance modifiers.

First, if someone else knows exactly how to use this mechanism, and they use to improve the type safety properties of a library that I'm importing, then my code can be safer than it would otherwise have been, and I don't have to write any variance modifiers at all.

As @leafpetersen mentioned, the underlying type structure is just a fact of life, but this means that it is possible to benefit from the improved type safety without worrying too much about exactly why the type safety has improved, and then we can proceed to an active use of the mechanism more gradually.

I liked the explanations about variance where the focus is on "input" and "output", but it is also possible to take a different path which is basically relying on feedback from the type checker:

Let's assume that we have a class C with a type parameter X which is legacy (that is, it has no variance modifier).

Try to change X to out X. If there are no compile-time errors then C is already safe, and you're done. This simply means that we're adding an explicit marker for the static type safety which was already there.

On the other hand, if there are compile-time errors then C uses X in certain ways that aren't statically safe. One way ahead is to change X to inout X. This means that X can be used safely anywhere in the class body, but clients of the class will pay, because they will have to live with a more rigid rule for assignability (C<num> c = C<int>(); used to be OK, but now we must use the same type argument, C<num> c = C<num>();).

Finally, the in modifier can be used to improve on the flexibility of the class in the very special case where X is only used for "in"put (that is, mainly, as the type of method parameters).

I think there are many, many ways to approach any complex topic, and we've looked at several of them in this discussion. The point is that the mechanism itself is technically well justified, and we have a bunch of ways to get to know how it works, and then we will develop a community awareness of how to deal with it every day.

modulovalue commented 2 years ago

Hixie wrote:

I continue to think that the benefits here (more expressive language) don't outweigh the costs (more complicated language).

leafpetersen wrote:

But the inability to actually express the correct variance in the cases where you need to is a major shortcoming in the language.

I think Hixie makes a valid point. Soundness is great, but even the most expressive language is of no use if it isn't able to attract and keep any new users. The reality is that Python and JS are the most popular languages and not Coq so any move away from Completeness towards Soundness carries the risk of alienating some new and existing users.

One of the core abstractions of Flutter is a 'Widget' where many different types are treated as a Widget and Flutter throws at runtime if misused. Awful Soundness-wise, but a good abstraction for making Flutter extremely easy to learn and attracting a lot of users. I think that it would be a mistake to assume that Soundness is always just 'better'.

I'm very excited about this feature, but It seems like efforts should be made to not overwhelm users of Dart that aren't ready for it so perhaps:

make it clear that it is an optional! and advanced feature that offers users the ability to give the compiler more information for easier maintenance of larger applications.
maybe even explicitly forbid introductory documents on https://dart.dev/guides and https://docs.flutter.dev from using explicit variance annotations unless it is absolutely necessary?

fweth commented 2 years ago

Would it be hard to restrict dynamic type checking to type casting via as? So that I know that the type system is statically sound in principal, but whenever I tell Dart "here, take this thing, and I promise, it is of type X" I know that the static type checker is no longer responsible to know the actual type of X? Or something like PureScript's unsafePartial?

The reality is that Python and JS are the most popular languages and not Coq so any move away from Completeness towards Soundness carries the risk of alienating some new and existing users.

Maybe I'm the exception here, but I use a lot of JS, yet when I do something more complicated, I want to use a statically typed language. I tried TypeScript but ran into an unsoundness issue on day 1 and didn't like it. So for me it would be very attractive, if some language offers me a statically sound alternative to JS, as I already have JS if I want to use no types and TS if I want to sprinkle some types on my JS code without going fully sound.

eernstg commented 2 years ago

Would it be hard to restrict dynamic type checking to type casting via as?

That is not possible unless we add a more sophisticated way to denote types (we'd basically need an 'existential open' operation). The problem is, by example, that if you have a list xs with static type List<T> and you want to add an element of type S, checking S <: T is not sufficient in order to ensure that there will not be a run-time type error.

void main() {
  List<num> xs = <int>[]; // `T` is `num`.
  xs.add(1.5); // `S` is `double`, so `S <: T` is true. Throws anyway, because `double <: int` is _not_ true.

  // A hypothetical extension supporting an 'existential open' operation could be used.
  final List<final X>() ys = xs; // Binds `X` to the dynamic type argument `int`.
  if (1.5 is X) ys.add(1.5); // Safe, doesn't add anything in this case.
}

If we add support for sound declaration-site variance then the author of a class can mark its type variables as covariant, contravariant, or invariant, and this will ensure soundness. In cases where we can't change a class to do this (say, List), we could use use-site invariance to make each list-typed variable safe (as if the type parameter of List had been invariant).

I believe that it's more helpful to allow program elements to be expressed in a typesafe manner, even in the situation where we improve some program elements and leave others unchanged. A program with explicit casts (if we can even write them) isn't going to be any safer, and it isn't going to be possible for a developer to mentally ascertain that the casts won't fail (because that would involve undecidable questions, which is also the reason why we can't ask a type checker to establish the safety or non-safety of these casts).

munificent commented 2 years ago

The reality is that Python and JS are the most popular languages and not Coq so any move away from Completeness towards Soundness carries the risk of alienating some new and existing users.

Python and JS aren't great comparisons since they don't have any types at all. If you don't like types to begin with, you aren't gonna like types regardless of how simple or complex they are. Looking at other statically typed languages, C++, C#, Java, Scala, Kotlin, and Swift all have sound variance for generic types as far as I know. (There are a couple of tiny edge cases like the null hole in Java wildcards, but that's essentially a bug.)

iazel commented 1 year ago

Thanks everyone for working on this proposal. I honestly hope it will go through soon.

I understand the concern that some may have about restricting what you can do, but I think we can all agree how awful it is to have a false sense of correctness. Plus, this is more of an opt-in feature, most of the time you don't even need to know about it, but it does make a difference for those little cases when you need it.

eernstg commented 1 year ago

I think it's worth noting that we can already emulate invariance if we are willing to pay a small extra cost at run time (because the invariant type variable is represented as two type variables), and if we are willing to deal with error messages where the emulation is revealed (which means that they are more complex to read and understand, because they are basically revealing some implementation details).

Assume that we want to model the following class hierarchy (where invariant type variables play an important role because type inference will otherwise very easily create a setup that causes run-time type errors to occur). Here is a version that relies on invariance as a proper language mechanism:

// Library 'result.dart'.

abstract class Result<inout T, inout E> {
  const Result();
  Result<T2, E> andThen<T2>(Result<T2, E> Function(T) f);
  Result<T2, E> map<T2>(T2 Function(T) f);
  Result<T, E2> mapErr<E2>(Result<T, E2> Function(E) f);
}

class ResultOk<inout T, inout E> implements Result<T, E> {
  final T value;
  ResultOk(this.value);
  Result<T2, E> andThen<T2>(Result<T2, E> Function(T) f) => f(value);
  Result<T2, E> map<T2>(T2 Function(T) f) => ResultOk(f(value));
  Result<T, E2> mapErr<E2>(Result<T, E2> Function(E) f) => ResultOk(value);
}

class ResultErr<inout T, inout E> extends Result<T, E> {
  final E error;
  const ResultErr(this.error);
  Result<T2, E> andThen<T2>(Result<T2, E> Function(T) f) => ResultErr(error);
  Result<T2, E> map<T2>(T2 Function(T) f) => ResultErr(error);
  Result<T, E2> mapErr<E2>(Result<T, E2> Function(E) f) => f(error);
}

Here is an example where the Result class hierarchy is used:

void main() {
  final ok = ResultOk<int, String>(10);
  final res = ok.andThen<String>((n) {
    if (n.isEven) return ResultOk(n.toString());
    return ResultErr("not even");
  });
  print('Result type: ${res.runtimeType}');

  // Invariance is enforced statically:
  // Result<num, Object> superTyped = ok; // Compile-time error.
}

However, the same example will also work with the following emulation of invariance. The main point is that every invariant type parameter gets an extra phantom type parameter which is used to maintain the invariance constraint (so class C<inout X> ... is expressed as class C<X, X2> .... The newly added type parameters will always have the value T Function(T) when the original type parameter has the value T (so we will only have C<T, T Function(T)> ..., never something like C<T, S> where S is different from T Function(T)).

Clients will not see the extra type arguments (and they won't get an opportunity to get them wrong), because we use type aliases to access the classes. So class C ... is renamed to class _C ..., and then we add typedef C<X> = _C<X, X Function(X)>;.

In this particular example we have two invariant type parameters, and we're collapsing the extra type parameters such that we can enforce invariance for two type parameters using just one extra type parameter. The extra one will then have the value (T1, T2) Function(T1, T2) in the case where the original type parameters have the value T1 respectively T2.

// Variant of library 'result.dart' where invariance is emulated.

typedef Result<T, E> = _Result<T, E, _Inv<T, E>>;
typedef ResultOk<T, E> = _ResultOk<T, E, _Inv<T, E>>;
typedef ResultErr<T, E> = _ResultErr<T, E, _Inv<T, E>>;

typedef _Inv<T1, T2> = (T1, T2) Function(T1, T2);

abstract class _Result<T, E, Invariance extends _Inv<T, E>> {
  const _Result();
  Result<T2, E> andThen<T2>(Result<T2, E> Function(T) f);
  Result<T2, E> map<T2>(T2 Function(T) f);
  Result<T, E2> mapErr<E2>(Result<T, E2> Function(E) f);
}

class _ResultOk<T, E, Invariance extends _Inv<T, E>> implements
    _Result<T, E, Invariance> {
  final T value;
  _ResultOk(this.value);
  Result<T2, E> andThen<T2>(Result<T2, E> Function(T) f) => f(value);
  Result<T2, E> map<T2>(T2 Function(T) f) => ResultOk(f(value));
  Result<T, E2> mapErr<E2>(Result<T, E2> Function(E) f) => ResultOk(value);
}

class _ResultErr<T, E, Invariance extends _Inv<T, E>> implements
    _Result<T, E, Invariance> {
  final E error;
  const _ResultErr(this.error);
  Result<T2, E> andThen<T2>(Result<T2, E> Function(T) f) => ResultErr(error);
  Result<T2, E> map<T2>(T2 Function(T) f) => ResultErr(error);
  Result<T, E2> mapErr<E2>(Result<T, E2> Function(E) f) => f(error);
}

Thanks to @iazel for coming up with this example!

Hixie commented 1 year ago

But covariance and contravariance and inout type parameters are things that for some reason I've never seen explained in such a way (and I've certainly never managed to explain it myself in such a way).

Nonetheless, people seem to manage to use Kotlin, Java, C#, Rust and many other languages which have variance.

I hope our bar is higher than "manage to use", though. Dart is a significantly easier language to use than Kotlin, and Rust, and APL, and many other languages that have lots of wonderfully powerful yet difficult to explain features, largely because it doesn't have those features. I would hate for us to throw away our advantage because we wanted to add some expressiveness that costs more than it is worth.

I do understand the concern, but I do not agree with the conclusion. Variance is hard, but it's a fact of life - it's just a mathematical property of the underlying structures that they behave that way. You can pretend otherwise, but that just pushes the problem off to runtime.

There's lots of things we push to runtime because it makes the language easier to use. Memory management, for example. That isn't intrinsically bad. It's a trade-off.

So, you can deal with it statically, or you can deal with it at runtime. It's not clear to me that the runtime error there is any easier to explain, and it's certainly harder to debug and fix.

That's not at all obvious to me. I think we should test this assumption with some usability tests.

In general, most programmers most of the time won't need to deal with variance, just as they most of the time don't need to now. But the inability to actually express the correct variance in the cases where you need to is a major shortcoming in the language.

I literally cannot think of a time where I have wished the language had this feature, and I've been writing Dart more or less non-stop for 7 years now. How are we determining that it is a major shortcoming?

lrhn commented 1 year ago

The one case where I have wanted declaration-side contravariance is StreamTransformer. (Which should probably not have been an interface to begin with, it's just a single function type, the cast is only there to make up for the lack of correct variance.)

There are other interfaces which could be contravariant, like Sink or StreamConsumer, but those are rarely a problem, because you never use them in a way where you're likely to up-cast ... I'm guessing, all I know is that they've never really been a problem. The StreamTransformer is used that way, because it also has a covariant type parameter, and you want to connect multiple transformers.

The place where unsound covariance is biting people in practice tends to be up-casting collections, List<num> numList = <int>[1]; numList.add(3.14);. This gives no warnings and causes a runtime error.

If the goal is to prevent runtime type errors, then we must prevent this code. One way to do so is to make List invariant.

That's hard to sell. The other option is use-site variance modifiers, which makes invariance easier to work with by allowing "partial up-casts", so you can write List<? extends num> someNumList = <int>[]; but then it prevents you from calling add because the type parameter occurs contravariantly in that signature.

(If we get declaration-site variance, we should be able to make Iterable and Future be covariant. Those are inherently covariant containers, which only provide values. But their APIs have pitfalls that make it hard to be soundly covariant.)

eernstg commented 1 year ago

I think it's fair to mention that use-site variance is a rather complex mechanism. With Dart, I believe that we can use a much simpler mechanism, and get the same improvement of type safety in the vast majority of situations where we would otherwise have used the more complex use-site variance mechanism.

We have a proposal for use-site invariance, dart-lang/sdk#229, which is a lot simpler than use-site variance. The point is that you can declare in a type annotation (say, the type of a variable or a parameter) that the type argument is exactly as stated, and not a subtype:

void main() {
  List<exactly int> xs = [1, 2, 3]; // `xs.add` is safe.
  xs.add(1); // OK.
  xs.add(3.14); // Compile-time error.

  List<exactly num> ys = xs; // Compile-time error.
  ys = xs as dynamic; // Run-time error, `exactly` is enforced at run time.

  // Here's the reason why we'd use `exactly` in the first place.
  List<num> ys = xs; // Allowed, but `ys.add` is now unsafe.
  ys.add(3.14); // OK at compile time, but throws at run time.
}

eernstg commented 1 year ago

tl;dr Main points use a bold font rd;lt

@Hixie wrote:

How are we determining that it is a major shortcoming?

I'm genuinely surprised that we have so few reports about these run-time type errors that could have been detected at compile-time: It has been known since 1980 or so which kinds of variance are statically safe (and this paper from 1989 is all about that question).

Still, Dart was designed to allow some unsafe declarations and expressions to be compiled (with a type check at run time), explicitly based on the rationale that this would keep the type system simpler.

So we could just conclude that it's not a major shortcoming, developers are happy, and users don't encounter a huge number of apps crashing because of run-time type errors. Done!

However, I tend to conclude that the current design is useful, and in particular that it is a useful trade-off in a large majority of the Dart software which is actually being written.

Some specific kinds of software tend to have more serious conflicts with this trade-off. In particular, code which is written in a more functional style may give rise to type parameters that need to be treated as contravariant or invariant, because the default (and currently unavoidable) covariant treatment is wrong all the time.

A very typical example comes up when a first class function is stored in an object, that is, when there is an instance variable whose type is a function type, and that function type contains type variables declared by the class.

Some examples: https://github.com/dart-lang/sdk/issues/36800, https://github.com/dart-lang/sdk/issues/48108, https://github.com/dart-lang/sdk/issues/48738, https://github.com/dart-lang/sdk/issues/49419, https://github.com/dart-lang/language/issues/3007, https://github.com/dart-lang/sdk/issues/52168.

Here is the core structure some of those examples:

class A<X> {
  final void Function(X) f;
  A(this.f);
}

void main() {
  A<num> a = A<int>((i) {});
  a.f(1); // Throws.
}

In the class A, X should be contravariant. This means that we should have A<num> <: A<int>, but we actually have A<int> <: A<num>, and there's an imminent danger of a run-time error if we ever use it. We miss out on the safe flexibility (it would be safe to allow A<int> a = A<num>((n) {});), but we are given the flexibility in the opposite direction (where every use of a.f will throw at run time). So we can do the wrong thing, but we're not allowed to do the correct thing.

I think sound variance can be used by designers of highly visible and widely shared code to give other developers the correct kind of flexibility (and avoid the unsafe kind), especially if they wish to use a style where first-class functions play an important role.

The rest of the world can continue to use dynamically checked covariance because it works quite well, and one generally doesn't even have to notice why certain constructs involving a class with a different variance is accepted or causes a compile-time error, we will just enjoy the fact that our code is now safer, even though we may not ever have written inout/in/out on any type parameter.

I believe that sound variance can help the community write safer code, and this can happen even if most developers haven't been thinking about sound variance at all. Over time we'll see how widespread the use of sound variance is; the main point is that it isn't a problem if it turns out to be used by somewhat specialized developers, and most of the Dart software out there continues to use dynamically checked covariance.