Transferred the generalized void informal spec to docs/language/informal

docs/language/informal/generalized-void.md

Index: docs/language/informal/generalized-void.md
diff --git a/docs/language/informal/generalized-void.md b/docs/language/informal/generalized-void.md
new file mode 100644
index 0000000000000000000000000000000000000000..8b90bcbc8fec99ff3bbc87b1182d1bf83c0099ca
--- /dev/null
+++ b/docs/language/informal/generalized-void.md
@@ -0,0 +1,324 @@
+## 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
+document specifies the feature for Dart 1.x and indicates how Dart 2
+differs at relevant points.
+
+**The feature** described here, *generalized void*, allows for using the
+type `void` as a type annotation, and as a type argument.

[Lasse Reichstein Nielsen, 2017/08/09 13:41:42]

Not sure there should be a comma here.

[eernst, 2017/08/09 14:30:03]

Done.

+
+The **motivation** for allowing the extended usage is that it helps
+developers state the intent that a particular **value should be
+ignored**. For example, a `Future<void>` may be awaited in order to satisfy
+ordering dependencies in the execution, but no useful value will be
+available at completion. Similarly, a `Visitor<void>` (where we assume the
+type argument is used to describe a value returned by the visitor) may be
+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.

[Lasse Reichstein Nielsen, 2017/08/09 13:41:42]

Is it worth mentioning that the type parameter of `Future` is really
representing a return type, which is why the lack of `Future<void>` hurts so
much when converting from synchronous code to asynchronous?

[eernst, 2017/08/09 14:30:04]

