dart-lang / dart-lang/language

Feature: Sound use-site variance

Open
#753 7 comments 30 reactions 0 assignees View on GitHub
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 sound mechanism for use-site variance or invariance in Dart.

Background: The original request motivating this feature is #213; the initial proposal for use-site invariance is #229. The related feature known as declaration-site variance was initially proposed in #213, with tracking issue #524.

The text below describes properties of use-site variance 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`; in other words.

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.

Unsound covariance enables many software designs that would be rejected by a traditional sound 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 sound 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. It consists of two elements: Use-site invariance and declaration-site variance.

### Use-site Invariance

Use-site invariance can be used by developers who wish to maintain a sound and strict discipline on instances of classes that have unsoundly covariant type parameters.

Syntactically, use-site invariance consists in allowing actual type arguments in type annotations to be annotated with the modifier `exactly`, which eliminates covariance for that type parameter. For example:

```dart
main() {
bool b = ...;
List xs = b ? [] : []; // OK, `xs` is unsoundly covariant.
List ys = xs; // Requires downcast (with NNBD: must be explicit).
ys = []; // OK, statically safe.

xs.add(3.1); // No compile-time error, checked dynamically, throws.
ys.add(3.1); // No error, no dynamic check: Statically safe.
}
```

Here are some core properties of use-site invariance:

A type argument marked `exactly` yields a subtype. For instance, `List` is a subtype of `List`.

Every instance of a generic class is created with a type which is fully exact. That is, if `o` is an instance of a generic class `C` taking two type arguments then the dynamic type of `o` is `C` for some types `T1` and `T2`.

At run time, exactness of a type parameter is reified. That is, if `t1` is an instance of `Type` that reifies `List` and `t2` a `Type` that reifies `List` then `t1 == t2` must evaluate to false. Technically, this distinction is required in order to maintain sound information about type parameter exactness:

```dart
main() {
List> xs = [];
List> ys = xs; // OK, an upcast.
ys.add([]); // No compile-time error, but dynamic check.
xs[0].add(3.1); // Statically safe.
}
```

When `ys.add` is invoked it is necessary to perform a dynamic check (as always, because `ys` has an unsoundly covariant static type and `add` has a non-covariant signature). If the dynamic type of `ys` does not include the information that its type argument is `List` (that is, if it's just considered to be `List`) then the dynamic check would allow the actual argument (whose type is `List`). But then we would get a type error at run-time for adding `3.1` to `xs[0]`. We cannot allow that to happen, because `xs[0].add(3.1)` is a statically type safe expression.

In summary, use-site invariance can be used to pin down type arguments which are otherwise only known by an upper bound, due to unsound covariance. When the type argument is known exactly for a given object, method invocations can be checked and recognized as statically safe, which improves the statically known level of correctness, and allows for improved performance.

### Use-site Variance

Use-site variance is a more complex and expressive feature than use-site invariance, but the fundamental ideas are the same. The main difference is that use-site variance allows for quantifying over a set of type arguments for a type parameter which is invariant (that is, it is marked as `inout` in the class declaration), thus creating a supertype.

```dart
class C {
X x;
C(this.x);
}

C c = C(42); // OK, because `int <: num`.
var y = c.x; // OK.
void foo() {
c.x = 43; // Error, the setter `x=` of `c` cannot be used with covariant receiver.
}
```

Use-site variance offers a superset of the features offered by use-site invariance, so this mechanism
can also be used by developers who wish to maintain a sound and strict discipline on instances of classes that have unsoundly covariant type parameters.

Syntactically, use-site invariance consists in allowing actual type arguments in type annotations to be annotated with the modifiers `out`, which adds covariance for that type parameter; `inout`, which removes all kinds of variance; or `in`, which adds contravariance. For example:

```dart
main() {
bool b = ...;
List xs = b ? [] : []; // OK, `xs` is unsoundly covariant.
List ys = xs; // Requires downcast (with NNBD, the cast must be explicit).
ys = []; // OK, statically safe.

xs.add(3.1); // No compile-time error, checked dynamically, throws.
ys.add(3.1); // No error, no dynamic check: Statically safe.

// Using class C from the previous example.
C c = C(3.0); // OK.
var y = c.x; // Error, getter `x` cannot be used with contravariant receiver.
}
```

Here are some core properties of use-site variance:

A type argument marked `inout` yields a subtype. For instance, `List` is a subtype of `List`.

A type argument marked `out` or `in` can only be used where it does not contradict the declaration-site variance of the corresponding type parameter. When allowed, it creates a supertype. For instance, `C` is a supertype of `C` where `C` is declared as shown earlier.

Every instance of a generic class is created with a type which is fully exact. That is, if `o` is an instance of a generic class `C` taking two type arguments then the dynamic type of `o` is `C` for some types `T1` and `T2`.

At run time, the use-site variance of a type argument is reified. That is, if `t1` is an instance of `Type` that reifies `C` and `t2` a `Type` that reifies `C` then `t1 == t2` must evaluate to false. Technically, this distinction is required in order to maintain soundness; the example given for use-site invariance in the previous section can be reused (using the keyword `inout` rather than `exactly`), because use-site variance is a superset of use-site invariance.

In summary, use-site variance can be used to pin down type arguments which are otherwise only known by an upper or lower bound, and they can allow type arguments to vary even though they are declared as `inout`. When the type argument is known exactly for a given object, method invocations can be checked and recognized as statically safe, which improves the statically known level of correctness, and allows for improved performance.

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.