Use-site Invariance

In response to #213, this issue is a proposal for adding _use-site invariance_ to Dart.

[Edit: Note that more recent discussions have typically used the syntax `List` where this proposal had `List`. Adjusted the text below to fit that.]

## Introducing Use-site Variance

(You can safely skip to the next section if you already know about use-site variance.)

Use-site variance is known from languages like [Java (using `? extends` and `? super`)](https://docs.oracle.com/javase/tutorial/extra/generics/wildcards.html) and [Kotlin (using `in` and `out`)](https://kotlinlang.org/docs/reference/generics.html#type-projections)), and the general idea is that each type parameter of a generic type annotation (e.g., the type of a variable or a formal parameter, or the return type of a method) may have an associated variance.

For instance, with a Java class declaration like `public class Foo {...}`, it is possible to specify that a given variable `foo` has a declared type like `Foo`, which makes it possible for `foo` to contain a reference to an instance of `Foo` for any `T` which is a subtype of `Number`. (If we had used a plain `Foo` then the variable would only be allowed to refer to an instance of `Foo`, not `Foo` etc).

In return for the added flexibility, usages of `foo` can only use a part of the public interface of `Foo`: A member can only be accessed if its type is such that `X` never occurs in any position that is not covariant. In particular, if `Foo` declares an instance method `void bar(X x)` then `foo.bar(...)` is a compile-time error (it does not matter what `...` stands for, it's always an error), because `bar` is not in the accessible subset of the members of `Foo` for a variable like `foo`.

The basic idea is that we'll "filter" the members in the static type of the receiver, and only allow access to those members that satisfy some extra constraints. This filtering step could also be seen as a projection (transforming a bigger thing to a smaller but similar thing), which can be seen in the terminology of Kotlin: Use-site variance in Kotlin is called [type projections](https://kotlinlang.org/docs/reference/generics.html#type-projections).

In general, covariant positions in a type corresponding to a "read" operation and contravariant positions correspond to a "write" operation, so we could say that if we make a type argument corresponding to a type parameter `X` covariant then we are projecting the set of members down to the set of members "that may let me read an `X`, but won't let me write any".

Here is a Kotlin example where `out` is used to make the type of `from` covariant in its type argument:

```kotlin
fun copy(from: Array, to: Array) { ... }
```

The `copy` function will accept a `from` argument whose type argument is an arbitrary type (rather than just one whose type argument is `Any`), but the `to` argument must be an `Array`. In return for the added flexibility on `from`, we can only read elements from that array, we cannot write them, but we can perform both reads and writes on `to`.

## How would Use-site Variance fit in Dart?

In Dart, type parameters of generic classes are always covariant, which is unsound for certain usages (cf. #213). This means that it makes no sense to add variance annotations to Dart exactly as they occur in other languages, but we can add an annotation that _eliminates_ the covariance which is otherwise admitted for every type argument in every type annotation which is a class type. This is the motivation for using the name 'use-site invariance' for this feature.

This proposal uses the modifier `exactly` to indicate that a given type argument is required to be invariant, but it is of course possible to give this marker many other syntactic forms.

Use-site invariance is particularly helpful in the case where the relevant type parameter `X` cannot be declared to be invariant (otherwise we could use declaration-site invariance, which is likely to be much less verbose, and more consistent).

One situation where this occurs is when a type parameter `X` is designed to "perform both reads and writes" for objects of type `X` (or any type which is covariant in `X`). It could also be because the change where `X` is made invariant would cause widespread breakage (e.g., because one class must now be split into several classes, with suitable subtype relationships among them).

For instance, the Dart `List` class will probably not be modified to `class List ..`, because this would be massively breaking. But it would be possible to apply use-site invariance in order to maintain the stronger typing discipline for each individual variable or parameter where this is considered helpful, and that wouldn't break any other usages of the given type.

The invariance of said variable or parameter would give developers a guarantee against variance related type errors, and the run time cost would also be avoided because the type checks are no longer needed.

Note that the combination of use-site invariance and declaration-site invariance allows for a relatively fine-grained control over the constraints and guarantees provided:

```dart
class A {
List l1;
List l2;
}

class B {
List l3;
List l4;
}

A a1; // Redundant invariance.
A a2;
B b1;
B b2;
```

With these declarations we would have guarantees like the following:

- We can safely read elements from all the lists `l1 .. l4` on the relevant receivers `a1`, `a2`, `b1`, or `b2`; likewise, code inside the classes can safely read elements from all the lists. Safe today, remains safe.
- We can safely write a value with static type `num` to `a1.l1`, `a2.l1`, and `b1.l3`. **Safety improved!**
- When writing a value with static type `num` to `a1.l2`, `a2.l2`, `b1.l4`, and `b2.l4`, we get the same dynamic checks that we have today—for _every_ write to a list, or with any other generic type that uses a type parameter in a non-covariant position. Safety unchanged (could specify more invariance to get more safety).
- It is safe for code inside class `A` to write an element of type `X` to `l1`, and similarly for code in `B` that writes an element to `l3`. **Safety improved!**
- For code inside class `A` and `B`, writing to `l2` respectively `l4` is subject the the same dynamic type checks that we have today. Safety unchanged (could specify more invariance to get more safety).

Note that 'safety' in all cases also means 'good performance', because there is no need to check safe types at run time.

Finally, note that the type annotation on `a1` is redundant because `A` has an invariant type parameter (due to declaration-site invariance), and then we top it up with use-site invariance for this variable. This might be considered to be an error (because redundancy is confusing) or it could be allowed (because that would allow some source code changes to be less breaking, and it doesn't actually cause any technical problems), but in any case it makes no difference: The type of `a1` has the same properties as the type of `a2`.

So the point is that we're able to combine declaration-site invariance and use-site invariance in various ways, in order to obtain the desired type safety and performance.

In this context, use-site invariance works as a kind of "glue" that allows us to obtain invariance also in cases where we are working with classes that need more flexibility than declaration-site invariance can offer, either because of the very design of those classes, or because it would cause massive breakage to change those classes.

## The Dynamic Type of an Instance.

It should be noted that we are already used to talk about the run-time type of an instance as a precise type. For example, let `C` be as follows:

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

If we consider the run-time type of the value of a literal like `17`, or an invocation of a generative constructor like `C(17)`, we can't respond "it's an `Object`" even though both instances would yield true if we test them with `is Object`. The run-time type of an instance `o` is understood to be the _most specific_ type `T` such that `o is T` evaluates to true.

But then we should not say that the value `o` of `C(17)` has run-time type `C`, it is actually `C`. That is, for a generic class type, the run-time type of an instance will have the modifier `exactly` on all type arguments.

## Reification of Invariance: Two Approaches

We can use a **simple approach** to use-site invariance where the property of having some amount of invariance is a property of the associated entity (such as a variable, a formal parameter, or a return value), but it can not be used in an actual type argument, and it can not be used in a superinterface.

For example, we can then have a variable whose type is `List`, and its value could be `[]`, but not `[]`. But we could not have a variable with type `List>` and we could not create an instance like `>[[]]` or call a generic function like `[1].map>((_) => [])`.

The point is that we could then avoid having any representation of use-site invariance in the types of instances at run-time, and in reified types. If a dynamic check is required then it is always concerned with the values of actual type arguments of the run-time type of an instance (that we are just about to assign to a variable, or pass to a formal parameter, or return). For example:

```dart
List xs = ...; // Complex expression, could be a `List`.
List ys = xs; // Check that the actual type argument is exactly `num`.
```

The reason why we have to constrain the usages of use-site invariance if we do not have reification is soundness:

```dart
// Assume that use-site invariance is _not_ reified in types, but
// allowed in type arguments. NB: THIS IS NOT SOUND!

main() {
List> xs = >[];
List> ys = xs; // Downcast, implies dynamic check.
xs.add([]); // Check dynamically that the argument `is List`: OK.
ys[0].add(3.14); // Statically safe, fails at runtime (shows unsoundness).
}
```

At the downcast, the value of `xs` has run-time type `List>`. We can check that the actual type argument is `List`, and the representation for this is the same as that for `List` (remember, we don't reify the 'exactly' bit), so we have to make the downcast _succeed_.

We might try to use the static type of `xs` to be more strict, but we'd ultimately need to be able to handle an assignment from an expression of type `dynamic`, so we cannot generally enforce a typing discipline unless we can enforce it based on information which is reified at run time.

But this means that we can add `[]` to this list via `xs`, and that will destroy the heap invariant (that is, we now have a variable with a type `T` whose value is not of type `T`). That situation destroys soundness, so we can get a failure when we pass a `double` in the subsequent invocation of `add`, even though that's statically safe.

Alternatively, we can use a **more powerful approach**: We could reify use-site invariance and allow types like `List>`, `List>`, etc.

I have described the more powerful approach below, and the less powerful model where reification is avoided falls out as a special case.

# Draft Proposal of Specification

The following is a preliminary version of the specification of this feature.

## Grammar

Syntactically, this feature consists of one extra modifier which can be added to the specification of a type argument in a parameterized type. Here is the needed grammar update:

```
::= '<' typeArgumentList '>'

::= (',' )*

::= 'exactly'?
```

It is a compile-time error if a `` _T_ is a parameterized type where one or more of the actual type arguments has the modifier `exactly`, unless it is used as a type annotation of a variable or a formal parameter, as a function return type, as an actual type argument, or as a bound of a type variable.

*In the simple approach: Omit 'as an actual type argument, or as a bound of a type variable'.*

## Static Analysis

In the superinterface subtype rule, the `exactly` modifier is preserved. *For example, `List` is a subtype of `Iterable`.*

We add a new subtype rule that is capable of eliminating 'exactly': Consider a parameterized type _S1_ of the form _C_, where _C_ is a generic class and _Wj_ is of the form _exactly? Tj_, and another parameterized type _S2_ of the form _C_, where _Zj_ is of the form _exactly? Tj_. Then _S1 <: S2_ whenever the following holds for all _j_: If _exactly_ is absent in _Wj_ then _exactly_ is absent in _Zj_.

*For example:*

```dart
List <: List
List <: List
// But `List` and `List` are unrelated.

List> <: List> <: List>
List> <: List>
// But `List>` is not a subtype of
// `List>`, and `List>` and
// `List>` are also unrelated.
```

*With the added subtype rule, some new situations arise where soundness is not guaranteed statically, but the general rules still apply: If assignability turns out to be justified by a supertype rather than a subtype, a dynamic check is generated.*

*Similarly, the new types enable the omission of many dynamic type checks, e.g., when adding an element to a list and in general when passing an argument to a covariant parameter. But this is again not a change that requires any specification changes, it follows as a consequence of the improved type information.*

## Discussion

One decision which is implied by this proposal is that we will not support use-site contravariance. I believe that this is not a deep decision, it would be easy to allow marking actual type arguments as `contravariant` as well as `exactly`, and the associated static and dynamic checks are well-understood.

However, contravariance is already present in Dart, in the shape of function types. It is often possible to use a function type (even though it is not quite as flexible as a class type), or to use invariance (declaration-site or use-site), which is arguably the most important special case of contravariance. So the decision to omit contravariance support is mainly based on the desire to keep the amount of complexity down. Nevertheless, we can presumably just add it if we want it.

Another decision to make is whether to reify invariance in types at run time. The reification has a certain space cost itself (one bit per type argument), and subtype checks would have to spend the time to check those bits.

On top of this, the use-site invariance mechanism is considerably simpler when we include the constraints that are required in order to maintain soundness in a setting where we do not reify invariance in types.

One possible approach could be to add the simple and constrained variant of use-site invariance to Dart first, and then possibly generalize this to include the full model. This would be a non-breaking extension because the constraints that couldn't be enforced in the simple approach could also not be expressed, so only new code will be able to both express and enforce the more complex typing requirements (such as nested occurrences of `exactly`).

Finally, the proposal makes it an error to use `exactly` in the specification of a type argument of a superinterface. This is because the type specified in a superinterface is already similar to the type of an instance, in the sense that its type arguments are the most precise ones that are applicable. Here is an example:

```dart
class A {}
class B extends A {} // Error.
```

The point is that whenever we encounter an instance `o` whose run-time type is `B` for some type `T`, it will also make `o is A` evaluate to true, and there is no proper subtype `T1 <: T` such that `o is A` is also true. This means that `exactly` on the type arguments of a superinterface is redundant. So we leave it out everywhere, rather than requiring it everywhere.

However, there is nothing special about using use-site invariance in nested positions in a superinterface (if we use the more powerful approach where `exactly` is allowed in a type argument at all). For example:

```dart
class MyListList implements List> {
...
}

main() {
List> xs = MyListList();
xs.add([]); // Statically safe.
xs[0].add(3.14); // Statically safe.
}
```