Declaration-site Invariance

[eernstg]

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

Declaration-site variance is known from languages like Scala (using + and -) and C# (using out and in), and the general idea is that each type parameter of a parameterized type declaration may have an associated variance.

For instance, class Foo[+A] .. declares a Scala class whose type argument A is covariant, which means that Foo[T2] is a subtype of Foo[T1] whenever T2 is a subtype of T1.

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 applied to every type parameter. This is the motivation for using the name 'declaration-site invariance' for this feature.

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

This is particularly helpful in the case where the type argument is used in a contravariant position in the body of the generic class.

For instance, if the Dart List class had been declared as class List<invariant E> .. then the add method on lists would have been statically safe. In return, Dart developers would then have to refactor their programs such that they'd never need covariance for lists (so a List<int> could never be the value of a variable of type List<dynamic> or List<num>, only a List<int> variable could refer to such an instance—plus of course variables whose type is a supertype of List<int> in a non-variant way, e.g., a variable of type Object would do as well).

However, the ability to declare a type argument as invariant would be even more helpful in cases where the design of a class relies on contravariant usages of a type parameter in more complex locations. Here is an example:

class Callbacks<invariant X> {
  bool Function(X) forOne;
  bool Function(Iterable<X>) forMany;
  Callbacks(this.forOne, this.forMany);
}

The Callbacks class has fields whose types are contravariant in a type parameter, and if X is covariant then this amounts to a violation of the 'expression soundness' property. First consider the situation today:

main() {
  // Under the current rules `invariant` cannot be specified, and `X` is covariant.
  Callbacks<num> cb = Callbacks<int>((x) => x.isEven, null);
  bool Function(num) f = cb.forOne; // ERROR, at run time.
  bool areEven(Iterable<num> it) => it.every((x) => x.isEven);
  cb.forMany = areEven; // OK.
}

The initialization of f to cb.forOne may seem to be type safe (replacing X by num in the declaration of forOne), but it is unsafe, and a dynamic check will be generated. Developers have no way to make this safe. The other side of this coin is that the assignment to forMany is safe.

In contrast, consider the situation where it is possible to declare the type argument of Callbacks as invariant:

main() {
  // With support for declaration-site invariance,
  // `invariant` can be specified and `X` is then invariant.

  // We cannot get started like before:
  // Callbacks<num> cb = Callbacks<int>((x) => x.isEven, null); // ERROR.

  // But we can use the only type argument that fits, `int`.
  Callbacks<int> cb = Callbacks<int>((x) => x.isEven, null); // OK
  bool Function(num) f = cb.forOne; // Statically known downcast.
  bool areEven(Iterable<num> it) => it.every((x) => x.isEven);
  cb.forMany = areEven; // OK.
}

