diff --git a/docs/language/informal/covariant-from-class.md b/docs/language/informal/covariant-from-class.md new file mode 100644 index 00000000000..b9f3afe7ac5 --- /dev/null +++ b/docs/language/informal/covariant-from-class.md @@ -0,0 +1,388 @@ +# Informal Specification: Parameters that are Covariant due to Class Type Parameters + +Owner: eernstg@. + +## Summary + +This document is an informal specification which specifies how to determine the +reified type of a tear-off where one or more parameters has a type annotation in +which a formal type parameter of the enclosing class occurs in a covariant +position. This feature has no effect in Dart 1, it only affects strong mode and +the upcoming Dart 2. + +## Motivation + +The main topic here is variance, so we will briefly introduce that +concept. + +Consider the situation where a type is specified as an expression that contains +another type as a subexpression. For instance, `List` contains `int` as a +subexpression. We may then consider `List<...>` as a function, and `int` as an +argument which is passed to that function. With that, covariance is the property +that this function is increasing, and contravariance is the property that it is +decreasing, using the subtype relation for comparisons. + +Generic classes in Dart are covariant in all their arguments. For example +`List` is covariant in `E`. This then means that `List<...>` is an +increasing function, i.e., whenever `S` is a subtype of `T`, `List` will be a +subtype of `List`. + +The subtype rule for function types in Dart 1 is different from the one in +strong mode and in the upcoming Dart 2. This difference is the main fact that +motivates the feature described in this document. + +Concretely, the subtype rule for function types allows for covariant return +types in all cases. For instance, assuming that two functions `f` and `g` have +identical parameter types, the type of `f` will always be a subtype of the type +of `g` if `f` returns `int` and `g` returns `num`. + +This is not true for parameter types. In Dart 1, the function type subtype rule +allows for covariant parameter types as well as contravariant ones, but strong +mode and the upcoming Dart 2 require contravariance for parameter types. For +instance, we have the following cases (using `void` for the return type, because +the return type is uninteresting, it should just be the same everywhere): + +```dart +typedef void F(num n); + +void f1(Object o) {} +void f2(num n) {} +void f3(int i) {} + +main() { + F myF; + myF = f1; // Contravariance: Succeeds in Dart 1, and in strong mode. + myF = f2; // Same type: Always succeeds. + myF = f3; // Covariance: Succeeds in Dart 1, but fails in strong mode. +} +``` + +In all cases, the variance is concerned with the relationship between the type +of the parameter for `myF` and the type of the parameter for the function which +is assigned to `myF`. Since Dart 1 subtyping makes both `f1` and `f3` subtypes +of the type of `myF`, all assignments succeed at run time (and static analysis +proceeds without warnings). In strong mode and Dart 2, `f3` does not have a +subtype of the type of `myF`, so this is considered as a downcast at compile +time, and it fails at runtime. + +Contravariance is the sound rule that most languages use, so this means that +function calls in strong mode and in Dart 2 are subject to more tight type +checking, and some run-time errors cannot occur. + +However, covariant parameter types can be quite natural and convenient, they +just impose an obligation on developers to use ad-hoc reasoning in order to +avoid the potential type errors at run time. The +[covariant overrides](https://github.com/dart-lang/sdk/blob/master/docs/language/informal/covariant-overrides.md) +feature was added exactly for this purpose: When developers want to use unsound +covariance, they can get it by requesting it explicitly. In the (vast majority +of) cases where the sound and more strict contravariant rule fits the intended +design, there will be no such request, and parameter type covariance (which +would then presumably only arise by mistake) will be flagged as a type error. + +In order to preserve a fundamental soundness property of Dart, the reified type +of tear-offs of methods has parameter type `Object` for every parameter whose +type is covariant. The desired property is that every expression with static +type `T` must evaluate to a value whose dynamic type `S` which is a subtype of +`T`. Here is an example why it would not work to reify the declared parameter +type directly: + +```dart +typedef void F(num n); + +class A { + // Assume the reified parameter type is `num`, directly as declared. + void f(covariant num n) {} +} + +class B extends A { + // Assume the reified parameter type is `int`, directly as declared. + void f(int i) {} +} + +main() { + A a = new B(); + F myF = a.f; // Statically safe, yet fails at run time in strong mode and Dart 2! +} +``` + +The problem is that `a.f` has static type `(num) -> void`, and if the +reified type at run time is `(int) -> void` then `a.f` is an expression +whose value at run time does _not_ conform to the statically known type. + +Even worse, there is no statically known type annotation that we can use in the +declaration of `myF` which will make it safe—the value of `a` could be an +instance of some other class `C` where the parameter type is `double`, and in +general we cannot statically specify a function type where the parameter type is +a subtype of the actual parameter type at runtime (as required for the +initialization to succeed). + +_We could use the bottom type as the argument type, `(Null) -> void`, but that +makes all invocations unsafe (except `myF(null)`). We believe that it is more +useful to preserve the information that "it must be some kind of number", even +though not all kinds of numbers will work. With `Null`, we just communicate that +all invocations are unsafe, with no hints at all about which ones would be less +unsafe than others._ + +We do not want any such expressions where the value is not a subtype of the +statically known type, and hence the reified type of `a.f` is `(Object) -> +void`. In general, the type of each covariant parameter is reified as +`Object`. In the example, this is how it works: + +```dart +typedef void F(num n); + +class A { + // The reified parameter type is `Object` because `n` is covariant. + void f(covariant num n) {} +} + +class B extends A { + // The reified parameter type is `Object` because `i` is covariant. + void f(int i) {} +} + +main() { + A a = new B(); + F myF = a.f; // Statically safe, and succeeds at runtime. +} +``` + +_Note that an invocation of `myF` can be statically safe and yet fail at runtime, +e.g., `myF(3.1)`, but this is exactly the same situation as with the torn-off +method: `a.f(3.1)` is also considered statically safe, and yet it will fail at +runtime._ + +The purpose of this document is to cover one extra type of situation where the +same typing situation arises. + +Parameters can have a covariant type because they are or contain a formal type +parameter of an enclosing generic class. Here is an example using the core class +`List` (which underscores that it is a common phenomenon, but any generic class +would do): + +```dart +// Here is the small part of the core List class that we need here. +abstract class List ... { + // The reified type is `(E) -> void` in all modes, as declared. + void add(E value); + // The reified type is `(Iterable) -> void` in all modes, as declared. + void addAll(Iterable iterable); + ... +} + +typedef void F(num n); +typedef void G(Iterable n); + +main() { + List xs = [1, 2]; + F myF = xs.add; // Statically safe, yet fails at run time + // in strong mode and Dart 2. + G myG = xs.addAll; // Same as above. +} +``` + +The example illustrates that the exact same typing situation arises in the +following two cases: + +- A covariant parameter type is induced by an overriding method declaration + (example: `int i` in `B.f`). +- A Covariant parameter type is induced by the use of a formal type parameter of + the enclosing generic class in a covariant position in the parameter type + declaration (example: `E value` and `Iterable iterable` in `List.add` + resp. `List.addAll`). + +This document specifies how to preserve the above mentioned expression soundness +property of Dart, based on a modified rule for how to reify parameter types of +tear-offs. + +## Informal specification + +### Syntax + +This feature does not give rise to any changes to the grammar of the language. + +### Standard mode + +This feature does not give rise to any changes to the static analysis nor the +dynamic semantics of standard mode. + +### Strong mode + +In strong mode, this feature causes changes to the reified type of a function +obtained by a closurizing property extraction in some cases, as specified +below. + +#### Static types + +The static type of a property extraction remains unchanged. + +_The static type of a torn-off method is taken directly from the statically +known declaration of that method, substituting actual type arguments for formal +type parameters as usual. For instance, the static type of `xs.addAll` is +`(Iterable) -> void` when the static type of `xs` is `List`._ + +#### Reified types + +We need to introduce a new kind of covariant parameters, in addition to the +notion of covariant parameters which is introduced in the informal +specification of +[covariant overrides](https://github.com/dart-lang/sdk/blob/master/docs/language/informal/covariant-overrides.md). + +Consider a class _T_ which is generic or has a generic supertype (directly or +indirectly). Let _S_ be said generic class. Assume that there is a declaration +of a method, setter, or operator `m` in _S_, that `X` is a formal type parameter +declared by _S_, and that said declaration of `m` has a formal parameter `x` +whose type contains `X` in a covariant position. In this situation we say that +the parameter `x` is **covariant due to class covariance**. + +_The type of `x` is in a covariant position when the type is `X` itself, e.g., +when the parameter is declared as `X x`. It is also in a covariant position when +it is declared like `List x`, because generic classes are covariant in all +their type arguments. An example where `X` does not occur in a covariant +position is when `x` is a function typed parameter like `int x(X arg)`._ + +In the remainder of this section, a parameter which is covariant according +to the definition given in +[covariant overrides](https://github.com/dart-lang/sdk/blob/master/docs/language/informal/covariant-overrides.md) +is treated the same as a parameter which is covariant due to class covariance as +defined in this document; in both cases we just refer to the parameter as a +_covariant parameter_. + +The reified type for a function _f_ obtained by a closurizing property +extraction on an instance method, setter, or operator is determined as follows: + +Let `m` be the name of the method, operator, or setter which is being +closurized, let _T_ be the dynamic type of the receiver, and let _D_ be +the declaration of `m` in _T_ or inherited by _T_ which is being extracted. + +The reified return type of _f_ the is the static return type of _D_. For each +parameter `p` declared in _D_ which is not covariant, the part in the dynamic +type of _f_ which corresponds to `p` is the static type of `p` in _D_. For each +covariant parameter `q`, the part in the dynamic type of _f_ which corresponds +to `q` is `Object`. + +_The occurrences of type parameters in the types of non-covariant parameters +(note that those occurrences must be in a non-covariant position in the +parameter type) are used as-is. For instance, `[].asMap()` will have the +reified type `() -> Map`._ + +The dynamic checks associated with invocation of such a function are still +needed, and they are unchanged. + +_That is, a dynamic error occurs if a method with a covariant parameter p is +invoked, and the actual argument value bound to p has a run-time type which is +not a subtype of the type declared for p._ + +## Alternatives + +The "erasure" of the reified parameter type for each covariant parameter to +`Object` may seem agressive. + +In particular, it ignores upper bounds on the formal type parameter which gives +rise to the covariance due to class covariance, and it ignores the structure of +the type where that formal type parameter is used. Here are two examples: + +```dart +class C { + void foo(X x) {} + void bar(List xs) {} +} +``` + +With this declaration, the reified type of `new C().foo` will be `(Object) +-> void`, even though it would have been possible to use the type `(num) -> +void` based on the upper bound of `X`, and still preserve the earlier mentioned +expression soundness. This is because all supertypes of the dynamic type of the +receiver that declare `foo` have an argument type for it which is a subtype of +`num`. + +Similarly, the reified type of `new C().bar` will be `(Object) -> void`, +even though it would have been possible to use the type `(List) -> void`. + +Note that the reified type is independent of the static type of the receiver, so +it does not matter that we consider `new C()` directly, rather than using +an intermediate variable whose type annotation is some supertype, e.g., +`C`. + +In the first example, `foo`, there is a loss of information because we are +(dynamically) allowed to assign the function to a variable of type `(Object) -> +void`. Even worse, we may assign it to a variable of type `(String) -> void`, +because `(Object) -> void` (that is, the actual type that the function reports +to have) is a subtype of `(String) -> void`. In that situation, every statically +safe invocation will fail, because there are no values of type `String` which +will satisfy the dynamic check in the function itself, which requires an +argument of type `int` (except `null`, of course, but this is rarely sufficient +to make the function useful). + +In the second example, `bar`, the same phenomenon is extended a little, because +we may assign the given torn-off function to a variable of type `(String) -> +void`, in addition to more reasonable ones like `(Object) -> void`, +`(Iterable) -> void`, and `(Iterable) -> void`. + +It is certainly possible to specify a more "tight" reified type like the ones +mentioned above. In order to do this, we would need the least upper bound of all +the statically known types in all supertypes of the dynamic type of the +receiver. This would involve a least upper bound operation on a set of types, +and it would involve an instantiate-to-bounds operation on the type parameters. + +The main problem with this approach is that some declarations do not allow for +computation of a finite type which is the least upper bound of all possible +instantiations, so we cannot instantiate-to-bound: + +```dart +// There is no finite type `T` such that all possible values +// for `X` are subtypes of `T`. +class D> {} +``` + +Similarly, some finite sets of types do not have a denotable least upper bound: + +```dart +class I {} +class J {} + +class A implements I, J {} +class B implements I, J {} +``` + +In this case both of `A` and `B` have the two immediate superinterfaces `I` and +`J`, and there is no single type (that we can express in Dart) which is the +least of all the supertypes of `A` and `B`. + +So in some cases we will have to error out when we compute the reified type of a +tear-off of a given method, unless we introduce intersection types and infinite +types, or unless we find some other way around this difficulty. + +On the other hand, it should be noted that the common usage of these torn-off +functions would be guided by the statically known types, which do have the +potential to keep them "within a safe domain". + +Here is an example: + +```dart +main() { + List xs = []; + void Function(int) f1 = xs.add; // Same type statically, OK at runtime. + void Function(num) f2 = xs.add; // Statically a downcast, can warn, OK at runtime. + void Function(Object) f3 = xs.add; // A downcast, can warn, OK at runtime. + void Function(String) f4 = xs.add; // An unrelated type, error in strong mode. + + List ys = xs; // "Forget part of the type". + void Function(int) f5 = ys.add; // Statically an upcast, OK at runtime. + void Function(num) f6 = ys.add; // Statically same type, OK at runtime. + void Function(Object) f7 = ys.add; // Statically a downcast, OK at runtime. + void Function(String) f8 = ys.add; // An unrelated type, error in strong mode. + + List zs = ys; + void Function(int) f9 = zs.add; // Statically an upcast, OK at runtime. + void Function(num) fa = zs.add; // Statically an upcast, OK at runtime. + void Function(Object) fb = zs.add; // Statically a same type, OK at runtime. + void Function(String) fc = zs.add; // Finally we can go wrong silently! +} +``` + +In other words, the static typing helps programmers to maintain the same level +of knowledge (say, "this is a list of `num`") consistently, even though it is +consistently incomplete ("it's actually a list of `int`"), and this helps a lot +in avoiding those crazy assignments (to `List`) where almost all method +invocations will go wrong.