Added a small paragraph mentioning this, and using `Future` as an example.
Interestingly, `Future` _never_ uses `T` contravariantly (of course the value
must be passed to the Future in some concrete `FutureImpl` class, but `Future`
itself doesn't reveal that).

+
+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.
+
+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.
+
+The mechanisms helping developers to avoid using values of type `void` are
+divided into **two phases**. This document specifies the first phase. The
+second phase may be added to Dart 1.x later, or it may only be provided in

[Lasse Reichstein Nielsen, 2017/08/09 13:41:42]

Definitely not going into Dart 1.0, everything we do from now on is Dart 2.

[eernst, 2017/08/09 14:30:03]

Removed the entire sentence. Everything will be about Dart 2 very soon anyway.

+Dart 2.0, depending on the schedule.
+
+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.
+
+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.
+```
+
+We plan to introduce a **voidness preservation analysis** (which is similar

[Lasse Reichstein Nielsen, 2017/08/09 13:41:42]

plan -> intend

[eernst, 2017/08/09 14:30:03]

Done.

+to a small type system) to keep track of such situations. As mentioned, the
+second phase is **not specified in this document**, and it is possible that
+voidness preservation will be checked in Dart 2 and strong mode, but that
+it is never added to Dart 1.x. In any case, voidness preservation is a

[Lasse Reichstein Nielsen, 2017/08/09 13:41:42]

Again, we are past Dart 1.x now.

[eernst, 2017/08/09 14:30:03]

Deleted the part that mentions language versions: '.. this document**. Voidness
preservation is a purely static..'.

+purely static analysis, and there are no plans to introduce dynamic
+checking for it.
+
+## Syntax
+
+The reserved word `void` remains a reserved word, but it will now be usable
+in additional contexts. Below are the grammar rules affected by this
+change. New grammar rules are marked NEW, other grammar rules are
+modified. Unchanged alternatives in a rule are shown as `...`. The grammar
+rules used as a starting point for this syntax are taken from the language
+specification as of June 2nd, 2017 (git commit 0603b18).

[Lasse Reichstein Nielsen, 2017/08/09 13:41:42]

We will need to update this for Function types (which are also not usable as
classes, so typeNotVoid would be typeNotVoidOrFunction).
Is that worth mentioning now?

[eernst, 2017/08/09 14:30:03]

The reference to the spec grammar below (CL 2688903004) shows the interactions
among these two extensions, because it contains both.

+
+```
+typeNotVoid ::= // NEW
+    typeName typeArguments?
+type ::= // ENTIRE RULE MODIFIED
+    typeNotVoid | 'void'
+redirectingFactoryConstructorSignature ::=
+    'const'? 'factory' identifier ('.' identifier)? 
+    formalParameterList `=' typeNotVoid ('.' identifier)?
+superclass ::=
+    'extends' typeNotVoid
+mixinApplication ::=
+    typeNotVoid mixins interfaces?
+typeParameter ::=
+    metadata identifier ('extends' typeNotVoid)?
+newExpression ::=
+    'new' typeNotVoid ('.' identifier)? arguments
+constObjectExpression ::=
+    'const' typeNotVoid ('.' identifier)? arguments
+typeTest ::=
+    isOperator typeNotVoid
+typeCast ::=
+    asOperator typeNotVoid
+onPart ::=
+    catchPart block |
+    'on' typeNotVoid catchPart? block
+typeNotVoidList ::=
+    typeNotVoid (',' typeNotVoid)*
+mixins ::=
+    'with' typeNotVoidList
+interfaces ::=
+    'implements' typeNotVoidList
+functionSignature ::=
+    metadata type? identifier formalParameterList
+functionFormalParameter ::=
+    metadata 'covariant'? type? identifier formalParameterList
+operatorSignature ::=
+    type? 'operator' operator formalParameterList
+getterSignature ::=
+    type? 'get' identifier
+setterSignature ::=
+    type? 'set' identifier formalParameterList
+topLevelDefinition ::=
+    ...
+    type? 'get' identifier functionBody |
+    type? 'set' identifier formalParameterList functionBody |
+    ...
+functionPrefix ::=
+    type? identifier
+```
+
+The rule for `returnType` in the grammar is deleted.
+
+*This is because we can now use `type`, which derives the same expressions
+as `returnType` used to derive. In that sense, some of these grammar
+modifications are renames. Note that the grammar contains known mistakes,
+especially concerned with the placement of `metadata`. This document makes
+no attempt to correct those mistakes, that is a separate issue.*
+
+*A complete grammar which includes support for generalized void is
+available in the file Dart.g
+from
+[https://codereview.chromium.org/2688903004/](https://codereview.chromium.org/2688903004/).*
+
+## Dynamic semantics
+
+There are no values at run time whose dynamic type is the type void.
+
+*This implies that it is never required for the getter `runtimeType` in the
+built-in class `Object` to return a reified representation of the type
+void. Note, however, that apart from the fact that usage is restricted for
+values with the type void, it is possible for an expression of type void to
+evaluate to any value. In that sense, every value has the type void, it is
+just not the only type that it has, and loosely speaking it is not the most
+specific type.*
+
+There is no value which is the reified representation of the type void at
+run time.
+
+*Syntactically, `void` cannot occur as an expression, and hence expression
+evaluation cannot directly yield such a value. However, a formal type
+parameter can be used in expressions, and the actual type argument bound to
+that formal type parameter can be the type void. That case is specified
+explicitly below. Apart from the reserved word `void` and a formal type
+parameter, no other term can denote the type void.*
+
+*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`.
+
+*It is encouraged for an implementation to use a reified representation for
+`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.*
+
+When `void` is specified as the return type of a function, the reified
+representation of the return type is left unspecified.
+
+*There is no way for a Dart program at run time to obtain a reified
+representation of that return type alone, even when the function type as a
+whole may be obtained (e.g., the function type could be evaluated as an
+expression). It is therefore not necessary to reified representation of
+such a return type.*
+
+*It may be possible to use a reflective subsystem (mirrors) to deconstruct
+a function type whose return type is the type void, but the existing design
+of the system library `dart:mirrors` already handles this case by allowing
+for a type mirror that does not have a reflected type.*
+
+Consider a type _T_ where the type void occurs as an actual type argument
+to a generic class, or as a parameter type in a function type. Dynamically,
+the more-specific-than relation (`<<`) and the dynamic subtype relation
+(`<:`) between _T_ and other types are determined by the following rule:
+the type void is treated as being the built-in class `Object`.
+
+*Dart 1.x does not support generic function types dynamically, because they
+are erased to regular function types during compilation. Hence there is no
+need to specify the the typing relations for generic function types. In
+Dart 2, the subtype relationship for generic function types follows from
+the rule that `void` is treated as `Object`.*
+
+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,
+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
+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.*
+
+It is a static warning for an expression to have type void, except for the

[Lasse Reichstein Nielsen, 2017/08/09 13:41:42]

In Dart 2, this will be a compile-time error, so just switch to that now.

[eernst, 2017/08/09 14:30:03]

Ah, that's funny: I had 'compile-time error' here until June 13th because we
might as well make it an error now (given that it would become an error in Dart
2 anyway), but then I was asked to change it to static warning, in order to make
it fit in Dart 1.x.

So right now I just have two requests (yours and Florian's), and I don't have
any strong opinions on the issue myself, so I'll keep it unchanged and then we
can go and fix it as needed. ;)

+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 typeTest `e is T` or `e is! 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
+it is allowed here for backward compatibility.*
+
+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.
+
+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
+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 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.