Generalized void informal spec clarified in several locations.

docs/language/informal/generalized-void.md

 ## Feature: Generalized Void
 
 Author: eernst@
 
 **Status**: Under implementation.
 
 **This document** is an informal specification of the generalized support
 in Dart 1.x for the type `void`. Dart 2 will have a very similar kind of
 generalized support for `void`, without the function type subtype exception
 that this feature includes for backward compatibility in Dart 1.x. This
@@ skipping 12 matching lines @@
 used to indicate that the visit is performed for its side-effects
 alone. The generalized void feature includes mechanisms to help developers
 avoid using such a value.
 
 In general, situations where it may be desirable to use `void` as
 a type argument arise when the corresponding formal type variable is used
 covariantly. For instance, the class `Future<T>` uses return types
 like `Future<T>` and `Stream<T>`, and it uses `T` as a parameter type of a
 callback in the method `then`.
 
-Note that is not technically dangerous to use a value of type `void`, it
-does not violate any constraints at the level of the language semantics.
-Developers just made the decision to declare that the value is useless,
-based on the program logic. Hence, there is **no requirement** for the
-generalized void mechanism to be strict and **sound**. However, it is the
-intention that the mechanism should be sufficiently strict to make the
-mechanism helpful and non-frustrating in practice.
+Note that it is not technically dangerous to use a value of type `void`,
+doing so does not violate any constraints at the level of the language
+semantics.  By using the type `void`, developers just indicate that the
+value of the corresponding expression evaluation is useless. Hence, there

[Lasse Reichstein Nielsen, 2017/08/22 05:31:06]

Maybe: "useless and unspecified"

[eernst, 2017/08/22 09:09:46]

Adjusted to 'meaningless'.

+is **no requirement** for the generalized void mechanism to be strict and
+**sound**. However, it is the intention that the mechanism should be
+sufficiently sound to make the mechanism helpful and non-frustrating in
+practice.
 
 No constraints are imposed on which values may be given type `void`, so in
 that sense `void` can be considered to be just another name for the type
-`Object`, flagged as useless. Note that this is an approximate rule (in
-Dart 1.x), it fails to hold for function types.
+`Object`, flagged as useless. Note that this is an approximate rule in
+Dart 1.x, it fails to hold for function types; it does hold in Dart 2.
 
 The mechanisms helping developers to avoid using values of type `void` are
 divided into **two phases**. This document specifies the first phase.
 
 The **first phase** uses restrictions which are based on syntactic criteria
 in order to ensure that direct usage of a value of type `void` is a static
 warning (in Dart 2: an error). A few exceptions are allowed, e.g., type
 casts, such that developers can explicitly make the choice to use such a
 value. The general rule is that all values of type `void` must be
-discarded.
+ignored.
 
 The **second phase** will deal with casts and preservation of
 voidness. Some casts will cause derived expressions to switch from having
 type `void` to having some other type, and hence those casts introduce the
 possibility that "a void value" will get passed and used. Here is an
 example:
 
 ```dart
 class A<T> { T foo(); }
 A<Object> a = new A<void>(); // Violates voidness preservation.
-var x = a.foo(); // Use a "void value", with static type Object.
+var x = a.foo(); // Use a "void value", now with static type Object.
 ```
 
 We intend to introduce a **voidness preservation analysis** (which is
 similar to a small type system) to keep track of such situations. As
 mentioned, the second phase is **not specified in this document**. Voidness
 preservation is a purely static analysis, and there are no plans to
 introduce dynamic checking for it.
 
 ## Syntax
 
@@ skipping 91 matching lines @@
 
 *Conversely, `void` cannot denote any other entity than the type void:
 `void` cannot occur as the declared name of any declaration (including
 library prefixes, types, variables, parameters, etc.). This implies that
 `void` is not subject to scoped lookup, and the name is not exported by any
 system library. Similarly, it can never be accessed using a prefixed
 expression (`p.void`). Hence, `void` has a fixed meaning everywhere in all
 Dart programs, and it can only occur as a stand-alone word.*
 
 When `void` is passed as an actual type argument to a generic class or a
