OLD | NEW |
(Empty) | |
| 1 ## Feature: Generalized Void |
| 2 |
| 3 Author: eernst@ |
| 4 |
| 5 **Status**: Under implementation. |
| 6 |
| 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 |
| 9 generalized support for `void`, without the function type subtype exception |
| 10 that this feature includes for backward compatibility in Dart 1.x. This |
| 11 document specifies the feature for Dart 1.x and indicates how Dart 2 |
| 12 differs at relevant points. |
| 13 |
| 14 **The feature** described here, *generalized void*, allows for using the |
| 15 type `void` as a type annotation and as a type argument. |
| 16 |
| 17 The **motivation** for allowing the extended usage is that it helps |
| 18 developers state the intent that a particular **value should be |
| 19 ignored**. For example, a `Future<void>` may be awaited in order to satisfy |
| 20 ordering dependencies in the execution, but no useful value will be |
| 21 available at completion. Similarly, a `Visitor<void>` (where we assume the |
| 22 type argument is used to describe a value returned by the visitor) may be |
| 23 used to indicate that the visit is performed for its side-effects |
| 24 alone. The generalized void feature includes mechanisms to help developers |
| 25 avoid using such a value. |
| 26 |
| 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 |
| 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 |
| 31 callback in the method `then`. |
| 32 |
| 33 Note that is not technically dangerous to use a value of type `void`, it |
| 34 does not violate any constraints at the level of the language semantics. |
| 35 Developers just made the decision to declare that the value is useless, |
| 36 based on the program logic. Hence, there is **no requirement** for the |
| 37 generalized void mechanism to be strict and **sound**. However, it is the |
| 38 intention that the mechanism should be sufficiently strict to make the |
| 39 mechanism helpful and non-frustrating in practice. |
| 40 |
| 41 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 `Object`, flagged as useless. Note that this is an approximate rule (in |
| 44 Dart 1.x), it fails to hold for function types. |
| 45 |
| 46 The mechanisms helping developers to avoid using values of type `void` are |
| 47 divided into **two phases**. This document specifies the first phase. |
| 48 |
| 49 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 |
| 51 warning (in Dart 2: an error). A few exceptions are allowed, e.g., type |
| 52 casts, such that developers can explicitly make the choice to use such a |
| 53 value. The general rule is that all values of type `void` must be |
| 54 discarded. |
| 55 |
| 56 The **second phase** will deal with casts and preservation of |
| 57 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 |
| 59 possibility that "a void value" will get passed and used. Here is an |
| 60 example: |
| 61 |
| 62 ```dart |
| 63 class A<T> { T foo(); } |
| 64 A<Object> a = new A<void>(); // Violates voidness preservation. |
| 65 var x = a.foo(); // Use a "void value", with static type Object. |
| 66 ``` |
| 67 |
| 68 We intend to introduce a **voidness preservation analysis** (which is |
| 69 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 |
| 71 preservation is a purely static analysis, and there are no plans to |
| 72 introduce dynamic checking for it. |
| 73 |
| 74 ## Syntax |
| 75 |
| 76 The reserved word `void` remains a reserved word, but it will now be usable |
| 77 in additional contexts. Below are the grammar rules affected by this |
| 78 change. New grammar rules are marked NEW, other grammar rules are |
| 79 modified. Unchanged alternatives in a rule are shown as `...`. The grammar |
| 80 rules used as a starting point for this syntax are taken from the language |
| 81 specification as of June 2nd, 2017 (git commit 0603b18). |
| 82 |
| 83 ``` |
| 84 typeNotVoid ::= // NEW |
| 85 typeName typeArguments? |
| 86 type ::= // ENTIRE RULE MODIFIED |
| 87 typeNotVoid | 'void' |
| 88 redirectingFactoryConstructorSignature ::= |
| 89 'const'? 'factory' identifier ('.' identifier)? |
| 90 formalParameterList `=' typeNotVoid ('.' identifier)? |
| 91 superclass ::= |
| 92 'extends' typeNotVoid |
| 93 mixinApplication ::= |
| 94 typeNotVoid mixins interfaces? |
| 95 typeParameter ::= |
| 96 metadata identifier ('extends' typeNotVoid)? |
| 97 newExpression ::= |
| 98 'new' typeNotVoid ('.' identifier)? arguments |
| 99 constObjectExpression ::= |
| 100 'const' typeNotVoid ('.' identifier)? arguments |
| 101 typeTest ::= |
| 102 isOperator typeNotVoid |
| 103 typeCast ::= |
| 104 asOperator typeNotVoid |
| 105 onPart ::= |
| 106 catchPart block | |
| 107 'on' typeNotVoid catchPart? block |
| 108 typeNotVoidList ::= |
| 109 typeNotVoid (',' typeNotVoid)* |
| 110 mixins ::= |
| 111 'with' typeNotVoidList |
| 112 interfaces ::= |
| 113 'implements' typeNotVoidList |
| 114 functionSignature ::= |
| 115 metadata type? identifier formalParameterList |
| 116 functionFormalParameter ::= |
| 117 metadata 'covariant'? type? identifier formalParameterList |
| 118 operatorSignature ::= |
| 119 type? 'operator' operator formalParameterList |
| 120 getterSignature ::= |
| 121 type? 'get' identifier |
| 122 setterSignature ::= |
| 123 type? 'set' identifier formalParameterList |
| 124 topLevelDefinition ::= |
| 125 ... |
| 126 type? 'get' identifier functionBody | |
| 127 type? 'set' identifier formalParameterList functionBody | |
| 128 ... |
| 129 functionPrefix ::= |
| 130 type? identifier |
| 131 ``` |
| 132 |
| 133 The rule for `returnType` in the grammar is deleted. |
| 134 |
| 135 *This is because we can now use `type`, which derives the same expressions |
| 136 as `returnType` used to derive. In that sense, some of these grammar |
| 137 modifications are renames. Note that the grammar contains known mistakes, |
| 138 especially concerned with the placement of `metadata`. This document makes |
| 139 no attempt to correct those mistakes, that is a separate issue.* |
| 140 |
| 141 *A complete grammar which includes support for generalized void is |
| 142 available in the file Dart.g |
| 143 from |
| 144 [https://codereview.chromium.org/2688903004/](https://codereview.chromium.org/26
88903004/).* |
| 145 |
| 146 ## Dynamic semantics |
| 147 |
| 148 There are no values at run time whose dynamic type is the type void. |
| 149 |
| 150 *This implies that it is never required for the getter `runtimeType` in the |
| 151 built-in class `Object` to return a reified representation of the type |
| 152 void. Note, however, that apart from the fact that usage is restricted for |
| 153 values with the type void, it is possible for an expression of type void to |
| 154 evaluate to any value. In that sense, every value has the type void, it is |
| 155 just not the only type that it has, and loosely speaking it is not the most |
| 156 specific type.* |
| 157 |
| 158 There is no value which is the reified representation of the type void at |
| 159 run time. |
| 160 |
| 161 *Syntactically, `void` cannot occur as an expression, and hence expression |
| 162 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 |
| 164 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 |
| 166 parameter, no other term can denote the type void.* |
| 167 |
| 168 *Conversely, `void` cannot denote any other entity than the type void: |
| 169 `void` cannot occur as the declared name of any declaration (including |
| 170 library prefixes, types, variables, parameters, etc.). This implies that |
| 171 `void` is not subject to scoped lookup, and the name is not exported by any |
| 172 system library. Similarly, it can never be accessed using a prefixed |
| 173 expression (`p.void`). Hence, `void` has a fixed meaning everywhere in all |
| 174 Dart programs, and it can only occur as a stand-alone word.* |
| 175 |
| 176 When `void` is passed as an actual type argument to a generic class or a |
| 177 generic function, and when the type void occurs as a parameter type in a |
| 178 function type, the reified representation is equal (according to `==`) to |
| 179 the reified representation of the built-in class `Object`. |
| 180 |
| 181 *It is encouraged for an implementation to use a reified representation for |
| 182 `void` as a type argument and as a parameter type in a function type which |
| 183 is not `identical` to the reified representation of the built-in class |
| 184 `Object`, but they must be equal. This allows implementations to produce |
| 185 better diagnostic messages, e.g., in case of a runtime error.* |
| 186 |
| 187 *This treatment of the reified representation of the type void reinforces |
| 188 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 |
| 190 compatibility we need to treat return types differently.* |
| 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 |
| 201 *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 |
| 203 of the system library `dart:mirrors` already handles this case by allowing |
| 204 for a type mirror that does not have a reflected type.* |
| 205 |
| 206 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, |
| 208 the more-specific-than relation (`<<`) and the dynamic subtype relation |
| 209 (`<:`) between _T_ and other types are determined by the following rule: |
| 210 the type void is treated as being the built-in class `Object`. |
| 211 |
| 212 *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 |
| 214 need to specify the the typing relations for generic function types. In |
| 215 Dart 2, the subtype relationship for generic function types follows from |
| 216 the rule that `void` is treated as `Object`.* |
| 217 |
| 218 Consider a function type _T_ where the return type is the type void. The |
| 219 dynamic more-specific-than relation, `<<`, and the dynamic subtype |
| 220 relation, `<:`, are determined by the existing rules in the language |
| 221 specification, supplemented by the above rule for handling occurrences of |
| 222 the type void other than as a return type. |
| 223 |
| 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 |
| 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, |
| 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 |
| 230 variable or parameter `x` whose type annotation is `Object Function(...)`, |
| 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 |
| 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 |
| 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 |
| 237 voidness preservation to detect and avoid this situation at compile time).* |
| 238 |
| 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 |
| 241 specify that separately.* |
| 242 |
| 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 |
| 245 parameter does not have a bound, or it has a bound which is the built-in |
| 246 class `Object`, or `dynamic`. |
| 247 |
| 248 *The treatment of malbounded types follows the current specification.* |
| 249 |
| 250 ## Static Analysis |
| 251 |
| 252 For the static analysis, the more-specific-than relation, `<<`, and the |
| 253 subtype relation, `<:`, are determined by the same rules as described above |
| 254 for the dynamic semantics. |
| 255 |
| 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 |
| 258 effectively considered to be a proper supertype of `Object`. As mentioned, |
| 259 voidness preservation is a separate analysis which is not specified by this |
| 260 document, but it is intended to be used in the future to track "voidness" |
| 261 in types and flag implicit casts wherein information about voidness may |
| 262 indirectly be lost. With voidness preservation in place, we expect to be |
| 263 able to treat the type void as `Object` in all cases during subtype |
| 264 checks.* |
| 265 |
| 266 It is a static warning for an expression to have type void, except for the |
| 267 following situations: |
| 268 |
| 269 * In an expressionStatement `e;`, e may have type void. |
| 270 * In the initialization and increment expressions of a for-loop, |
| 271 `for (e1; e2; e3) {..}`, `e1` and `e3` may have type void. |
| 272 * In a typeCast `e as T`, `e` may have type void. |
| 273 * In a typeTest `e is T` or `e is! T`, `e` may have type void. |
| 274 * In a parenthesized expression `(e)`, `e` may have type void. |
| 275 * In a return statement `return e;`, when the return type of the innermost |
| 276 enclosing function is the type void, `e` may have type void. |
| 277 |
| 278 *Note that the parenthesized expression itself has type void, so it is |
| 279 again subject to the same constraints. Also note that we may not allow |
| 280 return statements returning an expression of type void in the future, but |
| 281 it is allowed here for backward compatibility.* |
| 282 |
| 283 During bounds checking, it is possible that a bound of a formal type |
| 284 parameter of a generic class or function is statically known to be the type |
| 285 void. In this case, the bound is considered to be the built-in class |
| 286 `Object`. |
| 287 |
| 288 ## Discussion |
| 289 |
| 290 Expressions derived from typeCast and typeTest do not support `void` as the |
| 291 target type. We have omitted support for this situation because we consider |
| 292 it to be useless. If void is passed indirectly via a type variable `T` then |
| 293 `e as T`, `e is T`, and `e is! T` will treat `T` like `Object`. In general, |
| 294 the rationale is that the type void admits all values (because it is just |
| 295 `Object` plus a "static voidness flag"), but values of type void should be |
| 296 discarded. |
| 297 |
| 298 The treatment of bounds is delicate. We syntactically prohibit `void` as a |
| 299 bound of a formal type parameter of a generic class or function. It is |
| 300 possible to pass the type void as an actual type argument to a generic |
| 301 class, and that type argument might in turn be used as the bound of another |
| 302 formal type parameter of the class, or of a generic function in the |
| 303 class. It would be possible to make it a compile-time error to pass `void` |
| 304 as a type argument to a generic class where it will be used as a bound, but |
| 305 this would presumably require a transitive traversal of all generic classes |
| 306 and functions where the corresponding formal type parameter is passed on to |
| 307 other generic classes or functions, which would be highly brittle: A tiny |
| 308 change to a generic class or function could break code far away. So we do |
| 309 not wish to prevent formal type parameter bounds from indirectly becoming |
| 310 the type void. This motivated the decision to treat such a void-valued |
| 311 bound as `Object`. |
| 312 |
| 313 ## Updates |
| 314 |
| 315 * August 9th 2017: Transferred to SDK repo, docs/language/informal. |
| 316 |
| 317 * July 16th 2017: Reformatted as a gist. |
| 318 |
| 319 * June 13th 2017: Compile-time error for using a void value was changed to |
| 320 static warning. |
| 321 * June 12th 2017: Grammar changed extensively, to use |
| 322 `typeNotVoid` rather than |
| 323 `voidOrType`. |
| 324 * June 5th 2017: Added `typeCast` and |
| 325 `typeTest` to the locations where void |
| 326 expressions may occur. |
OLD | NEW |