dart-lang / dart-lang/language

Feature: Statically checked declaration-site variance

Open
#524 103 comments 260 reactions 1 assignee Claimed by @kallentu View on GitHub
dart-4.0 feature 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

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.