-generic function, and when the type void occurs as a parameter type in a
-function type, the reified representation is equal (according to `==`) to
-the reified representation of the built-in class `Object`.
+generic function invocation, and when the type void occurs as a parameter
+type in a function type, the reified representation is equal (according to

[Lasse Reichstein Nielsen, 2017/08/22 05:31:06]

Consider: equal -> equivalent
We use "equivalent" below.

[Lasse Reichstein Nielsen, 2017/08/22 05:31:07]

What does it mean to "occur as a parameter type" in a function type? I'd say
"Function(void)", but there is nothing reified about that one, so I'm not sure
what this is saying.

[eernst, 2017/08/22 09:09:46]

Done.

+`==`) to the reified representation of the built-in class `Object`.
 
 *It is encouraged for an implementation to use a reified representation for

[Lasse Reichstein Nielsen, 2017/08/22 05:31:06]

Wording, consider: "An implementation is encouraged to .."
(Shorter and more direct, I'm trying to avoid using "it" too much myself :).

 `void` as a type argument and as a parameter type in a function type which
 is not `identical` to the reified representation of the built-in class
 `Object`, but they must be equal. This allows implementations to produce
 better diagnostic messages, e.g., in case of a runtime error.*
 
 *This treatment of the reified representation of the type void reinforces
 the understanding that "voidness" is merely a statically known flag on the
 built-in class `Object`, it is not a separate type. However, for backward
 compatibility we need to treat return types differently.*
 
@@ skipping 25 matching lines @@
 
 Consider a function type _T_ where the return type is the type void. The
 dynamic more-specific-than relation, `<<`, and the dynamic subtype
 relation, `<:`, are determined by the existing rules in the language
 specification, supplemented by the above rule for handling occurrences of
 the type void other than as a return type.
 
 *This ensures backward compatibility for the cases where the type void can
 be used already today. It follows that it will be a breaking change to
 switch to a ruleset where the type void even as a return type is treated
-like the built-in class Object, i.e. when switching to Dart 2.0. However,
+like the built-in class Object, i.e. when switching to Dart 2. However,
 the only situation where the semantics differs is as follows: Consider a
 situation where a value of type `void Function(...)` is assigned to a
 variable or parameter `x` whose type annotation is `Object Function(...)`,
 where the argument types are arbitrary, but such that the assignment is
 permitted. In that situation, in checked mode, the assignment will fail
 with the current semantics, because the type of that value is not a subtype
 of the type of `x`. The rules in this document preserve that behavior. If
 we were to consistently treat the type void as `Object` at run time (as in
 Dart 2) then this assignment would be permitted (but we would then use
 voidness preservation to detect and avoid this situation at compile time).*
 
 *The semantics of checked mode checks involving types where the type void
 occurs is determined by the semantics of subtype tests, so we do not
 specify that separately.*
 
 An instantiation of a generic class `G` is malbounded if it contains `void`
 as an actual type argument for a formal type parameter, unless that type
 parameter does not have a bound, or it has a bound which is the built-in
 class `Object`, or `dynamic`.
 
 *The treatment of malbounded types follows the current specification.*
 
 ## Static Analysis
 
 For the static analysis, the more-specific-than relation, `<<`, and the
 subtype relation, `<:`, are determined by the same rules as described above
 for the dynamic semantics.
 
 *That is, the type void is considered to be equivalent to the built-in

[Lasse Reichstein Nielsen, 2017/08/22 05:31:06]

Here we use "equivalent".

-class `Object`, except when used as a return type, in which case it is
-effectively considered to be a proper supertype of `Object`. As mentioned,
-voidness preservation is a separate analysis which is not specified by this
-document, but it is intended to be used in the future to track "voidness"
-in types and flag implicit casts wherein information about voidness may
-indirectly be lost. With voidness preservation in place, we expect to be
-able to treat the type void as `Object` in all cases during subtype
-checks.*
+class `Object` in Dart 1.x, except when used as a return type, in which
+case it is effectively considered to be a proper supertype of `Object`. In
+Dart 2 subtyping, the type void is consistently considered to be equivalent
+to the built-in class `Object`. As mentioned, this document does not
+specify voidness preservation; however, when voidness preservation checks
+are added we get an effect in Dart 2 which is similar to the special
+treatment of void as a return type in Dart 1.x: The function type downcast
+which will be rejected in Dart 1.x (at run time, with a static warning at
+compile time) will become a voidness preservation violation, i.e., a
+compile-time error.*
 
-It is a static warning for an expression to have type void, except for the
-following situations:
+It is a static warning for an expression to have type void (in Dart 2: a
+compile-time error), except for the following situations:
 
 *   In an expressionStatement `e;`, e may have type void.
 *   In the initialization and increment expressions of a for-loop,
     `for (e1; e2; e3) {..}`, `e1` and `e3` may have type void.
 *   In a typeCast `e as T`, `e` may have type void.
 *   In a parenthesized expression `(e)`, `e` may have type void.
 *   In a return statement `return e;`, when the return type of the innermost
     enclosing function is the type void, `e` may have type void.
 
 *Note that the parenthesized expression itself has type void, so it is
 again subject to the same constraints. Also note that we may not allow
-return statements returning an expression of type void in the future, but
+return statements returning an expression of type void in Dart 2, but
 it is allowed here for backward compatibility.*
 
+*The value yielded by an expression of type void must be discarded (and
+hence ignored), except when explicitly subjected to a type cast. This
+"makes it hard to use useless values", but leaves a small escape hatch open
+for the cases where the developer knows that the typing misrepresents the
+actual situation.*
+
 During bounds checking, it is possible that a bound of a formal type
 parameter of a generic class or function is statically known to be the type
 void. In this case, the bound is considered to be the built-in class
 `Object`.
 
 ## Discussion
 
 Expressions derived from typeCast and typeTest do not support `void` as the
 target type. We have omitted support for this situation because we consider
 it to be useless. If void is passed indirectly via a type variable `T` then
 `e as T`, `e is T`, and `e is! T` will treat `T` like `Object`. In general,
 the rationale is that the type void admits all values (because it is just
 `Object` plus a "static voidness flag"), but values of type void should be
-discarded.
+discarded. So there is no point in *obtaining* the type void for a given
+expression which already has a different type.
 
 The treatment of bounds is delicate. We syntactically prohibit `void` as a
 bound of a formal type parameter of a generic class or function. It is
 possible to pass the type void as an actual type argument to a generic
 class, and that type argument might in turn be used as the bound of another
 formal type parameter of the class, or of a generic function in the
 class. It would be possible to make it a compile-time error to pass `void`
 as a type argument to a generic class where it will be used as a bound, but
-this would presumably require a transitive traversal of all generic classes
-and functions where the corresponding formal type parameter is passed on to
+this would require a transitive traversal of all generic classes and
+functions where the corresponding formal type parameter is passed on to
 other generic classes or functions, which would be highly brittle: A tiny
 change to a generic class or function could break code far away. So we do
 not wish to prevent formal type parameter bounds from indirectly becoming
 the type void. This motivated the decision to treat such a void-valued
 bound as `Object`.
 
 ## Updates
 
-*   August 16h 2017: Removed exceptions allowing `e is T` and `e is! T`.
+*   August 17th 2017: Several parts clarified.
+
+*   August 16th 2017: Removed exceptions allowing `e is T` and `e is! T`.
 
 *   August 9th 2017: Transferred to SDK repo, docs/language/informal.
 
 *   July 16th 2017: Reformatted as a gist.
 
 *   June 13th 2017: Compile-time error for using a void value was changed to
     static warning.
-*   June 12th 2017: Grammar changed extensively, to use
-    `typeNotVoid` rather than
-    `voidOrType`.
-*   June 5th 2017: Added `typeCast` and
-    `typeTest` to the locations where void
-    expressions may occur.
+
+*   June 12th 2017: Grammar changed extensively, to use `typeNotVoid`
+    rather than `voidOrType`.
+
+*   June 5th 2017: Added `typeCast` and `typeTest` to the locations where
+    void expressions may occur.