dart-lang / dart-lang/language
Feature: Statically checked declaration-site variance
- Dominant language
- TeX
- Stars
- 2.9k
- Forks
- 239
- Avg merge
- 2d 18h
- Merged PRs (30d)
- 14
Description
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 #213; the initial proposal for declaration-site invariance is #214. The initial proposal for the related feature known as use-site invariance is #229, and the corresponding tracking issue is #753.
Note that this issue does come up in practice. Here are a few examples gathered since April 2023. Many of them contain interesting discussions!
- https://github.com/dart-lang/sdk/issues/63960
- https://github.com/dart-lang/sdk/issues/62825
- https://github.com/dart-lang/sdk/issues/61814
- https://github.com/dart-lang/sdk/issues/61312
- https://github.com/dart-lang/sdk/issues/60742
- https://github.com/dart-lang/sdk/issues/60288
- https://github.com/dart-lang/sdk/issues/60009
- https://github.com/dart-lang/language/issues/4230
- https://github.com/dart-lang/sdk/issues/57799
- https://github.com/dart-lang/sdk/issues/57052
- https://github.com/dart-lang/sdk/issues/56231
- https://github.com/dart-lang/sdk/issues/55427
- https://github.com/dart-lang/sdk/issues/55321
- https://github.com/dart-lang/sdk/issues/55315
- https://github.com/dart-lang/sdk/issues/54439
- https://github.com/dart-lang/sdk/issues/54200
- https://github.com/dart-lang/sdk/issues/54122
- https://github.com/dart-lang/sdk/issues/54108
- https://github.com/dart-lang/sdk/issues/52168
- https://github.com/dart-lang/sdk/issues/52249
- https://github.com/dart-lang/sdk/issues/52826
- https://github.com/dart-lang/sdk/issues/52943
- https://github.com/dart-lang/language/issues/3156
- https://github.com/dart-lang/sdk/issues/53179#issuecomment-1674678378
- https://github.com/dart-lang/sdk/issues/53481
- https://github.com/dart-lang/sdk/issues/53523
- https://github.com/dart-lang/sdk/issues/33697
- https://github.com/dart-lang/language/issues/3380
- https://github.com/dart-lang/language/issues/3385
- https://github.com/dart-lang/core/issues/663
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` is a subtype of `C` whenever `T2` is a subtype of `T1`. Other subtype rules can then be used to show subtype relationships like `List <: Iterable` and `Map <: Map <: 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 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` or even a `List`, 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` is allowed to refer to a `List`) in return for accepting the potential dynamic type errors (a `List` _will_ work safely under the type `List` 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:
```dart
abstract class Good {
X get m1;
void set m2(Y value);
Z m3(List zs);
}
class Bad {
Y get m1; // Error.
void set m2(X value); // Error.
Y m3(List 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 <: C`; if `X` is marked `in` then `C <: C`. _Note that there is no subtype relationship between `C` and `C` 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:
```dart
class A {
X get m;
}
class B implements A {}
```
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.
Contributor guide
Assessment
This issue has not been assessed yet.