OLD | NEW |
(Empty) | |
| 1 # Informal Specification: Parameters that are Covariant due to Class Type Parame
ters |
| 2 |
| 3 Owner: eernstg@. |
| 4 |
| 5 ## Summary |
| 6 |
| 7 This document is an informal specification which specifies how to determine the |
| 8 reified type of a tear-off where one or more parameters has a type annotation in |
| 9 which a formal type parameter of the enclosing class occurs in a covariant |
| 10 position. This feature has no effect in Dart 1, it only affects strong mode and |
| 11 the upcoming Dart 2. |
| 12 |
| 13 ## Motivation |
| 14 |
| 15 The main topic here is variance, so we will briefly introduce that |
| 16 concept. |
| 17 |
| 18 Consider the situation where a type is specified as an expression that contains |
| 19 another type as a subexpression. For instance, `List<int>` contains `int` as a |
| 20 subexpression. We may then consider `List<...>` as a function, and `int` as an |
| 21 argument which is passed to that function. With that, covariance is the property |
| 22 that this function is increasing, and contravariance is the property that it is |
| 23 decreasing, using the subtype relation for comparisons. |
| 24 |
| 25 Generic classes in Dart are covariant in all their arguments. For example |
| 26 `List<E>` is covariant in `E`. This then means that `List<...>` is an |
| 27 increasing function, i.e., whenever `S` is a subtype of `T`, `List<S>` will be a |
| 28 subtype of `List<T>`. |
| 29 |
| 30 The subtype rule for function types in Dart 1 is different from the one in |
| 31 strong mode and in the upcoming Dart 2. This difference is the main fact that |
| 32 motivates the feature described in this document. |
| 33 |
| 34 Concretely, the subtype rule for function types allows for covariant return |
| 35 types in all cases. For instance, assuming that two functions `f` and `g` have |
| 36 identical parameter types, the type of `f` will always be a subtype of the type |
| 37 of `g` if `f` returns `int` and `g` returns `num`. |
| 38 |
| 39 This is not true for parameter types. In Dart 1, the function type subtype rule |
| 40 allows for covariant parameter types as well as contravariant ones, but strong |
| 41 mode and the upcoming Dart 2 require contravariance for parameter types. For |
| 42 instance, we have the following cases (using `void` for the return type, because |
| 43 the return type is uninteresting, it should just be the same everywhere): |
| 44 |
| 45 ```dart |
| 46 typedef void F(num n); |
| 47 |
| 48 void f1(Object o) {} |
| 49 void f2(num n) {} |
| 50 void f3(int i) {} |
| 51 |
| 52 main() { |
| 53 F myF; |
| 54 myF = f1; // Contravariance: Succeeds in Dart 1, and in strong mode. |
| 55 myF = f2; // Same type: Always succeeds. |
| 56 myF = f3; // Covariance: Succeeds in Dart 1, but fails in strong mode. |
| 57 } |
| 58 ``` |
| 59 |
| 60 In all cases, the variance is concerned with the relationship between the type |
| 61 of the parameter for `myF` and the type of the parameter for the function which |
| 62 is assigned to `myF`. Since Dart 1 subtyping makes both `f1` and `f3` subtypes |
| 63 of the type of `myF`, all assignments succeed at run time (and static analysis |
| 64 proceeds without warnings). In strong mode and Dart 2, `f3` does not have a |
| 65 subtype of the type of `myF`, so this is considered as a downcast at compile |
| 66 time, and it fails at runtime. |
| 67 |
| 68 Contravariance is the sound rule that most languages use, so this means that |
| 69 function calls in strong mode and in Dart 2 are subject to more tight type |
| 70 checking, and some run-time errors cannot occur. |
| 71 |
| 72 However, covariant parameter types can be quite natural and convenient, they |
| 73 just impose an obligation on developers to use ad-hoc reasoning in order to |
| 74 avoid the potential type errors at run time. The |
| 75 [covariant overrides](https://github.com/dart-lang/sdk/blob/master/docs/language
/informal/covariant-overrides.md) |
| 76 feature was added exactly for this purpose: When developers want to use unsound |
| 77 covariance, they can get it by requesting it explicitly. In the (vast majority |
| 78 of) cases where the sound and more strict contravariant rule fits the intended |
| 79 design, there will be no such request, and parameter type covariance (which |
| 80 would then presumably only arise by mistake) will be flagged as a type error. |
| 81 |
| 82 In order to preserve a fundamental soundness property of Dart, the reified type |
| 83 of tear-offs of methods has parameter type `Object` for every parameter whose |
| 84 type is covariant. The desired property is that every expression with static |
| 85 type `T` must evaluate to a value whose dynamic type `S` which is a subtype of |
| 86 `T`. Here is an example why it would not work to reify the declared parameter |
| 87 type directly: |
| 88 |
| 89 ```dart |
| 90 typedef void F(num n); |
| 91 |
| 92 class A { |
| 93 // Assume the reified parameter type is `num`, directly as declared. |
| 94 void f(covariant num n) {} |
| 95 } |
| 96 |
| 97 class B extends A { |
| 98 // Assume the reified parameter type is `int`, directly as declared. |
| 99 void f(int i) {} |
| 100 } |
| 101 |
| 102 main() { |
| 103 A a = new B(); |
| 104 F myF = a.f; // Statically safe, yet fails at run time in strong mode and Dart
2! |
| 105 } |
| 106 ``` |
| 107 |
| 108 The problem is that `a.f` has static type `(num) -> void`, and if the |
| 109 reified type at run time is `(int) -> void` then `a.f` is an expression |
| 110 whose value at run time does _not_ conform to the statically known type. |
| 111 |
| 112 Even worse, there is no statically known type annotation that we can use in the |
| 113 declaration of `myF` which will make it safe—the value of `a` could be an |
| 114 instance of some other class `C` where the parameter type is `double`, and in |
| 115 general we cannot statically specify a function type where the parameter type is |
| 116 a subtype of the actual parameter type at runtime (as required for the |
| 117 initialization to succeed). |
| 118 |
| 119 _We could use the bottom type as the argument type, `(Null) -> void`, but that |
| 120 makes all invocations unsafe (except `myF(null)`). We believe that it is more |
| 121 useful to preserve the information that "it must be some kind of number", even |
| 122 though not all kinds of numbers will work. With `Null`, we just communicate that |
| 123 all invocations are unsafe, with no hints at all about which ones would be less |
| 124 unsafe than others._ |
| 125 |
| 126 We do not want any such expressions where the value is not a subtype of the |
| 127 statically known type, and hence the reified type of `a.f` is `(Object) -> |
| 128 void`. In general, the type of each covariant parameter is reified as |
| 129 `Object`. In the example, this is how it works: |
| 130 |
| 131 ```dart |
| 132 typedef void F(num n); |
| 133 |
| 134 class A { |
| 135 // The reified parameter type is `Object` because `n` is covariant. |
| 136 void f(covariant num n) {} |
| 137 } |
| 138 |
| 139 class B extends A { |
| 140 // The reified parameter type is `Object` because `i` is covariant. |
| 141 void f(int i) {} |
| 142 } |
| 143 |
| 144 main() { |
| 145 A a = new B(); |
| 146 F myF = a.f; // Statically safe, and succeeds at runtime. |
| 147 } |
| 148 ``` |
| 149 |
| 150 _Note that an invocation of `myF` can be statically safe and yet fail at runtime
, |
| 151 e.g., `myF(3.1)`, but this is exactly the same situation as with the torn-off |
| 152 method: `a.f(3.1)` is also considered statically safe, and yet it will fail at |
| 153 runtime._ |
| 154 |
| 155 The purpose of this document is to cover one extra type of situation where the |
| 156 same typing situation arises. |
| 157 |
| 158 Parameters can have a covariant type because they are or contain a formal type |
| 159 parameter of an enclosing generic class. Here is an example using the core class |
| 160 `List` (which underscores that it is a common phenomenon, but any generic class |
| 161 would do): |
| 162 |
| 163 ```dart |
| 164 // Here is the small part of the core List class that we need here. |
| 165 abstract class List<E> ... { |
| 166 // The reified type is `(E) -> void` in all modes, as declared. |
| 167 void add(E value); |
| 168 // The reified type is `(Iterable<E>) -> void` in all modes, as declared. |
| 169 void addAll(Iterable<E> iterable); |
| 170 ... |
| 171 } |
| 172 |
| 173 typedef void F(num n); |
| 174 typedef void G(Iterable<num> n); |
| 175 |
| 176 main() { |
| 177 List<num> xs = <int>[1, 2]; |
| 178 F myF = xs.add; // Statically safe, yet fails at run time |
| 179 // in strong mode and Dart 2. |
| 180 G myG = xs.addAll; // Same as above. |
| 181 } |
| 182 ``` |
| 183 |
| 184 The example illustrates that the exact same typing situation arises in the |
| 185 following two cases: |
| 186 |
| 187 - A covariant parameter type is induced by an overriding method declaration |
| 188 (example: `int i` in `B.f`). |
| 189 - A Covariant parameter type is induced by the use of a formal type parameter of |
| 190 the enclosing generic class in a covariant position in the parameter type |
| 191 declaration (example: `E value` and `Iterable<E> iterable` in `List.add` |
| 192 resp. `List.addAll`). |
| 193 |
| 194 This document specifies how to preserve the above mentioned expression soundness |
| 195 property of Dart, based on a modified rule for how to reify parameter types of |
| 196 tear-offs. |
| 197 |
| 198 ## Informal specification |
| 199 |
| 200 ### Syntax |
| 201 |
| 202 This feature does not give rise to any changes to the grammar of the language. |
| 203 |
| 204 ### Standard mode |
| 205 |
| 206 This feature does not give rise to any changes to the static analysis nor the |
| 207 dynamic semantics of standard mode. |
| 208 |
| 209 ### Strong mode |
| 210 |
| 211 In strong mode, this feature causes changes to the reified type of a function |
| 212 obtained by a closurizing property extraction in some cases, as specified |
| 213 below. |
| 214 |
| 215 #### Static types |
| 216 |
| 217 The static type of a property extraction remains unchanged. |
| 218 |
| 219 _The static type of a torn-off method is taken directly from the statically |
| 220 known declaration of that method, substituting actual type arguments for formal |
| 221 type parameters as usual. For instance, the static type of `xs.addAll` is |
| 222 `(Iterable<num>) -> void` when the static type of `xs` is `List<num>`._ |
| 223 |
| 224 #### Reified types |
| 225 |
| 226 We need to introduce a new kind of covariant parameters, in addition to the |
| 227 notion of covariant parameters which is introduced in the informal |
| 228 specification of |
| 229 [covariant overrides](https://github.com/dart-lang/sdk/blob/master/docs/language
/informal/covariant-overrides.md). |
| 230 |
| 231 Consider a class _T_ which is generic or has a generic supertype (directly or |
| 232 indirectly). Let _S_ be said generic class. Assume that there is a declaration |
| 233 of a method, setter, or operator `m` in _S_, that `X` is a formal type parameter |
| 234 declared by _S_, and that said declaration of `m` has a formal parameter `x` |
| 235 whose type contains `X` in a covariant position. In this situation we say that |
| 236 the parameter `x` is **covariant due to class covariance**. |
| 237 |
| 238 _The type of `x` is in a covariant position when the type is `X` itself, e.g., |
| 239 when the parameter is declared as `X x`. It is also in a covariant position when |
| 240 it is declared like `List<X> x`, because generic classes are covariant in all |
| 241 their type arguments. An example where `X` does not occur in a covariant |
| 242 position is when `x` is a function typed parameter like `int x(X arg)`._ |
| 243 |
| 244 In the remainder of this section, a parameter which is covariant according |
| 245 to the definition given in |
| 246 [covariant overrides](https://github.com/dart-lang/sdk/blob/master/docs/language
/informal/covariant-overrides.md) |
| 247 is treated the same as a parameter which is covariant due to class covariance as |
| 248 defined in this document; in both cases we just refer to the parameter as a |
| 249 _covariant parameter_. |
| 250 |
| 251 The reified type for a function _f_ obtained by a closurizing property |
| 252 extraction on an instance method, setter, or operator is determined as follows: |
| 253 |
| 254 Let `m` be the name of the method, operator, or setter which is being |
| 255 closurized, let _T_ be the dynamic type of the receiver, and let _D_ be |
| 256 the declaration of `m` in _T_ or inherited by _T_ which is being extracted. |
| 257 |
| 258 The reified return type of _f_ the is the static return type of _D_. For each |
| 259 parameter `p` declared in _D_ which is not covariant, the part in the dynamic |
| 260 type of _f_ which corresponds to `p` is the static type of `p` in _D_. For each |
| 261 covariant parameter `q`, the part in the dynamic type of _f_ which corresponds |
| 262 to `q` is `Object`. |
| 263 |
| 264 _The occurrences of type parameters in the types of non-covariant parameters |
| 265 (note that those occurrences must be in a non-covariant position in the |
| 266 parameter type) are used as-is. For instance, `<String>[].asMap()` will have the |
| 267 reified type `() -> Map<int, String>`._ |
| 268 |
| 269 The dynamic checks associated with invocation of such a function are still |
| 270 needed, and they are unchanged. |
| 271 |
| 272 _That is, a dynamic error occurs if a method with a covariant parameter p is |
| 273 invoked, and the actual argument value bound to p has a run-time type which is |
| 274 not a subtype of the type declared for p._ |
| 275 |
| 276 ## Alternatives |
| 277 |
| 278 The "erasure" of the reified parameter type for each covariant parameter to |
| 279 `Object` may seem agressive. |
| 280 |
| 281 In particular, it ignores upper bounds on the formal type parameter which gives |
| 282 rise to the covariance due to class covariance, and it ignores the structure of |
| 283 the type where that formal type parameter is used. Here are two examples: |
| 284 |
| 285 ```dart |
| 286 class C<X extends num> { |
| 287 void foo(X x) {} |
| 288 void bar(List<X> xs) {} |
| 289 } |
| 290 ``` |
| 291 |
| 292 With this declaration, the reified type of `new C<int>().foo` will be `(Object) |
| 293 -> void`, even though it would have been possible to use the type `(num) -> |
| 294 void` based on the upper bound of `X`, and still preserve the earlier mentioned |
| 295 expression soundness. This is because all supertypes of the dynamic type of the |
| 296 receiver that declare `foo` have an argument type for it which is a subtype of |
| 297 `num`. |
| 298 |
| 299 Similarly, the reified type of `new C<int>().bar` will be `(Object) -> void`, |
| 300 even though it would have been possible to use the type `(List<num>) -> void`. |
| 301 |
| 302 Note that the reified type is independent of the static type of the receiver, so |
| 303 it does not matter that we consider `new C<int>()` directly, rather than using |
| 304 an intermediate variable whose type annotation is some supertype, e.g., |
| 305 `C<num>`. |
| 306 |
| 307 In the first example, `foo`, there is a loss of information because we are |
| 308 (dynamically) allowed to assign the function to a variable of type `(Object) -> |
| 309 void`. Even worse, we may assign it to a variable of type `(String) -> void`, |
| 310 because `(Object) -> void` (that is, the actual type that the function reports |
| 311 to have) is a subtype of `(String) -> void`. In that situation, every statically |
| 312 safe invocation will fail, because there are no values of type `String` which |
| 313 will satisfy the dynamic check in the function itself, which requires an |
| 314 argument of type `int` (except `null`, of course, but this is rarely sufficient |
| 315 to make the function useful). |
| 316 |
| 317 In the second example, `bar`, the same phenomenon is extended a little, because |
| 318 we may assign the given torn-off function to a variable of type `(String) -> |
| 319 void`, in addition to more reasonable ones like `(Object) -> void`, |
| 320 `(Iterable<Object>) -> void`, and `(Iterable<int>) -> void`. |
| 321 |
| 322 It is certainly possible to specify a more "tight" reified type like the ones |
| 323 mentioned above. In order to do this, we would need the least upper bound of all |
| 324 the statically known types in all supertypes of the dynamic type of the |
| 325 receiver. This would involve a least upper bound operation on a set of types, |
| 326 and it would involve an instantiate-to-bounds operation on the type parameters. |
| 327 |
| 328 The main problem with this approach is that some declarations do not allow for |
| 329 computation of a finite type which is the least upper bound of all possible |
| 330 instantiations, so we cannot instantiate-to-bound: |
| 331 |
| 332 ```dart |
| 333 // There is no finite type `T` such that all possible values |
| 334 // for `X` are subtypes of `T`. |
| 335 class D<X extends D<X>> {} |
| 336 ``` |
| 337 |
| 338 Similarly, some finite sets of types do not have a denotable least upper bound: |
| 339 |
| 340 ```dart |
| 341 class I {} |
| 342 class J {} |
| 343 |
| 344 class A implements I, J {} |
| 345 class B implements I, J {} |
| 346 ``` |
| 347 |
| 348 In this case both of `A` and `B` have the two immediate superinterfaces `I` and |
| 349 `J`, and there is no single type (that we can express in Dart) which is the |
| 350 least of all the supertypes of `A` and `B`. |
| 351 |
| 352 So in some cases we will have to error out when we compute the reified type of a |
| 353 tear-off of a given method, unless we introduce intersection types and infinite |
| 354 types, or unless we find some other way around this difficulty. |
| 355 |
| 356 On the other hand, it should be noted that the common usage of these torn-off |
| 357 functions would be guided by the statically known types, which do have the |
| 358 potential to keep them "within a safe domain". |
| 359 |
| 360 Here is an example: |
| 361 |
| 362 ```dart |
| 363 main() { |
| 364 List<int> xs = <int>[]; |
| 365 void Function(int) f1 = xs.add; // Same type statically, OK at runtime. |
| 366 void Function(num) f2 = xs.add; // Statically a downcast, can warn, OK at runt
ime. |
| 367 void Function(Object) f3 = xs.add; // A downcast, can warn, OK at runtime. |
| 368 void Function(String) f4 = xs.add; // An unrelated type, error in strong mode. |
| 369 |
| 370 List<num> ys = xs; // "Forget part of the type". |
| 371 void Function(int) f5 = ys.add; // Statically an upcast, OK at runtime. |
| 372 void Function(num) f6 = ys.add; // Statically same type, OK at runtime. |
| 373 void Function(Object) f7 = ys.add; // Statically a downcast, OK at runtime. |
| 374 void Function(String) f8 = ys.add; // An unrelated type, error in strong mode. |
| 375 |
| 376 List<Object> zs = ys; |
| 377 void Function(int) f9 = zs.add; // Statically an upcast, OK at runtime. |
| 378 void Function(num) fa = zs.add; // Statically an upcast, OK at runtime. |
| 379 void Function(Object) fb = zs.add; // Statically a same type, OK at runtime. |
| 380 void Function(String) fc = zs.add; // Finally we can go wrong silently! |
| 381 } |
| 382 ``` |
| 383 |
| 384 In other words, the static typing helps programmers to maintain the same level |
| 385 of knowledge (say, "this is a list of `num`") consistently, even though it is |
| 386 consistently incomplete ("it's actually a list of `int`"), and this helps a lot |
| 387 in avoiding those crazy assignments (to `List<String>`) where almost all method |
| 388 invocations will go wrong. |
OLD | NEW |