With invariance, developers can make the choice to have less flexibility (they can't abstract over the exact type argument), in return for improved static safety. Also note that the assignment to cb.forMany still works, because areEven is actually a function whose type is a subtype of the required type, so there is no need to complain even when we know the truth. ;-)

In summary, declaration site invariance in Dart would allow developers to make a different trade-off between the unsound but convenient ability to use covariance, and the more restrictive but sound use of invariance, for each type parameter.

Grammar

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

<typeParameter> ::= <metadata> 'invariant'? <typeIdentifier> ('extends' <typeNotVoid>)?

Static Analysis

The subtype rule that deals with variance is updated such that a parameterized type which is an instantiation of a generic class, C<T₁, .., T_s>, is a subtype of another parameterized type C<U₁, .., U_s> whenever (1) T_j <: U_j for each j, and (2) U_j <: T_j for each j where the corresponding formal type parameter of C is invariant.

The rules governing class declarations are updated: Let C be a generic class with type parameter declarations invariant? X₁ extends B₁, .., invariant? X_s extends B_s and let D<T₁, .., T_t> be a direct superinterface of C. It is a compile-time error if there is a j such that invariant? in the declaration of X_j is empty (that is, X_j is covariant), and there is an i such that X_j occurs in T_i, and the declaration of i'th type parameter of D is invariant (that is, this declaration contains the modifier invariant). Moreover, it is a compile-time error if there is a j such that invariant? in the declaration of X_j is present (that is, X_j is invariant), and there is an i such that X_j occurs in T_i, and the declaration of i'th type parameter of D is not invariant (that is, this declaration does not contain the modifier invariant).

If we do not have the first of these errors then we could have the following kind of unsafe upcast sequences:

class D<invariant X> { X x; }
class C<X> extends D<X> { ... }

// The above declaration of `X` in `C` is an error, because we
// would otherwise have the following:

C<int> c = C();
C<num> c1 = c; // Upcast, by covariance.
D<num> d = c1; // Upcast, using 'extends' subtype rule.

main() {
  d.x = 4.2; // If allowed, this would violate soundness.
}

When d is initialized, the heap invariant ('soundness') is violated. Further usages such as d.x = 4.2 in main must fail because 4.2 is not an int, but, given that X of D is declared invariant, the static analysis would imply that d.x = 4.2 is safe. Hence, we make the declaration of X in C an error.

Similarly, if we do not have the second of these errors then we could have the following kind run-time failure:

class D<X> { X x; }
class C<invariant X> extends D<X> { ... }

// The above declaration of `X` in `C` is an error, because we
// would otherwise have the following:

C<int> c = C();
D<int> d = c; // Upcast, using the 'extends' subtype rule.
D<num> d1 = d; // Upcast, using covariance. But it cannot succeed!

Even though the initialization of d1 is an upcast (so it ought to be perfectly safe), we do not have the required subtype relationship from C<int> to D<num>, so that initialization must cause a dynamic error, or the heap invariant (soundness) will be violated. So we make the declaration of X in D an error.

Discussion

Obviously, invariant is a verbose syntax for specifying that a given type parameter is invariant, and it is very likely that some other syntax will be chosen because it's more concise. On the other hand, invariant matches the use of covariant in Dart already, and it seems rather descriptive.

For a less verbose syntax, using = (as in class C<=X>) would fit pretty well into the tradition of using + and - for covariant resp. contravariant type parameters (in research papers since the 90'ties, and in Scala), even though invariance is traditionally implicit, so there is no actual history of using = for that. A counterargument could be that the occurrence of <= at the given point is visually confusing, and maybe things like class C<X, =Y> are, too.

Following the syntax of C#, we could also use inout to indicate invariance. A counterargument against this choice would be that there are no in or out keywords for related declarations (so inout doesn't come up naturally, and it's not a very natural "word" anyway). Moreover, inout is perhaps already more strongly associated with value parameters (e.g., in Swift).

It would also be possible to associate the invariance with the enclosing class as a whole (which means that it would be applied to all type parameters). This would be more concise when that effect is desired, but it is rather inflexible. It could be considered as an abbreviation.

Another issue which comes up naturally is why this proposal does not mention contravariance. It wouldn't be difficult at all to add support for contravariant as a modifier on a declaration of a formal type parameter (or some other syntax meaning the same thing), and then adjusting the variance related subtype rule accordingly. The reason why I did not include contravariance is simply that it introduces yet another bunch of rules around the subtype relationships of Dart, and this is something that developers will need to be aware of all the time. So we could easily do that, but we might also go for the simpler model without contravariance for classes, and relying on the current advice: "if you need contravariance, you should consider using a function type".

One property of declaration-site invariance which may be somewhat inconvenient is that it propagates up and down the type hierarchy: Whenever there is a connection in the superinterface graph (directly or indirectly) between two type variables X of a class C and Y of a class D (e.g., class C<X> implements D<int, Map<String, X>> {} and class D<Z, Y> {}), we cannot make just one of them invariant—it must be none of them, or both of them; in general, for a set of thus "connected" type variables, we must make none of them invariant, or all of them.

Consequently, declaration-site invariance can be used freely for newly designed class hierarchies, and for type parameters that are introduced in a class without being passed on to superinterfaces, but it will be less easy to sprinkle declaration-site invariance into existing class hierarchies for type variables that are used to specify any superinterfaces.

[munificent]

I would love better static control over variance in Dart. I think dealing with the historical baggage of List<T> is going to make that really hard. We could leave that type covariant with runtime checks everywhere like we do now, but I'm really worried about the performance implications of that.

It might be too much of a breaking change to make List<T> invariant. But I do wonder if something like Kotlin's type projections would help. Perhaps a covariant or contravariant type projection of List<T> would be able to eliminate the runtime variance checks since at that point the compiler knows you're dealing with a statically sound subset of the interface.

[eernstg]

@munificent wrote

too much of a breaking change to make List<T> invariant

Indeed! But that could be addressed using use-site invariance (I'm working on that ;-). Kotlin's type projections are very similar to Java wildcards, and those two mechanisms have exactly the same meaning when it comes to the 'projection' part (it prevents access to members whose signature have a contravariant occurrence of a covariant type parameter, and vice versa). I don't immediately see any difference between type arguments out T in Kotlin and ? extends T in Java. In any case, we can certainly apply use-site invariance to eliminate the dynamic type checks that we currently have for things like myList.add(...).

But I also think it makes sense to allow developers to mark a type parameter as invariant in some cases. For instance, when a type parameter is used in a contravariant position in the type of a mutable field (that's the prototypical example of a "contravariant member"). Such a class is never going to work well with a covariant treatment of that type parameter, so it makes sense to allow the author of this class to say, once and for all, that this parameter should never be covariant.

[munificent]

But I also think it makes sense to allow developers to mark a type parameter as invariant in some cases.

Yes, I totally agree. I think declaration-site variance is what you want 90% of the time. Generic class authors are much more likely than class users to have the sophisticated type expertise to know which variance is appropriate for the type.

I just wanted to point out that declaration site variance isn't enough if we want to be able to eliminate the runtime overhead of covariance checks for most code, since we can't break List.

[eernstg]

The topic of unsoundness derived from the combination of covariance (for class type arguments) and contravariant placement of the corresponding type parameters (in the body of the class) has been discussed many times.

One example is dart-lang/linter#1199.

Another one, dart-lang/site-www#1017, contains further links to more than a dozen SDK issues on topics that are related to this issue.

[eernstg]

About the relationship between Java wildcards and Kotlin type projections: Ross Tate notes here that Kotlin adopted 'mixed-site' variance, which is basically a declaration-site plus use-site mechanism. The point is that declaration-site variance is too restricted to work well in some situations (in particular, in a language with support for mutable state), and use-site variance is (1) too verbose and (2) verbose/complex in client code, rather than in the declaration of the types that are used in client code.

A similar idea was proposed by John Altidor et al. a couple of years earlier (here), where they add declaration-site variance to Java (which already has use-site variance under the name 'wildcarded types').

With support for both kinds, we avoid the verbosity and complexity wherever possible (declaration-site variance works like a default, that we then don't have to write in a lot of places), but we can still have use-site variance in those cases where declaration-site variance can't help us. So I'm working under the assumption that it makes sense for Dart to have both, too.

[eernstg]

have you considered "where" clause on type parameters

It's true that we could express a larger variety of relationships using equations, and where clauses are basically more powerful than plain upper bound declarations because of this. For example, the following allows us to express a relationship between X and Y that we cannot express today (it's basically a lower bound on Y):

class C<X, Y> where List<X> extends Y {}

But I think that's a quite different topic than declaration-site invariance: A richer set of constraints on the allowable values of type parameters will make it possible to get more guarantees in the body of the class that carries these constraints, but it would probably not be easy to prove that many new facts about usages (that is, in code where the type C<..> is used): If you have a variable v of type C<S, T> then you just know that its value has type C<S1, T1> for some S1 <: S and T1 <: T, and then it probably doesn't help you much to know that List<S1> <: T1 (because you can't access S1 or T1, anyway), and you probably won't have to require that List<S> <: T; even if we do require that, they are just type arguments that you have chosen statically when you declared v, so the code that uses v won't get very many new guarantees about the value of that variable.

In contrast, declaration-site invariance will provide clients with new guarantees (e.g., because many method invocations which would otherwise be unsafe are now safe); but it makes no difference whatsoever for the body of the class that clients will only be able to have invariant references to it.

So "where" clauses might be a useful topic to explore, but I don't think it's this issue. ;-)

[eernstg]

I haven't been doing "read it aloud" exercises consistently, even though I do recognize that it's a very useful property of language design if a straightforward reading provides relevant insight. But, for starters, I'd go with an obvious "Here's a class. Its name is C, it has one type parameter X which is invariant, and it extends D<X> ..." ;-)

The underlying notion of being an invariant type parameter is a property of the enclosing class: You can't obtain a related type by changing the value of the type argument. The other side of that coin is that if you have a variable of type C<num> then you know that the value of that variable will have a dynamic type which has C<num> as a superinterface (so it could be C<num> or some subtype D<num, List<int>> with class D<X, Y> extends C<X> .., etc), but it couldn't be C<int>. So when we consider a variable (parameter, returned value, etc.), we know that the actual type argument will be exactly num, at the statically known type C.

Because of this connection, I've often used exactly to indicate this relationship when considering use-site invariance. But it's a bit less natural with declaration-site invariance, because it's declaration-site and hence connects more strongly with the type parameter, and less strongly with the actual type arguments that we may encounter wherever this class is used.

[eernstg]

@tatumizer wrote:

.. invariant .. brings up memories of Sepulka :-)

Sepuling is a fine art! ;-)

What will happen if we change List<num> to List<invariant num>?

List<invariant num> nums=[0];
var objects = nums as List<Object>;  // static error?
var ints = nums as List<int>; // static error?

With the given declaration of nums, its value can have List<num> as a superinterface, but not List<int> or List<double>, so fewer things can occur than before the change. (List is an abstract class, so we can't just say "it can only have type List<num>"; the "superinterface" incantation is just there to take into account that it can be a C<num> for some class C<X> implements List<X>.., etc.)

The things that are possible will all allow for the cast to List<Object> (because that's still an upcast). So there's nothing dangerous about the line marked static error?, but it is also still an 'unnecessary cast'. So we'd presumably treat it exactly the same as today.

The cast to List<int> is a downcast, and the static type of nums justifies the conclusion that this cast will definitely fail, so we can make it an error.

(We need to specify exact types, cf. dart-lang/sdk#33307, and this particular question will be settled as part of that effort.)

[eernstg]

@tatumizer wrote:

this proposal is a part of a larger effort

Every language proposal which gets into the language is part of the development of Dart, so there is always a larger effort around these things. But I was just saying that, specifically, it's part of the topic 'exact types' to decide whether or not you'll get an error at the line var ints ...

About the Schrödinger state: With int x2 = 1.5 as num; you'll get a dynamic error, and similarly for List<int> l2 = [] as List<num>;. It's statically known, of course, that these two initializing expressions need a dynamic check, and dart-lang/sdk#31410 requests that it should be a compile-time error. So if you're referring to the fact that the development from Dart 1 to Dart 2 included a lot of extra static type safety then I can only agree, and, of course, everything about invariance is yet another step in the direction of more static safety.

[eernstg]

Closing this issue in favor of sound declaration site variance (#524).