OLD | NEW |
1 ## Feature: Generalized Void | 1 ## Feature: Generalized Void |
2 | 2 |
3 Author: eernst@ | 3 Author: eernst@ |
4 | 4 |
5 **Status**: Under implementation. | 5 **Status**: Under implementation. |
6 | 6 |
7 **This document** is an informal specification of the generalized support | 7 **This document** is an informal specification of the generalized support |
8 in Dart 1.x for the type `void`. Dart 2 will have a very similar kind of | 8 in Dart 1.x for the type `void`. Dart 2 will have a very similar kind of |
9 generalized support for `void`, without the function type subtype exception | 9 generalized support for `void`, without the function type subtype exception |
10 that this feature includes for backward compatibility in Dart 1.x. This | 10 that this feature includes for backward compatibility in Dart 1.x. This |
(...skipping 12 matching lines...) Expand all Loading... |
23 used to indicate that the visit is performed for its side-effects | 23 used to indicate that the visit is performed for its side-effects |
24 alone. The generalized void feature includes mechanisms to help developers | 24 alone. The generalized void feature includes mechanisms to help developers |
25 avoid using such a value. | 25 avoid using such a value. |
26 | 26 |
27 In general, situations where it may be desirable to use `void` as | 27 In general, situations where it may be desirable to use `void` as |
28 a type argument arise when the corresponding formal type variable is used | 28 a type argument arise when the corresponding formal type variable is used |
29 covariantly. For instance, the class `Future<T>` uses return types | 29 covariantly. For instance, the class `Future<T>` uses return types |
30 like `Future<T>` and `Stream<T>`, and it uses `T` as a parameter type of a | 30 like `Future<T>` and `Stream<T>`, and it uses `T` as a parameter type of a |
31 callback in the method `then`. | 31 callback in the method `then`. |
32 | 32 |
33 Note that is not technically dangerous to use a value of type `void`, it | 33 Note that using the value of an expression of type `void` is not |
34 does not violate any constraints at the level of the language semantics. | 34 technically dangerous, doing so does not violate any constraints at the |
35 Developers just made the decision to declare that the value is useless, | 35 level of the language semantics. By using the type `void`, developers |
36 based on the program logic. Hence, there is **no requirement** for the | 36 indicate that the value of the corresponding expression evaluation is |
37 generalized void mechanism to be strict and **sound**. However, it is the | 37 meaningless. Hence, there is **no requirement** for the generalized void |
38 intention that the mechanism should be sufficiently strict to make the | 38 mechanism to be strict and **sound**. However, it is the intention that the |
39 mechanism helpful and non-frustrating in practice. | 39 mechanism should be sufficiently sound to make the mechanism helpful and |
| 40 non-frustrating in practice. |
40 | 41 |
41 No constraints are imposed on which values may be given type `void`, so in | 42 No constraints are imposed on which values may be given type `void`, so in |
42 that sense `void` can be considered to be just another name for the type | 43 that sense `void` can be considered to be just another name for the type |
43 `Object`, flagged as useless. Note that this is an approximate rule (in | 44 `Object`, flagged as useless. Note that this is an approximate rule in |
44 Dart 1.x), it fails to hold for function types. | 45 Dart 1.x, it fails to hold for function types; it does hold in Dart 2. |
45 | 46 |
46 The mechanisms helping developers to avoid using values of type `void` are | 47 The mechanisms helping developers to avoid using the value of an expression |
47 divided into **two phases**. This document specifies the first phase. | 48 of type `void` are divided into **two phases**. This document specifies the |
| 49 first phase. |
48 | 50 |
49 The **first phase** uses restrictions which are based on syntactic criteria | 51 The **first phase** uses restrictions which are based on syntactic criteria |
50 in order to ensure that direct usage of a value of type `void` is a static | 52 in order to ensure that direct usage of the value of an expression of type |
51 warning (in Dart 2: an error). A few exceptions are allowed, e.g., type | 53 `void` is a static warning (in Dart 2: an error). A few exceptions are |
52 casts, such that developers can explicitly make the choice to use such a | 54 allowed, e.g., type casts, such that developers can explicitly make the |
53 value. The general rule is that all values of type `void` must be | 55 choice to use such a value. The general rule is that for every expression |
54 discarded. | 56 of type `void`, its value must be ignored. |
55 | 57 |
56 The **second phase** will deal with casts and preservation of | 58 The **second phase** will deal with casts and preservation of |
57 voidness. Some casts will cause derived expressions to switch from having | 59 voidness. Some casts will cause derived expressions to switch from having |
58 type `void` to having some other type, and hence those casts introduce the | 60 type `void` to having some other type, and hence those casts introduce the |
59 possibility that "a void value" will get passed and used. Here is an | 61 possibility that "a void value" will get passed and used. Here is an |
60 example: | 62 example: |
61 | 63 |
62 ```dart | 64 ```dart |
63 class A<T> { T foo(); } | 65 class A<T> { T foo(); } |
64 A<Object> a = new A<void>(); // Violates voidness preservation. | 66 A<Object> a = new A<void>(); // Violates voidness preservation. |
65 var x = a.foo(); // Use a "void value", with static type Object. | 67 var x = a.foo(); // Use a "void value", now with static type Object. |
66 ``` | 68 ``` |
67 | 69 |
68 We intend to introduce a **voidness preservation analysis** (which is | 70 We intend to introduce a **voidness preservation analysis** (which is |
69 similar to a small type system) to keep track of such situations. As | 71 similar to a small type system) to keep track of such situations. As |
70 mentioned, the second phase is **not specified in this document**. Voidness | 72 mentioned, the second phase is **not specified in this document**. Voidness |
71 preservation is a purely static analysis, and there are no plans to | 73 preservation is a purely static analysis, and there are no plans to |
72 introduce dynamic checking for it. | 74 introduce dynamic checking for it. |
73 | 75 |
74 ## Syntax | 76 ## Syntax |
75 | 77 |
(...skipping 82 matching lines...) Expand 10 before | Expand all | Expand 10 after Loading... |
158 There is no value which is the reified representation of the type void at | 160 There is no value which is the reified representation of the type void at |
159 run time. | 161 run time. |
160 | 162 |
161 *Syntactically, `void` cannot occur as an expression, and hence expression | 163 *Syntactically, `void` cannot occur as an expression, and hence expression |
162 evaluation cannot directly yield such a value. However, a formal type | 164 evaluation cannot directly yield such a value. However, a formal type |
163 parameter can be used in expressions, and the actual type argument bound to | 165 parameter can be used in expressions, and the actual type argument bound to |
164 that formal type parameter can be the type void. That case is specified | 166 that formal type parameter can be the type void. That case is specified |
165 explicitly below. Apart from the reserved word `void` and a formal type | 167 explicitly below. Apart from the reserved word `void` and a formal type |
166 parameter, no other term can denote the type void.* | 168 parameter, no other term can denote the type void.* |
167 | 169 |
168 *Conversely, `void` cannot denote any other entity than the type void: | 170 *There is no way for a Dart program at run time to obtain a reified |
169 `void` cannot occur as the declared name of any declaration (including | 171 representation of a return type or parameter type of a function type, even |
170 library prefixes, types, variables, parameters, etc.). This implies that | 172 when the function type as a whole may be obtained (e.g., the function type |
171 `void` is not subject to scoped lookup, and the name is not exported by any | 173 could be passed as a type argument and the corresponding formal type |
172 system library. Similarly, it can never be accessed using a prefixed | 174 parameter could be evaluated as an expression). A reified representation of |
173 expression (`p.void`). Hence, `void` has a fixed meaning everywhere in all | 175 such a return type is therefore not necessary.* |
174 Dart programs, and it can only occur as a stand-alone word.* | |
175 | 176 |
176 When `void` is passed as an actual type argument to a generic class or a | 177 For a composite type (a generic class instantiation or a function type), |
177 generic function, and when the type void occurs as a parameter type in a | 178 the reified representation at run time must be such that the type void and |
178 function type, the reified representation is equal (according to `==`) to | 179 the built-in class `Object` are treated as equal according to `==`, but |
179 the reified representation of the built-in class `Object`. | 180 they need not be `identical`. |
180 | 181 |
181 *It is encouraged for an implementation to use a reified representation for | 182 *For example, with `typedef F<S, T> = S Function(T)`, the `Type` instance |
182 `void` as a type argument and as a parameter type in a function type which | 183 for `F<Object, void>` at run time is `==` to the one for `F<void, void>` |
183 is not `identical` to the reified representation of the built-in class | 184 and for `F<void, Object>`.* |
184 `Object`, but they must be equal. This allows implementations to produce | 185 |
185 better diagnostic messages, e.g., in case of a runtime error.* | 186 *In case of a dynamic error, implementations are encouraged to emit an |
| 187 error message that includes information about such parts of types being |
| 188 `void` rather than `Object`. Developers will then see types which are |
| 189 similar to the source code declarations. This may be achieved using |
| 190 distinct `Type` objects to represent types such as `F<void, void>` and |
| 191 `F<Object, void>`, comparing equal using `==` but not `identical`.* |
186 | 192 |
187 *This treatment of the reified representation of the type void reinforces | 193 *This treatment of the reified representation of the type void reinforces |
188 the understanding that "voidness" is merely a statically known flag on the | 194 the understanding that "voidness" is merely a statically known flag on the |
189 built-in class `Object`, it is not a separate type. However, for backward | 195 built-in class `Object`. However, for backward compatibility we need to |
190 compatibility we need to treat return types differently.* | 196 treat return types differently in Dart 1.x.* |
191 | |
192 When `void` is specified as the return type of a function, the reified | |
193 representation of the return type is left unspecified. | |
194 | |
195 *There is no way for a Dart program at run time to obtain a reified | |
196 representation of that return type alone, even when the function type as a | |
197 whole may be obtained (e.g., the function type could be evaluated as an | |
198 expression). It is therefore not necessary to reified representation of | |
199 such a return type.* | |
200 | 197 |
201 *It may be possible to use a reflective subsystem (mirrors) to deconstruct | 198 *It may be possible to use a reflective subsystem (mirrors) to deconstruct |
202 a function type whose return type is the type void, but the existing design | 199 a function type whose return type is the type void, but the existing design |
203 of the system library `dart:mirrors` already handles this case by allowing | 200 of the system library `dart:mirrors` already handles this case by allowing |
204 for a type mirror that does not have a reflected type.* | 201 for a type mirror that does not have a reflected type. All in all, the type |
| 202 void does not need to be reified at run time, and it is not reified.* |
205 | 203 |
206 Consider a type _T_ where the type void occurs as an actual type argument | 204 Consider a type _T_ where the type void occurs as an actual type argument |
207 to a generic class, or as a parameter type in a function type. Dynamically, | 205 to a generic class, or as a parameter type in a function type. Dynamically, |
208 the more-specific-than relation (`<<`) and the dynamic subtype relation | 206 the more-specific-than relation (`<<`) and the dynamic subtype relation |
209 (`<:`) between _T_ and other types are determined by the following rule: | 207 (`<:`) between _T_ and other types are determined by the following rule: |
210 the type void is treated as being the built-in class `Object`. | 208 the type void is treated as being the built-in class `Object`. |
211 | 209 |
212 *Dart 1.x does not support generic function types dynamically, because they | 210 *Dart 1.x does not support generic function types dynamically, because they |
213 are erased to regular function types during compilation. Hence there is no | 211 are erased to regular function types during compilation. Hence there is no |
214 need to specify the the typing relations for generic function types. In | 212 need to specify the the typing relations for generic function types. In |
215 Dart 2, the subtype relationship for generic function types follows from | 213 Dart 2, the subtype relationship for generic function types follows from |
216 the rule that `void` is treated as `Object`.* | 214 the rule that `void` is treated as `Object`.* |
217 | 215 |
218 Consider a function type _T_ where the return type is the type void. The | 216 Consider a function type _T_ where the return type is the type void. In |
219 dynamic more-specific-than relation, `<<`, and the dynamic subtype | 217 Dart 1.x, the dynamic more-specific-than relation, `<<`, and the dynamic |
220 relation, `<:`, are determined by the existing rules in the language | 218 subtype relation, `<:`, are determined by the existing rules in the |
221 specification, supplemented by the above rule for handling occurrences of | 219 language specification, supplemented by the above rule for handling |
222 the type void other than as a return type. | 220 occurrences of the type void other than as a return type. In Dart 2 there |
| 221 is no exception for return types: the type void is treated as being the |
| 222 built-in class `Object`. |
223 | 223 |
224 *This ensures backward compatibility for the cases where the type void can | 224 *This ensures backward compatibility for the cases where the type void can |
225 be used already today. It follows that it will be a breaking change to | 225 be used already today. It follows that it will be a breaking change to |
226 switch to a ruleset where the type void even as a return type is treated | 226 switch to a ruleset where the type void even as a return type is treated |
227 like the built-in class Object, i.e. when switching to Dart 2.0. However, | 227 like the built-in class Object, i.e. when switching to Dart 2. However, |
228 the only situation where the semantics differs is as follows: Consider a | 228 the only situation where the semantics differs is as follows: Consider a |
229 situation where a value of type `void Function(...)` is assigned to a | 229 situation where a value of type `void Function(...)` is assigned to a |
230 variable or parameter `x` whose type annotation is `Object Function(...)`, | 230 variable or parameter `x` whose type annotation is `Object Function(...)`, |
231 where the argument types are arbitrary, but such that the assignment is | 231 where the argument types are arbitrary, but such that the assignment is |
232 permitted. In that situation, in checked mode, the assignment will fail | 232 permitted. In that situation, in checked mode, the assignment will fail |
233 with the current semantics, because the type of that value is not a subtype | 233 with the current semantics, because the type of that value is not a subtype |
234 of the type of `x`. The rules in this document preserve that behavior. If | 234 of the type of `x`. The rules in this document preserve that behavior. If |
235 we were to consistently treat the type void as `Object` at run time (as in | 235 we were to consistently treat the type void as `Object` at run time (as in |
236 Dart 2) then this assignment would be permitted (but we would then use | 236 Dart 2) then this assignment would be permitted (but we would then use |
237 voidness preservation to detect and avoid this situation at compile time).* | 237 voidness preservation to detect and avoid this situation at compile time).* |
238 | 238 |
239 *The semantics of checked mode checks involving types where the type void | 239 *The semantics of checked mode checks involving types where the type void |
240 occurs is determined by the semantics of subtype tests, so we do not | 240 occurs is determined by the semantics of subtype tests, so we do not |
241 specify that separately.* | 241 specify that separately.* |
242 | 242 |
243 An instantiation of a generic class `G` is malbounded if it contains `void` | 243 An instantiation of a generic class `G` is malbounded if it contains `void` |
244 as an actual type argument for a formal type parameter, unless that type | 244 as an actual type argument for a formal type parameter, unless that type |
245 parameter does not have a bound, or it has a bound which is the built-in | 245 parameter does not have a bound, or it has a bound which is the built-in |
246 class `Object`, or `dynamic`. | 246 class `Object`, or `dynamic`. |
247 | 247 |
248 *The treatment of malbounded types follows the current specification.* | 248 *The treatment of malbounded types follows the current specification.* |
249 | 249 |
250 ## Static Analysis | 250 ## Static Analysis |
251 | 251 |
252 For the static analysis, the more-specific-than relation, `<<`, and the | 252 For the static analysis, the more-specific-than relation, `<<`, and the |
253 subtype relation, `<:`, are determined by the same rules as described above | 253 subtype relation, `<:`, are determined by the same rules as described above |
254 for the dynamic semantics. | 254 for the dynamic semantics, for both Dart 1.x and Dart 2. |
255 | 255 |
256 *That is, the type void is considered to be equivalent to the built-in | 256 *That is, the type void is considered to be equivalent to the built-in |
257 class `Object`, except when used as a return type, in which case it is | 257 class `Object` in Dart 1.x, except when used as a return type, in which |
258 effectively considered to be a proper supertype of `Object`. As mentioned, | 258 case it is effectively considered to be a proper supertype of `Object`. In |
259 voidness preservation is a separate analysis which is not specified by this | 259 Dart 2 subtyping, the type void is consistently considered to be equivalent |
260 document, but it is intended to be used in the future to track "voidness" | 260 to the built-in class `Object`. As mentioned, this document does not |
261 in types and flag implicit casts wherein information about voidness may | 261 specify voidness preservation; however, when voidness preservation checks |
262 indirectly be lost. With voidness preservation in place, we expect to be | 262 are added we get an effect in Dart 2 which is similar to the special |
263 able to treat the type void as `Object` in all cases during subtype | 263 treatment of void as a return type in Dart 1.x: The function type downcast |
264 checks.* | 264 which will be rejected in Dart 1.x (at run time, with a static warning at |
| 265 compile time) will become a voidness preservation violation, i.e., a |
| 266 compile-time error.* |
265 | 267 |
266 It is a static warning for an expression to have type void, except for the | 268 It is a static warning for an expression to have type void (in Dart 2: a |
267 following situations: | 269 compile-time error), except for the following situations: |
268 | 270 |
269 * In an expressionStatement `e;`, e may have type void. | 271 * In an expressionStatement `e;`, e may have type void. |
270 * In the initialization and increment expressions of a for-loop, | 272 * In the initialization and increment expressions of a for-loop, |
271 `for (e1; e2; e3) {..}`, `e1` and `e3` may have type void. | 273 `for (e1; e2; e3) {..}`, `e1` and `e3` may have type void. |
272 * In a typeCast `e as T`, `e` may have type void. | 274 * In a typeCast `e as T`, `e` may have type void. |
273 * In a parenthesized expression `(e)`, `e` may have type void. | 275 * In a parenthesized expression `(e)`, `e` may have type void. |
274 * In a return statement `return e;`, when the return type of the innermost | 276 * In a return statement `return e;`, when the return type of the innermost |
275 enclosing function is the type void, `e` may have type void. | 277 enclosing function is the type void, `e` may have type void. |
276 | 278 |
277 *Note that the parenthesized expression itself has type void, so it is | 279 *Note that the parenthesized expression itself has type void, so it is |
278 again subject to the same constraints. Also note that we may not allow | 280 again subject to the same constraints. Also note that we may not allow |
279 return statements returning an expression of type void in the future, but | 281 return statements returning an expression of type void in Dart 2, but |
280 it is allowed here for backward compatibility.* | 282 it is allowed here for backward compatibility.* |
281 | 283 |
| 284 *The value yielded by an expression of type void must be discarded (and |
| 285 hence ignored), except when explicitly subjected to a type cast. This |
| 286 "makes it hard to use a meaningless value", but leaves a small escape hatch |
| 287 open for the cases where the developer knows that the typing misrepresents |
| 288 the actual situation.* |
| 289 |
282 During bounds checking, it is possible that a bound of a formal type | 290 During bounds checking, it is possible that a bound of a formal type |
283 parameter of a generic class or function is statically known to be the type | 291 parameter of a generic class or function is statically known to be the type |
284 void. In this case, the bound is considered to be the built-in class | 292 void. In this case, the bound is considered to be the built-in class |
285 `Object`. | 293 `Object`. |
286 | 294 |
| 295 In Dart 2, it is a compile-time error when a method declaration _D2_ with |
| 296 return type void overrides a method declaration _D1_ whose return type is |
| 297 not void. |
| 298 |
| 299 *This rule is a special case of voidness preservation, which is needed in |
| 300 order to maintain the discipline which arises naturally from the function |
| 301 type subtype rules in Dart 1.x concerning void as a return type.* |
| 302 |
287 ## Discussion | 303 ## Discussion |
288 | 304 |
289 Expressions derived from typeCast and typeTest do not support `void` as the | 305 Expressions derived from typeCast and typeTest do not support `void` as the |
290 target type. We have omitted support for this situation because we consider | 306 target type. We have omitted support for this situation because we consider |
291 it to be useless. If void is passed indirectly via a type variable `T` then | 307 it to be useless. If void is passed indirectly via a type variable `T` then |
292 `e as T`, `e is T`, and `e is! T` will treat `T` like `Object`. In general, | 308 `e as T`, `e is T`, and `e is! T` will treat `T` like `Object`. In general, |
293 the rationale is that the type void admits all values (because it is just | 309 the rationale is that the type void admits all values (because it is just |
294 `Object` plus a "static voidness flag"), but values of type void should be | 310 `Object` plus a "static voidness flag"), but the value of expressions of |
295 discarded. | 311 type void should be discarded. So there is no point in *obtaining* the type |
| 312 void for a given expression which already has a different type. |
296 | 313 |
297 The treatment of bounds is delicate. We syntactically prohibit `void` as a | 314 The treatment of bounds is delicate. We syntactically prohibit `void` as a |
298 bound of a formal type parameter of a generic class or function. It is | 315 bound of a formal type parameter of a generic class or function. It is |
299 possible to pass the type void as an actual type argument to a generic | 316 possible to pass the type void as an actual type argument to a generic |
300 class, and that type argument might in turn be used as the bound of another | 317 class, and that type argument might in turn be used as the bound of another |
301 formal type parameter of the class, or of a generic function in the | 318 formal type parameter of the class, or of a generic function in the |
302 class. It would be possible to make it a compile-time error to pass `void` | 319 class. It would be possible to make it a compile-time error to pass `void` |
303 as a type argument to a generic class where it will be used as a bound, but | 320 as a type argument to a generic class where it will be used as a bound, but |
304 this would presumably require a transitive traversal of all generic classes | 321 this would require a transitive traversal of all generic classes and |
305 and functions where the corresponding formal type parameter is passed on to | 322 functions where the corresponding formal type parameter is passed on to |
306 other generic classes or functions, which would be highly brittle: A tiny | 323 other generic classes or functions, which would be highly brittle: A tiny |
307 change to a generic class or function could break code far away. So we do | 324 change to a generic class or function could break code far away. So we do |
308 not wish to prevent formal type parameter bounds from indirectly becoming | 325 not wish to prevent formal type parameter bounds from indirectly becoming |
309 the type void. This motivated the decision to treat such a void-valued | 326 the type void. This motivated the decision to treat such a void-valued |
310 bound as `Object`. | 327 bound as `Object`. |
311 | 328 |
312 ## Updates | 329 ## Updates |
313 | 330 |
314 * August 16h 2017: Removed exceptions allowing `e is T` and `e is! T`. | 331 * August 22nd 2017: Reworded specification of reified types to deal with |
| 332 only such values which may be obtained at run time (previously mentioned |
| 333 some entities which may not exist). Added one override rule. |
| 334 |
| 335 * August 17th 2017: Several parts clarified. |
| 336 |
| 337 * August 16th 2017: Removed exceptions allowing `e is T` and `e is! T`. |
315 | 338 |
316 * August 9th 2017: Transferred to SDK repo, docs/language/informal. | 339 * August 9th 2017: Transferred to SDK repo, docs/language/informal. |
317 | 340 |
318 * July 16th 2017: Reformatted as a gist. | 341 * July 16th 2017: Reformatted as a gist. |
319 | 342 |
320 * June 13th 2017: Compile-time error for using a void value was changed to | 343 * June 13th 2017: Compile-time error for using a void value was changed to |
321 static warning. | 344 static warning. |
322 * June 12th 2017: Grammar changed extensively, to use | 345 |
323 `typeNotVoid` rather than | 346 * June 12th 2017: Grammar changed extensively, to use `typeNotVoid` |
324 `voidOrType`. | 347 rather than `voidOrType`. |
325 * June 5th 2017: Added `typeCast` and | 348 |
326 `typeTest` to the locations where void | 349 * June 5th 2017: Added `typeCast` and `typeTest` to the locations where |
327 expressions may occur. | 350 void expressions may occur. |
OLD | NEW |