From d8f44d02de9c0f2807dd1e592c164efd3fd0f6fc Mon Sep 17 00:00:00 2001
From: Leaf Petersen <leafp@google.com>
Date: Fri, 29 Mar 2019 15:30:32 -0700
Subject: [PATCH 01/12] Add initial proposal for NNBD feature spec

---
 .../feature-specification.md                  | 352 ++++++++++++++++++
 1 file changed, 352 insertions(+)
 create mode 100644 working/0110-incremental-sound-nnbd/feature-specification.md

diff --git a/working/0110-incremental-sound-nnbd/feature-specification.md b/working/0110-incremental-sound-nnbd/feature-specification.md
new file mode 100644
index 0000000000..1daade25a2
--- /dev/null
+++ b/working/0110-incremental-sound-nnbd/feature-specification.md
@@ -0,0 +1,352 @@
+# Sound non-nullable (by default) types with incremental migration 
+
+Author: leafp@google.com
+
+Status: Draft
+
+This is the proposed specification for [sound non-nullable by default types](http://github.com/dart-lang/language/issues/110).
+Discussion of this proposal should take place in [Issue 110](http://github.com/dart-lang/language/issues/100).
+
+Discussion issues on specific topics related to this proposal are [here](https://github.com/dart-lang/language/issues?utf8=%E2%9C%93&q=is%3Aissue+label%3Annbd+)
+
+The motivations for the feature along with the migration plan and strategy are
+discussed in more detail in
+the
+[roadmap](https://github.com/dart-lang/language/blob/master/working/0110-incremental-sound-nnbd/roadmap.md).
+
+This proposal draws on the proposal that Patrice Chalin wrote
+up [here](https://github.com/dart-archive/dart_enhancement_proposals/issues/30),
+and on the proposal that Bob Nystrom wrote
+up
+[here](https://github.com/dart-lang/language/blob/master/resources/old-non-nullable-types.md).
+
+
+## Syntax
+
+The grammar of types is extended to allow any type to be suffixed with a `?`
+(e.g. `int ?`) indicating the nullable version of that type.
+
+A new primitive type `Never`.  This type is denoted by the built-in type
+declaration `Never`, with the same syntactic and scoping treatment as with other
+built-in types such as `dynamic`.
+
+The grammer of expressions is extended to allow any expression to be suffixed
+with a `!`.
+
+The grammer of static and instance fields and static and local variables is
+extended to allow any declaration to include the modifer `lazy`.
+
+The grammar of function types is extended to allow an additional group of named
+parameters prefaced with the word `required` (e.g. `int Function(int, {int?
+y}, required {int z})`.
+
+The grammar of function/method/closure declarations is extended to allow an
+additional group of named parameters prefaced with the word `required`
+(e.g. `int f(int x, {int?  y}, required {int z})`.
+
+
+### Grammatical ambiguities and clarifications.
+
+#### Nested nullable types
+
+The grammar for types does not allow multiple successive `?` operators on a
+type.  That is, the grammar for types is
+
+```
+type' ::= functionType
+          | qualified typeArguments? 
+
+type ::= type' `?`?
+```
+
+#### Conditional expression ambiguities
+
+Conditional expressions inside of braces are ambiguous between sets and maps.
+That is, `{ a as int ? - 3 : 3 }` can be parsed as a set literal `{ (a as int)
+? - 3 : 3 }` or as a map literal `{ (a as int ?) - 3 : 3 }`.  Parsers will
+prefer the former parse over the latter.
+
+The same is true for `{ a is int ? - 3 : 3 }`.
+
+The same is true for `{ int ? - 3 : 3 }` if we allow this.
+
+
+## Static semantics
+
+
+### Static errors
+
+We say that a type `T` is **nullable** if `Null <: T`.  This is equivalent to
+the syntactic criterion that `T` is any of:
+  - `Null`
+  - `S?` for some `S`
+  - `FutureOr<S>` for some `S` where `S` is nullable
+  - `dynamic`
+  - `void`
+  - `X extends Null`
+
+We say that a type `T` is **non-nullable** if `T <: Object`.  This is equivalent
+to the syntactic criterion that `T` is any of:
+  - `Object`, `int`, `bool`, `Never`
+  - Any class type or generic class type
+  - `FutureOr<S>` where `S` is non-nullable
+  - `X extends S` where `S` is non-nullable
+  - `X & S` where `S` is non-nullable
+
+Note that there are types which are neither nullable nor non-nullable.  For
+example `X extends T` where `T` is nullable is neither nullable nor
+non-nullable.
+
+We say that a type `T` is **potentially nullable** if `T` is not non-nullable.
+Note that this is different from saying that `T` is nullable.  For example, a
+type variable `X extends Object?` is a type which is potentially nullable but
+not nullable.
+
+We say that a type `T` is **potentially non-nullable** if `T` is not nullable.
+Note that this is different from saying that `T` is non-nullable.  For example,
+a type variable `X extends Object?` is a type which is potentially non-nullable
+but not non-nullable.
+
+It is an error to call a method, setter, getter or operator on an expression
+whose type is potentially nullable and not `dynamic`, except for the methods,
+setters, getters, and operators on `Object`.
+
+It is an error to read a field or tear off a method from an expression whose
+type is potentially nullable and not `dynamic`, except for the methods and
+fields on `Object`.
+
+It is an error to call an expression whose type is potentially nullable and not
+`dynamic`.
+
+It is an error for a top level variable, static field, or instance field with no
+static initializer to have a potentially nullable type unless the variable or
+field is marked with the `lazy` modifier.
+
+It is an error if a local variable that is potentially non-nullable and is not
+marked `lazy` is used before it is definitely assigned (see Definite Assignment
+below).
+
+It is an error if a method, function, getter, or closure with a potentially
+non-nullable return type does not definitely complete (see Definite Completion
+below).
+
+It is an error if an optional parameter (named or otherwise) with no default
+value has a potentially non-nullable type.
+
+It is an error if a required named parameter has a default value.
+
+It is an error if a named parameter that is part of a `required` group is not
+bound to an argument at a call site.
+
+It is an error to call the default `List` constructor with a length argument and
+a type argument which is potentially non-nullable.
+
+For the purposes of errors and warnings, the null aware operators `?.` and `?..`
+are checked as if the receiver of the operator had non-nullable type.
+
+It is an error for a class to extend, implement, or mixin a type of the form
+`T?` for any `T`.
+
+It is an error for a class to extend, implement, or mixin the type `Never`.
+
+It is an error to call a method, setter, or getter on a receiver of static type
+`Never` (including via a null aware operator).
+
+It is an error to apply an expression of `Never` in the function position in a
+function call.
+
+It is an error if the static type of `e` in the expression `throw e` is
+potentially nullable.
+
+It is not an error for the body of a `lazy` field to reference `this`.
+
+It is an error for a formal parameter to be declared `lazy`.
+
+It is an error if the type `T` in the **on-catch** clause `on T catch` is
+potentially nullable.
+
+### Assignability
+
+The definition of assignability is changed as follows.  
+
+A type `T` is **assignable** to a type `S` if `T` is `dynamic`, or if `S` is a
+subtype of `T`.
+
+### Generics
+
+The default bound of generic type parameters is treated as `Object?`.
+
+### Type promotion, Definite Assignment, and Definite Completion
+
+### Null promotion
+
+The machinery of type promotion is extended to promote the type of variables
+based on nullability checks subject to the same set of restrictions as normal
+promotion.  The relevant checks and the types they are considered to promote to
+are as follows.
+
+A check of the form `e == null` or of the form `e is Null` where `e` has static
+type `T` promotes the type of `e` to `Null` in the `true` continuation, and to
+**NonNull**(`T`) in the
+`false` continuation.
+
+A check of the form `e != null` or of the form `e is T` where `e` has static
+type `T?` promotes the type of `e` to `T` in the `true` continuation, and to
+`Null` in the `false` continuation.
+
+
+The **NonNull** function defines the null-promoted version of a type, and is defined as follows.
+
+- **NonNull**(Null) = Never
+- **NonNull**(_C_<_T_<sub>1</sub>, ... , _T_<sub>_n_</sub>>) = _C_<_T_<sub>1</sub>, ... , _T_<sub>_n_</sub>>  for class *C* other than Null
+- **NonNull**(FutureOr<_T_>) = FutureOr<_T_>   
+- **NonNull**(_T_<sub>0</sub> Function(...)) = _T_<sub>0</sub> Function(...)
+- **NonNull**(_Function) = Function
+- **NonNull**(Never) = Never
+- **NonNull**(dynamic) = dynamic
+- **NonNull**(void) = void   
+- **NonNull**(_X_) = X & **NonNull**(B), where B is the bound of X.
+- **NonNull**(_X_ & T) = X & **NonNull**(T)
+- **NonNull**(_T_?) = **NonNull**(_T_)
+- **NonNull**(_T_\*) = **NonNull**(_T_)
+
+#### Type promotion, Definite Assignment, and Definite Completion
+
+These are extended as per separate proposal.
+
+### Runtime semantics
+
+#### Null assertion operator
+
+An expression of the form `e!` evaluates `e` to a value `v`, throws a runtime
+error if `v` is `null`, and otherwise evaluates to `v`.
+
+#### Null aware operator
+
+An expression of the form `e?.<tail>` where `<tail>` is any sequence of
+selectors evaluates to `null` if `e` evaluates to `null`, and otherwise
+evaluates to the same value as `e.<tail>`.
+
+An expression of the form `e?..<tail>` where `<tail>` is any sequence of
+selectors evaluates to `null` if `e` evaluates to `null`, and otherwise
+evaluates to the same value as `e..<tail>`.
+
+**TODO** Define exactly how a valid `<tail>` is delimited.
+
+#### Lazy fields and variables
+
+A read of a field or variable which is marked as `lazy` which has not yet been
+written to causes the initializer expression of the variable to be evaluated to
+a value, assigned to the variable or field, and returned as the value of the
+read.
+  - If there is no initializer expression, the read causes a runtime error.
+  - Evaluating the initializer expression may validly cause a write to the field
+    or variable, assuming that the field or variable is not final.  In this
+    case, the variable assumes the written value for the duration of the
+    evaluation of the initializer expression, whereupon the final value of the
+    initializer expression overwrites the intermediate written value.
+  - Evaluating the initializer expression may cause an exception to be thrown.
+    If the variable was written to before the exception was thrown, the value of
+    the variable on subsequent reads is the written value.  If the variable was
+    not written before the exception was thrown, then the next read attempts to
+    evaluate the initializer expression again.
+  - If a variable or field is read from during the process of evaluating its own
+    initializer expression, and no write to the variable has occurred, the read
+    is treated as a first read and the initializer expression is evaluated
+    again.
+
+A toplevel variable with an initializer is evaluated as if it was marked `lazy`.
+Note that this is a change from pre-NNBD semantics in that:
+  - Throwing an exception during initializer evaluation no longer sets the
+    variable to `null`
+  - Reading the variable during initializer evaluation is no longer a
+
+## Core library changes
+
+Calling the `.length` setter on a `List` of non-nullable element type with an
+argument greater than the current length of the list is a runtime error.
+
+## Migration features
+
+For migration, we support incremental adoption of non-nullability as described
+in
+the
+[roadmap](https://github.com/dart-lang/language/blob/master/working/0110-incremental-sound-nnbd/roadmap.md).
+
+### Opted in libraries.
+
+Libraries and packages must opt into the feature as described elsewhere.  An
+opted-in library may depend on un-opted-in libraries, and vice versa.
+
+### Errors as warnings
+
+When weak null checking is enabled, all errors specified this proposal (that is,
+all errors that arise only out of the new features of this proposal) shall be
+treated as warnings.
+
+When strong null checking is enabled, errors specified in this proposal shall be
+treated as errors.
+
+### Legacy libraries
+
+Static checking for a library which has not opted into this feature (a *legacy*
+library) is done using the semantics as of the last version of the language
+before this feature ships (or the last version to which it has opted in, if that
+is different).  All opted-in libraries upstream from the legacy library are
+viewed by the legacy library with nullability related features erased from their
+APIs.  In particular:
+  - All types of the form `T?` in the opted-in API are treated as `T`.
+  - All required named parameters are treated as optional named parameters.
+  - The type `Never` is treated as the type `Null`
+
+In a legacy library, none of the new syntax introduced by this proposal is
+available, and it is a static error if it is used.
+
+
+### Importing legacy libraries from opted-in libraries
+
+The type system is extended with a notion of a legacy type operator.  For every
+type `T`, there is an additional type `T*` which is the legacy version of the
+type.  There is no surface syntax for legacy types, and implementations should
+display the legacy type `T*` in the same way that they would display the type
+`T`, except in so far as it is useful to communicate to programmers for the
+purposes of error messages that the type originates in unmigrated code.
+
+When static checking is done in a migrated library, types which are imported
+from unmigrated libraries are seen as legacy types.  However, for the purposes
+of type inference in migrated libraries, types imported from unmigrated
+libraries shall be treated as non-nullable.  As a result, legacy types will
+never appear as type annotations in migrated libraries, nor will they appear in
+reified positions.
+
+### Exports
+
+If an unmigrated library re-exports a migrated library, the re-exported symbols
+retain their migrated status (that is, downstream migrated libraries will see
+their migrated types).
+
+It is an error for a migrated library to re-export symbols from an unmigrated
+library.
+
+### Override checking
+
+In an unmigrated library, override checking is done using legacy types.  This
+means that an unmigrated library can bring together otherwise incompatible
+methods.  When choosing the most specific signature during interface
+computation, all nullability and requiredness annotations are ignored, and the
+`Never` type is treated as `Null`.
+
+In a migrated library, override checking must check that an override is
+consistent with all overridden methods from other migrated libraries in the
+super-interface chain, since a legacy library is permitted to override otherwise
+incompatible signatures for a method.
+
+## Subtyping
+
+We modify the subtyping rules to account for nullability and legacy types as
+specified
+[here](https://github.com/dart-lang/language/blob/master/resources/type-system/subtyping.md).
+
+## Upper and lower bounds
+
+**TODO** This is work in progress

From f7c278f063f81711bc9886aff0bbb2e2a872eef5 Mon Sep 17 00:00:00 2001
From: Leaf Petersen <leafp@google.com>
Date: Fri, 29 Mar 2019 16:51:27 -0700
Subject: [PATCH 02/12] Updates

---
 .../feature-specification.md                  | 80 ++++++++++++-------
 1 file changed, 51 insertions(+), 29 deletions(-)

diff --git a/working/0110-incremental-sound-nnbd/feature-specification.md b/working/0110-incremental-sound-nnbd/feature-specification.md
index 1daade25a2..64a2a6897c 100644
--- a/working/0110-incremental-sound-nnbd/feature-specification.md
+++ b/working/0110-incremental-sound-nnbd/feature-specification.md
@@ -5,7 +5,7 @@ Author: leafp@google.com
 Status: Draft
 
 This is the proposed specification for [sound non-nullable by default types](http://github.com/dart-lang/language/issues/110).
-Discussion of this proposal should take place in [Issue 110](http://github.com/dart-lang/language/issues/100).
+Discussion of this proposal should take place in [Issue 110](http://github.com/dart-lang/language/issues/110).
 
 Discussion issues on specific topics related to this proposal are [here](https://github.com/dart-lang/language/issues?utf8=%E2%9C%93&q=is%3Aissue+label%3Annbd+)
 
@@ -24,17 +24,17 @@ up
 ## Syntax
 
 The grammar of types is extended to allow any type to be suffixed with a `?`
-(e.g. `int ?`) indicating the nullable version of that type.
+(e.g. `int?`) indicating the nullable version of that type.
 
 A new primitive type `Never`.  This type is denoted by the built-in type
 declaration `Never`, with the same syntactic and scoping treatment as with other
-built-in types such as `dynamic`.
+built-in types such as `Null`.
 
 The grammer of expressions is extended to allow any expression to be suffixed
 with a `!`.
 
-The grammer of static and instance fields and static and local variables is
-extended to allow any declaration to include the modifer `lazy`.
+The grammer of instance fields and local variables is extended to allow any
+declaration to include the modifer `lazy`.
 
 The grammar of function types is extended to allow an additional group of named
 parameters prefaced with the word `required` (e.g. `int Function(int, {int?
@@ -83,11 +83,11 @@ the syntactic criterion that `T` is any of:
   - `FutureOr<S>` for some `S` where `S` is nullable
   - `dynamic`
   - `void`
-  - `X extends Null`
 
 We say that a type `T` is **non-nullable** if `T <: Object`.  This is equivalent
 to the syntactic criterion that `T` is any of:
-  - `Object`, `int`, `bool`, `Never`
+  - `Object`, `int`, `bool`, `Never`, `Function`
+  - Any function type
   - Any class type or generic class type
   - `FutureOr<S>` where `S` is non-nullable
   - `X extends S` where `S` is non-nullable
@@ -118,9 +118,9 @@ fields on `Object`.
 It is an error to call an expression whose type is potentially nullable and not
 `dynamic`.
 
-It is an error for a top level variable, static field, or instance field with no
-static initializer to have a potentially nullable type unless the variable or
-field is marked with the `lazy` modifier.
+It is an error for an instance field with no static initializer to have a
+potentially nullable type unless the variable or field is marked with the `lazy`
+modifier.
 
 It is an error if a local variable that is potentially non-nullable and is not
 marked `lazy` is used before it is definitely assigned (see Definite Assignment
@@ -160,7 +160,8 @@ potentially nullable.
 
 It is not an error for the body of a `lazy` field to reference `this`.
 
-It is an error for a formal parameter to be declared `lazy`.
+It is an error for a toplevel variable, a static field, or a formal parameter to
+be declared `lazy`.
 
 It is an error if the type `T` in the **on-catch** clause `on T catch` is
 potentially nullable.
@@ -178,6 +179,8 @@ The default bound of generic type parameters is treated as `Object?`.
 
 ### Type promotion, Definite Assignment, and Definite Completion
 
+**TODO** Fill this out.
+
 ### Null promotion
 
 The machinery of type promotion is extended to promote the type of variables
@@ -194,14 +197,18 @@ A check of the form `e != null` or of the form `e is T` where `e` has static
 type `T?` promotes the type of `e` to `T` in the `true` continuation, and to
 `Null` in the `false` continuation.
 
+The static type of an expression `e!` is **NonNull**(`T`) where `T` is the
+static type of `e`.
 
-The **NonNull** function defines the null-promoted version of a type, and is defined as follows.
+The **NonNull** function defines the null-promoted version of a type, and is
+defined as follows.
 
 - **NonNull**(Null) = Never
 - **NonNull**(_C_<_T_<sub>1</sub>, ... , _T_<sub>_n_</sub>>) = _C_<_T_<sub>1</sub>, ... , _T_<sub>_n_</sub>>  for class *C* other than Null
 - **NonNull**(FutureOr<_T_>) = FutureOr<_T_>   
 - **NonNull**(_T_<sub>0</sub> Function(...)) = _T_<sub>0</sub> Function(...)
-- **NonNull**(_Function) = Function
+- **NonNull**(Function) = Function
+- **NonNull**(Object) = Object
 - **NonNull**(Never) = Never
 - **NonNull**(dynamic) = dynamic
 - **NonNull**(void) = void   
@@ -242,24 +249,25 @@ read.
   - If there is no initializer expression, the read causes a runtime error.
   - Evaluating the initializer expression may validly cause a write to the field
     or variable, assuming that the field or variable is not final.  In this
-    case, the variable assumes the written value for the duration of the
-    evaluation of the initializer expression, whereupon the final value of the
-    initializer expression overwrites the intermediate written value.
+    case, the variable assumes the written value.  The final value of the
+    initializer expression overwrites any intermediate written values.
   - Evaluating the initializer expression may cause an exception to be thrown.
     If the variable was written to before the exception was thrown, the value of
-    the variable on subsequent reads is the written value.  If the variable was
-    not written before the exception was thrown, then the next read attempts to
-    evaluate the initializer expression again.
+    the variable on subsequent reads is the last written value.  If the variable
+    was not written before the exception was thrown, then the next read attempts
+    to evaluate the initializer expression again.
   - If a variable or field is read from during the process of evaluating its own
     initializer expression, and no write to the variable has occurred, the read
     is treated as a first read and the initializer expression is evaluated
     again.
 
-A toplevel variable with an initializer is evaluated as if it was marked `lazy`.
-Note that this is a change from pre-NNBD semantics in that:
+A toplevel or static variable with an initializer is evaluated as if it was
+marked `lazy`.  Note that this is a change from pre-NNBD semantics in that:
   - Throwing an exception during initializer evaluation no longer sets the
     variable to `null`
-  - Reading the variable during initializer evaluation is no longer a
+  - Reading the variable during initializer evaluation is no longer a checked
+    error.
+
 
 ## Core library changes
 
@@ -269,7 +277,7 @@ argument greater than the current length of the list is a runtime error.
 ## Migration features
 
 For migration, we support incremental adoption of non-nullability as described
-in
+at a high level in
 the
 [roadmap](https://github.com/dart-lang/language/blob/master/working/0110-incremental-sound-nnbd/roadmap.md).
 
@@ -280,12 +288,14 @@ opted-in library may depend on un-opted-in libraries, and vice versa.
 
 ### Errors as warnings
 
-When weak null checking is enabled, all errors specified this proposal (that is,
-all errors that arise only out of the new features of this proposal) shall be
-treated as warnings.
+Weak null checking is enabled as soon as a package or library opts into this
+feature. When weak null checking is enabled, all errors specified this proposal
+(that is, all errors that arise only out of the new features of this proposal)
+shall be treated as warnings.
 
-When strong null checking is enabled, errors specified in this proposal shall be
-treated as errors.
+Strong null checking is enabled by running the compilation or execution
+environment with the appropriate flags.  When strong null checking is enabled,
+errors specified in this proposal shall be treated as errors.
 
 ### Legacy libraries
 
@@ -302,7 +312,6 @@ APIs.  In particular:
 In a legacy library, none of the new syntax introduced by this proposal is
 available, and it is a static error if it is used.
 
-
 ### Importing legacy libraries from opted-in libraries
 
 The type system is extended with a notion of a legacy type operator.  For every
@@ -319,6 +328,19 @@ libraries shall be treated as non-nullable.  As a result, legacy types will
 never appear as type annotations in migrated libraries, nor will they appear in
 reified positions.
 
+### Type reification
+
+All types reified in legacy libraries are reified as legacy types.  Runtime
+subtyping checks treat them according to the subtyping rules specified
+separately.
+
+### Runtime checks and weak checking
+
+When weak checking is enabled, runtime type tests (including explicit and
+implicit casts) shall succeed with a warning whenever the runtime type test
+would have succeeded if all `?` types were ignored, `Never` were treated as
+`Null`, and `required` named parameters were treated as optional.
+
 ### Exports
 
 If an unmigrated library re-exports a migrated library, the re-exported symbols

From 79e8f5892cf63d3e674abaceabe8150a5c00a866 Mon Sep 17 00:00:00 2001
From: Leaf Petersen <leafp@google.com>
Date: Wed, 17 Apr 2019 14:31:37 -0700
Subject: [PATCH 03/12] Address some comments

---
 .../feature-specification.md                  | 89 ++++++++++++-------
 1 file changed, 57 insertions(+), 32 deletions(-)

diff --git a/working/0110-incremental-sound-nnbd/feature-specification.md b/working/0110-incremental-sound-nnbd/feature-specification.md
index 64a2a6897c..db6fe5050b 100644
--- a/working/0110-incremental-sound-nnbd/feature-specification.md
+++ b/working/0110-incremental-sound-nnbd/feature-specification.md
@@ -27,22 +27,20 @@ The grammar of types is extended to allow any type to be suffixed with a `?`
 (e.g. `int?`) indicating the nullable version of that type.
 
 A new primitive type `Never`.  This type is denoted by the built-in type
-declaration `Never`, with the same syntactic and scoping treatment as with other
-built-in types such as `Null`.
+declaration `Never` declared in `dart:core`.
 
 The grammer of expressions is extended to allow any expression to be suffixed
 with a `!`.
 
-The grammer of instance fields and local variables is extended to allow any
-declaration to include the modifer `lazy`.
+The modifier `late` is added as a built-in identifier.  The grammer of top level
+variables, static fields, instance fields, and local variables is extended to
+allow any declaration to include the modifer `late`.  **TODO: consider making
+`late` a keyword**
 
-The grammar of function types is extended to allow an additional group of named
-parameters prefaced with the word `required` (e.g. `int Function(int, {int?
-y}, required {int z})`.
-
-The grammar of function/method/closure declarations is extended to allow an
-additional group of named parameters prefaced with the word `required`
-(e.g. `int f(int x, {int?  y}, required {int z})`.
+The modifier `required` is added as a built-in identifier. The grammar of
+function types is extended to allow any named parameter declaration to be
+prefixed by the `required` modifier (e.g. `int Function(int, {int?  y, required
+int z})`. **TODO: consider making `required` a keyword**
 
 
 ### Grammatical ambiguities and clarifications.
@@ -62,8 +60,8 @@ type ::= type' `?`?
 #### Conditional expression ambiguities
 
 Conditional expressions inside of braces are ambiguous between sets and maps.
-That is, `{ a as int ? - 3 : 3 }` can be parsed as a set literal `{ (a as int)
-? - 3 : 3 }` or as a map literal `{ (a as int ?) - 3 : 3 }`.  Parsers will
+That is, `{ a as bool ? - 3 : 3 }` can be parsed as a set literal `{ (a as bool)
+? - 3 : 3 }` or as a map literal `{ (a as bool ?) - 3 : 3 }`.  Parsers will
 prefer the former parse over the latter.
 
 The same is true for `{ a is int ? - 3 : 3 }`.
@@ -118,17 +116,18 @@ fields on `Object`.
 It is an error to call an expression whose type is potentially nullable and not
 `dynamic`.
 
-It is an error for an instance field with no static initializer to have a
-potentially nullable type unless the variable or field is marked with the `lazy`
-modifier.
+It is an error if an instance field with potentially nullable type has no
+initializer expression and is not initialized in a constructor via an
+initializing formal or an initializer list entry, unless the variable or field
+is marked with the `late` modifier.
 
 It is an error if a local variable that is potentially non-nullable and is not
-marked `lazy` is used before it is definitely assigned (see Definite Assignment
+marked `late` is used before it is definitely assigned (see Definite Assignment
 below).
 
-It is an error if a method, function, getter, or closure with a potentially
-non-nullable return type does not definitely complete (see Definite Completion
-below).
+It is an error if a method, function, getter, or function expression with a
+potentially non-nullable return type does not definitely complete (see Definite
+Completion below).
 
 It is an error if an optional parameter (named or otherwise) with no default
 value has a potentially non-nullable type.
@@ -158,10 +157,12 @@ function call.
 It is an error if the static type of `e` in the expression `throw e` is
 potentially nullable.
 
-It is not an error for the body of a `lazy` field to reference `this`.
+It is not an error for the body of a `late` field to reference `this`.
 
-It is an error for a toplevel variable, a static field, or a formal parameter to
-be declared `lazy`.
+It is an error for a formal parameter to be declared `late`.
+
+It is not a compile time error to write to a `final` variable if that variable
+is declared `late` and does not have an initializer.
 
 It is an error if the type `T` in the **on-catch** clause `on T catch` is
 potentially nullable.
@@ -204,11 +205,10 @@ The **NonNull** function defines the null-promoted version of a type, and is
 defined as follows.
 
 - **NonNull**(Null) = Never
-- **NonNull**(_C_<_T_<sub>1</sub>, ... , _T_<sub>_n_</sub>>) = _C_<_T_<sub>1</sub>, ... , _T_<sub>_n_</sub>>  for class *C* other than Null
+- **NonNull**(_C_<_T_<sub>1</sub>, ... , _T_<sub>_n_</sub>>) = _C_<_T_<sub>1</sub>, ... , _T_<sub>_n_</sub>>  for class *C* other than Null (including Object).
 - **NonNull**(FutureOr<_T_>) = FutureOr<_T_>   
 - **NonNull**(_T_<sub>0</sub> Function(...)) = _T_<sub>0</sub> Function(...)
 - **NonNull**(Function) = Function
-- **NonNull**(Object) = Object
 - **NonNull**(Never) = Never
 - **NonNull**(dynamic) = dynamic
 - **NonNull**(void) = void   
@@ -217,7 +217,7 @@ defined as follows.
 - **NonNull**(_T_?) = **NonNull**(_T_)
 - **NonNull**(_T_\*) = **NonNull**(_T_)
 
-#### Type promotion, Definite Assignment, and Definite Completion
+#### Extended Type promotion, Definite Assignment, and Definite Completion
 
 These are extended as per separate proposal.
 
@@ -240,9 +240,9 @@ evaluates to the same value as `e..<tail>`.
 
 **TODO** Define exactly how a valid `<tail>` is delimited.
 
-#### Lazy fields and variables
+#### Late fields and variables
 
-A read of a field or variable which is marked as `lazy` which has not yet been
+A read of a field or variable which is marked as `late` which has not yet been
 written to causes the initializer expression of the variable to be evaluated to
 a value, assigned to the variable or field, and returned as the value of the
 read.
@@ -261,12 +261,37 @@ read.
     is treated as a first read and the initializer expression is evaluated
     again.
 
-A toplevel or static variable with an initializer is evaluated as if it was
-marked `lazy`.  Note that this is a change from pre-NNBD semantics in that:
+A write to a field or variable which is marked `final` and `late` is a runtime
+error unless the field or variable was declared with no initializer expression,
+and there have been no previous writes to the field or variable (including via
+an initializing formal or an initializer list entry).
+
+Overriding a field which is marked both `final` and `late` with a member which
+does not otherwise introduce a setter introduces an implicit setter which
+throws.  For example:
+
+```
+class A {
+  final late int x;
+}
+class B extends A {
+  int get x => 3;
+}
+class C extends A {
+  final late int x = 3;
+}
+void test() {
+   Expect.throws(() => new B().x = 3);
+   Expect.throws(() => new C().x = 3);
+}
+```
+
+A toplevel or static variable with an initializer is evaluated as if it
+was marked `late`.  Note that this is a change from pre-NNBD semantics in that:
   - Throwing an exception during initializer evaluation no longer sets the
     variable to `null`
-  - Reading the variable during initializer evaluation is no longer a checked
-    error.
+  - Reading the variable during initializer evaluation is no longer checked for,
+    and does not cause an error.
 
 
 ## Core library changes

From eec13c1654a122e76963f0ecdb329f91b588a886 Mon Sep 17 00:00:00 2001
From: Leaf Petersen <leafp@google.com>
Date: Wed, 17 Apr 2019 21:20:49 -0700
Subject: [PATCH 04/12] Proposed grammar for late and required

---
 specification/dart.sty         |  2 ++
 specification/dartLangSpec.tex | 26 +++++++++++++++++---------
 2 files changed, 19 insertions(+), 9 deletions(-)

diff --git a/specification/dart.sty b/specification/dart.sty
index 77d8efa2bb..30af2edb6d 100644
--- a/specification/dart.sty
+++ b/specification/dart.sty
@@ -19,6 +19,7 @@
 \def\MIXIN{\builtinId{mixin}}
 \def\OPERATOR{\builtinId{operator}}
 \def\PART{\builtinId{part}}
+\def\REQUIRED{\builtinId{required}}
 \def\SET{\builtinId{set}}
 \def\STATIC{\builtinId{static}}
 \def\TYPEDEF{\builtinId{typedef}}
@@ -45,6 +46,7 @@
 \def\IF{\keyword{if}}
 \def\IN{\keyword{in}}
 \def\IS{\keyword{is}}
+\def\LATE{\keyword{late}}
 \def\NEW{\keyword{new}}
 \def\NULL{\keyword{null}}
 \def\OF{\keyword{of}}
diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 7115b354e5..10de5cc821 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -826,7 +826,8 @@ \section{Variables}
 
 <declaredIdentifier> ::= <metadata> \COVARIANT{}? <finalConstVarOrType> <identifier>
 
-<finalConstVarOrType> ::= \FINAL{} <type>?
+<finalConstVarOrType> ::= \LATE{} \FINAL{}? <type>?
+  \alt \FINAL{} <type>?
   \alt \CONST{} <type>?
   \alt <varOrType>
 
@@ -1405,13 +1406,13 @@ \subsection{Formal Parameters}
 \begin{grammar}
 <formalParameterList> ::= `(' `)'
   \alt `(' <normalFormalParameters> `,'? `)'
-  \alt `(' <normalFormalParameters> `,' <optionalFormalParameters> `)'
-  \alt `(' <optionalFormalParameters> `)'
+  \alt `(' <normalFormalParameters> `,' <optionalOrNamedFormalParameters> `)'
+  \alt `(' <optionalOrNamedFormalParameters> `)'
 
 <normalFormalParameters> ::= \gnewline{}
   <normalFormalParameter> (`,' <normalFormalParameter>)*
 
-<optionalFormalParameters> ::= <optionalPositionalFormalParameters>
+<optionalOrNamedFormalParameters> ::= <optionalPositionalFormalParameters>
   \alt <namedFormalParameters>
 
 <optionalPositionalFormalParameters> ::= \gnewline{}
@@ -1479,8 +1480,8 @@ \subsubsection{Optional Formals}
 \begin{grammar}
 <defaultFormalParameter> ::= <normalFormalParameter> (`=' <expression>)?
 
-<defaultNamedParameter> ::= <normalFormalParameter> (`=' <expression>)?
-  \alt <normalFormalParameter> ( `:' <expression>)?
+<defaultNamedParameter> ::= \REQUIRED{}? <normalFormalParameter> (`=' <expression>)?
+  \alt \REQUIRED{}? <normalFormalParameter> ( `:' <expression>)?
 \end{grammar}
 
 The form \syntax{<normalFormalParameter> `:' <expression>}
@@ -1848,8 +1849,13 @@ \section{Classes}
   \alt \EXTERNAL{}? <operatorSignature>
   \alt (\EXTERNAL{} \STATIC{}?)? <functionSignature>
   \alt \STATIC{} (\FINAL{} | \CONST{}) <type>? <staticFinalDeclarationList>
+  \alt \STATIC{} \LATE{} \FINAL{}? <type>? <initializedIdentifierList>
+  \alt \STATIC{} (\VAR{} | <type>) <initializedIdentifierList>
+  \alt \COVARIANT{} (\VAR{} | \LATE{}) <initializedIdentifierList>
+  \alt \COVARIANT{} \LATE{}? <type> <initializedIdentifierList>
+  \alt \LATE{} \FINAL{}? <type>? <initializedIdentifierList>
   \alt \FINAL{} <type>? <initializedIdentifierList>
-  \alt (\STATIC{} | \COVARIANT{})? (\VAR{} | <type>) <initializedIdentifierList>
+  \alt \(\VAR{} | <type>) <initializedIdentifierList>
 
 <staticFinalDeclarationList> ::= \gnewline{}
   <staticFinalDeclaration> (`,' <staticFinalDeclaration>)*
@@ -3001,7 +3007,7 @@ \subsubsection{Generative Constructors}
   \alt <assertion>
 
 <fieldInitializer> ::= \gnewline{}
-  (\THIS{} `.')? <identifier> `=' <conditionalExpression> <cascadeSection>*
+  (\THIS{} `.')? <identifier> `=' <conditionalExpression> <cascadeSequence>
 \end{grammar}
 
 \LMHash{}%
@@ -5882,7 +5888,7 @@ \section{Expressions}
 
 \begin{grammar}
 <expression> ::= <assignableExpression> <assignmentOperator> <expression>
-  \alt <conditionalExpression> <cascadeSection>*
+  \alt <conditionalExpression> <cascadeSequence>
   \alt <throwExpression>
 
 <expressionWithoutCascade> ::= \gnewline{}
@@ -9479,6 +9485,8 @@ \subsubsection{Cascaded Invocations}
 where $e$ is an expression and \metavar{suffix} is a sequence of operator, method, getter or setter invocations.
 
 \begin{grammar}
+<cascadeSequence> ::= (`?'? <cascadeSection>+)?
+
 <cascadeSection> ::= `..' (<cascadeSelector> <argumentPart>*)
   \gnewline{} (<assignableSelector> <argumentPart>*)*
   \gnewline{} (<assignmentOperator> <expressionWithoutCascade>)?

From 1260b583e244850f64f150e452f1a59067a2937f Mon Sep 17 00:00:00 2001
From: Leaf Petersen <leafp@google.com>
Date: Fri, 19 Apr 2019 13:46:55 -0700
Subject: [PATCH 05/12] More grammar changes

---
 specification/dartLangSpec.tex | 23 ++++++++++++++++-------
 1 file changed, 16 insertions(+), 7 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 10de5cc821..b5f4e3c7c6 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -3007,7 +3007,7 @@ \subsubsection{Generative Constructors}
   \alt <assertion>
 
 <fieldInitializer> ::= \gnewline{}
-  (\THIS{} `.')? <identifier> `=' <conditionalExpression> <cascadeSequence>
+  (\THIS{} `.')? <identifier> `=' <conditionalExpression> <cascadeSequence>?
 \end{grammar}
 
 \LMHash{}%
@@ -5888,7 +5888,7 @@ \section{Expressions}
 
 \begin{grammar}
 <expression> ::= <assignableExpression> <assignmentOperator> <expression>
-  \alt <conditionalExpression> <cascadeSequence>
+  \alt <conditionalExpression> <cascadeSequence>?
   \alt <throwExpression>
 
 <expressionWithoutCascade> ::= \gnewline{}
@@ -9485,12 +9485,14 @@ \subsubsection{Cascaded Invocations}
 where $e$ is an expression and \metavar{suffix} is a sequence of operator, method, getter or setter invocations.
 
 \begin{grammar}
-<cascadeSequence> ::= (`?'? <cascadeSection>+)?
+<cascadeSequence> ::= (`?..' \alt `..`) <cascadeSection> <cascadeSectionContinuation>*
 
-<cascadeSection> ::= `..' (<cascadeSelector> <argumentPart>*)
+<cascadeSection> ::= (<cascadeSelector> <argumentPart>*)
   \gnewline{} (<assignableSelector> <argumentPart>*)*
   \gnewline{} (<assignmentOperator> <expressionWithoutCascade>)?
 
+<cascadeSectionContinuation> ::= `..' <cascadeSection>
+
 <cascadeSelector> ::= `[' <expression> `]'
   \alt <identifier>
 
@@ -11504,6 +11506,8 @@ \subsection{Assignable Expressions}
 
 <assignableSelector> ::= <unconditionalAssignableSelector>
   \alt `?.' <identifier>
+  \alt `!'
+
 \end{grammar}
 
 \LMHash{}%
@@ -14114,8 +14118,10 @@ \subsection{Static Types}
 }
 
 \begin{grammar}
-<type> ::= <functionTypeTails>
-  \alt <typeNotFunction> <functionTypeTails>
+
+<type> ::= <typeNotQuestion> `?'?
+
+<typeNotQuestion> ::= <functionType>
   \alt <typeNotFunction>
 
 <typeNotFunction> ::= <typeNotVoidNotFunction>
@@ -14133,7 +14139,10 @@ \subsection{Static Types}
 <typeNotVoidNotFunctionList> ::= \gnewline{}
   <typeNotVoidNotFunction> (`,' <typeNotVoidNotFunction>)*
 
-<typeNotVoid> ::= <functionType>
+<typeNotVoid> ::= <typeNotVoidNotQuestion> `?'?
+
+<typeNotVoidNotQuestion> ::=
+  <functionType>
   \alt <typeNotVoidNotFunction>
 
 <functionType> ::= <functionTypeTails>

From 03cc142afe5afbeb8c2d3bf6673f9aff25b41227 Mon Sep 17 00:00:00 2001
From: Leaf Petersen <leafp@google.com>
Date: Fri, 19 Apr 2019 14:30:20 -0700
Subject: [PATCH 06/12] Fix function types

---
 specification/dartLangSpec.tex | 25 ++++++++++---------------
 1 file changed, 10 insertions(+), 15 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index b5f4e3c7c6..166f53a0ca 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -1855,7 +1855,7 @@ \section{Classes}
   \alt \COVARIANT{} \LATE{}? <type> <initializedIdentifierList>
   \alt \LATE{} \FINAL{}? <type>? <initializedIdentifierList>
   \alt \FINAL{} <type>? <initializedIdentifierList>
-  \alt \(\VAR{} | <type>) <initializedIdentifierList>
+  \alt (\VAR{} | <type>) <initializedIdentifierList>
 
 <staticFinalDeclarationList> ::= \gnewline{}
   <staticFinalDeclaration> (`,' <staticFinalDeclaration>)*
@@ -14119,16 +14119,17 @@ \subsection{Static Types}
 
 \begin{grammar}
 
-<type> ::= <typeNotQuestion> `?'?
-
-<typeNotQuestion> ::= <functionType>
+<type> ::= <functionType> `?'?
   \alt <typeNotFunction>
 
-<typeNotFunction> ::= <typeNotVoidNotFunction>
-  \alt \VOID{}
+<typeNotVoid> ::= <functionType> `?'?
+  \alt <typeNotVoidNotFunction>
 
-<typeNotVoidNotFunction> ::= <typeName> <typeArguments>?
-  \alt \FUNCTION{}
+<typeNotFunction> ::= \VOID{}
+  \alt <typeNotVoidNotFunction>
+
+<typeNotVoidNotFunction> ::= <typeName> <typeArguments>? `?'?
+  \alt \FUNCTION{} `?'?
 
 <typeName> ::= <typeIdentifier> (`.' <typeIdentifier>)?
 
@@ -14139,16 +14140,10 @@ \subsection{Static Types}
 <typeNotVoidNotFunctionList> ::= \gnewline{}
   <typeNotVoidNotFunction> (`,' <typeNotVoidNotFunction>)*
 
-<typeNotVoid> ::= <typeNotVoidNotQuestion> `?'?
-
-<typeNotVoidNotQuestion> ::=
-  <functionType>
-  \alt <typeNotVoidNotFunction>
-
 <functionType> ::= <functionTypeTails>
   \alt <typeNotFunction> <functionTypeTails>
 
-<functionTypeTails> ::= <functionTypeTail> <functionTypeTails>
+<functionTypeTails> ::= <functionTypeTail> `?'? <functionTypeTails>
   \alt <functionTypeTail>
 
 <functionTypeTail> ::= \FUNCTION{} <typeParameters>? <parameterTypeList>

From 03813d3eb79dd66eb14ef940e5d3d973cd6a9b95 Mon Sep 17 00:00:00 2001
From: Leaf Petersen <leafp@google.com>
Date: Tue, 23 Apr 2019 16:45:14 -0700
Subject: [PATCH 07/12] Add specification for null-shorting

---
 specification/dartLangSpec.tex                |   3 +-
 .../feature-specification.md                  | 145 ++++++++++++++++--
 2 files changed, 137 insertions(+), 11 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 166f53a0ca..d9fcfdb509 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -9485,7 +9485,7 @@ \subsubsection{Cascaded Invocations}
 where $e$ is an expression and \metavar{suffix} is a sequence of operator, method, getter or setter invocations.
 
 \begin{grammar}
-<cascadeSequence> ::= (`?..' \alt `..`) <cascadeSection> <cascadeSectionContinuation>*
+<cascadeSequence> ::= (`?..' \alt `..') <cascadeSection> <cascadeSectionContinuation>*
 
 <cascadeSection> ::= (<cascadeSelector> <argumentPart>*)
   \gnewline{} (<assignableSelector> <argumentPart>*)*
@@ -11506,6 +11506,7 @@ \subsection{Assignable Expressions}
 
 <assignableSelector> ::= <unconditionalAssignableSelector>
   \alt `?.' <identifier>
+  \alt `?.[' <expression> `]'
   \alt `!'
 
 \end{grammar}
diff --git a/working/0110-incremental-sound-nnbd/feature-specification.md b/working/0110-incremental-sound-nnbd/feature-specification.md
index db6fe5050b..8ca99eb57a 100644
--- a/working/0110-incremental-sound-nnbd/feature-specification.md
+++ b/working/0110-incremental-sound-nnbd/feature-specification.md
@@ -4,6 +4,14 @@ Author: leafp@google.com
 
 Status: Draft
 
+## CHANGELOG
+
+2019.04.23:
+  - Added specification of short-circuiting null
+  - Added `e1?.[e2]` operator syntax
+
+## Summary
+
 This is the proposed specification for [sound non-nullable by default types](http://github.com/dart-lang/language/issues/110).
 Discussion of this proposal should take place in [Issue 110](http://github.com/dart-lang/language/issues/110).
 
@@ -23,16 +31,20 @@ up
 
 ## Syntax
 
+The precise changes to the syntax are given in an accompanying set of
+modifications to the grammar in the formal specification.  This section
+summarizes in prose the grammar changes associated with this feature.
+
 The grammar of types is extended to allow any type to be suffixed with a `?`
 (e.g. `int?`) indicating the nullable version of that type.
 
 A new primitive type `Never`.  This type is denoted by the built-in type
 declaration `Never` declared in `dart:core`.
 
-The grammer of expressions is extended to allow any expression to be suffixed
+The grammar of expressions is extended to allow any expression to be suffixed
 with a `!`.
 
-The modifier `late` is added as a built-in identifier.  The grammer of top level
+The modifier `late` is added as a built-in identifier.  The grammar of top level
 variables, static fields, instance fields, and local variables is extended to
 allow any declaration to include the modifer `late`.  **TODO: consider making
 `late` a keyword**
@@ -42,13 +54,17 @@ function types is extended to allow any named parameter declaration to be
 prefixed by the `required` modifier (e.g. `int Function(int, {int?  y, required
 int z})`. **TODO: consider making `required` a keyword**
 
+The grammar of selectors is extended to allow null-aware subscripting using the
+syntax `e1?.[e2]` which evaluates to `null` if `e1` evaluates to `null` and
+otherwise evaluates as `e1[e2]`.
+
 
 ### Grammatical ambiguities and clarifications.
 
 #### Nested nullable types
 
 The grammar for types does not allow multiple successive `?` operators on a
-type.  That is, the grammar for types is
+type.  That is, the grammar for types is nominally equivalent to:
 
 ```
 type' ::= functionType
@@ -167,6 +183,7 @@ is declared `late` and does not have an initializer.
 It is an error if the type `T` in the **on-catch** clause `on T catch` is
 potentially nullable.
 
+
 ### Assignability
 
 The definition of assignability is changed as follows.  
@@ -230,15 +247,123 @@ error if `v` is `null`, and otherwise evaluates to `v`.
 
 #### Null aware operator
 
-An expression of the form `e?.<tail>` where `<tail>` is any sequence of
-selectors evaluates to `null` if `e` evaluates to `null`, and otherwise
-evaluates to the same value as `e.<tail>`.
+The semantics of the null aware operator `?.` are defined via a source to source
+translation of expressions into Dart code extended with a let binding construct.
+The translation is defined using meta-level functions over syntax.  We use the
+notation `fn[x : Exp] : Exp => E` to define a meta-level function of type `Exp
+-> Exp` (that is, a function from expressions to expressions), and similarly
+`fn[k : Exp -> Exp] : Exp => E` to define a meta-level function of type `Exp ->
+Exp -> Exp`.  Where obvious from context, we elide the parameter and return
+types on the meta-level functions.  The meta-variables `F` and `G` are used to
+range over meta-level functions. Application of a meta-level function is written
+as `F[p]` where `p` is the argument.
+
+The null-shorting translation of an expression `e` is meta-level function `F` of
+type `Exp -> Exp -> Exp` which takes as an argument the continuation of `e` and
+produces an expression semantically equivalent to `e` with all occurrences of
+`?.` eliminated in favor of explicit sequencing using a `let` construct.
+
+Let `ID` be the identity function `fn[x : Exp] : Exp => x`.
+
+The expression translation of an expression `e` is the result of applying the
+null-shorting translation of `e` to `ID`.  That is, if `e` translates to `F`,
+then `F[ID]` is the expression translation of `e`.
+
+We use `EXP(e)` as a shorthand for the expression translation of `e`.  That is,
+if the null-shorting translation of `e` is `F`, then `EXP(e)` is `F[ID]`.
+
+We extend the expression translation to argument lists in the obvious way, using
+`ARGS(args)` to denote the result of applying the expression translation
+pointwise to the arguments in the argument list `args`.
 
-An expression of the form `e?..<tail>` where `<tail>` is any sequence of
-selectors evaluates to `null` if `e` evaluates to `null`, and otherwise
-evaluates to the same value as `e..<tail>`.
+We use three combinators to express the translation.
+
+The null-aware shorting combinator `SHORT` is defined as:
+```
+  SHORT = fn[r : Exp, c : Exp -> Exp] =>
+              fn[k : Exp -> Exp] : Exp =>
+                let x = r in x == null ? null : k[c[x]]
+```
+
+where `x` is a fresh object level variable.  The `SHORT` combinator is used to
+give semantics to uses of the `?.` operator.  It is parameterized over the
+receiver of the conditional property access (`r`) and a meta-level function
+(`c`) which given an object-level variable (`x`) bound to the result of
+evaluating the receiver, produces the final expression.  The result is
+parameterized over the continuation of the expression being translated.  The
+continuation is only called in the case that the result of evaluating the
+receiver is non-null.
+
+The shorting propagation combinator `PASSTHRU` is defined as:
+```
+  PASSTHRU = fn[F : Exp -> Exp -> Exp, c : Exp -> Exp] =>
+               fn[k : Exp -> Exp] : Exp => F[fn[x] => k[c[x]]]
+```
+
+The `PASSTHRU` combinator is used to give semantics to expression forms which
+propagate null-shorting behavior.  It is parameterized over the translation `F`
+of the potentially null-shorting expression, and over a meta-level function `c`
+which given an expression which denotes the value of the translated
+null-shorting expression produces the final expression being translated.  The
+result is parameterized over the continuation of the expression being
+translated, which is called unconditionally.
+
+The null-shorting termination combinator TERM is defined as:
+```
+  TERM = fn[r : Exp] => fn[k : Exp -> Exp] : Exp => k[r]
+```
 
-**TODO** Define exactly how a valid `<tail>` is delimited.
+The `TERM` combinator is used to give semantics to expressions which neither
+short-circuit nor propagate null-shorting behavior.  It is parameterized over
+the translated expression, and simply passes on the expression to its
+continuation.
+
+- A property access `e?.f` translates to:
+  - `SHORT[EXP(e), fn[x] => x.f]`
+- If `e` translates to `F` then `e.f` translates to:
+  - `PASSTHRU[F, fn[x] => x.f]`
+- A null aware method call `e?.m(args)` translates to:
+  - `SHORT[EXP(e), fn[x] => x.m(ARGS(args))]`
+- If `e` translates to `F` then `e.m(args)` translates to:
+  - `PASSTHRU[F, fn[x] => x.m(ARGS(args))]`
+- If `e` translates to `F` then `e(args)` translates to:
+  - `PASSTHRU[F, fn[x] => x(ARGS(args))]`
+- If `e1` translates to `F` then `e1?.[e2]` translates to:
+  - `SHORT[EXP(e1), fn[x] => x[EXP(e2)]]`
+- If `e1` translates to `F` then `e1[e2]` translates to:
+  - `PASSTHRU[F, fn[x] => x[EXP(e2)]]`
+- The assignment `e1?.f = e2` translates to:
+  - `SHORT[EXP(e1), fn[x] => x.f = EXP(e2)]`
+- The other assignment operators are handled equivalently.
+- If `e1` translates to `F` then `e1.f = e2` translates to:
+  - `PASSTHRU[F, fn[x] => x.f = EXP(e2)]`
+- The other assignment operators are handled equivalently.
+- If `e1` translates to `F` then `e1?.[e2] = e3` translates to:
+  - `SHORT[EXP(e1), fn[x] => x[EXP(e2)] = EXP(e3)]`
+- The other assignment operators are handled equivalently.
+- If `e1` translates to `F` then `e1[e2] = e3` translates to:
+  - `PASSTHRU[F, fn[x] => x[EXP(e2)] = EXP(e3)]`
+- The other assignment operators are handled equivalently.
+- A cascade expression `e..s` translates as follows, where `F` is the
+    translation of `e` and  `x` and `y` are fresh object level variables:
+    ```
+        fn[k : Exp -> Exp] : Exp =>
+           F[fn[r : Exp] : Exp => let x = r in
+                                  let y = EXP(x.s)
+                                  in k[x]
+           ]
+    ```
+- A null-shorting cascade expression `e?..s` translates as follows, where `x`
+    and `y` are fresh object level variables.
+    ```
+       fn[k : Exp -> Exp] : Exp =>
+           let x = EXP(e) in x == null ? null : let y = EXP(x.s) in k(x)
+    ```
+- All other expressions are translated compositionally using the `TERM`
+  combinator.  Examples:
+  - An identifier `x` translates to `TERM[x]`
+  - A list literal `[e1, ..., en]` translates to `TERM[ [EXP(e1), ..., EXP(en)] ]`
+  - A parenthesized expression `(e)` translates to `TERM[(EXP(e))]`
 
 #### Late fields and variables
 

From 2466591b46859be3984ab051c55e515abf8abc01 Mon Sep 17 00:00:00 2001
From: Leaf Petersen <leafp@google.com>
Date: Tue, 28 May 2019 18:31:15 -0700
Subject: [PATCH 08/12] Fixes for late

---
 specification/dartLangSpec.tex | 21 +++++++++------------
 1 file changed, 9 insertions(+), 12 deletions(-)

diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index a26c76d4b3..f71a7ef88f 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -832,10 +832,9 @@ \section{Variables}
 
 <declaredIdentifier> ::= <metadata> \COVARIANT{}? <finalConstVarOrType> <identifier>
 
-<finalConstVarOrType> ::= \LATE{} \FINAL{}? <type>?
-  \alt \FINAL{} <type>?
+<finalConstVarOrType> ::= \alt \LATE{}? \FINAL{} <type>?
   \alt \CONST{} <type>?
-  \alt <varOrType>
+  \alt \LATE{}? <varOrType>
 
 <varOrType> ::= \VAR{}
   \alt <type>
@@ -1854,14 +1853,12 @@ \section{Classes}
   \alt (\EXTERNAL{} \STATIC{}?)? <setterSignature>
   \alt \EXTERNAL{}? <operatorSignature>
   \alt (\EXTERNAL{} \STATIC{}?)? <functionSignature>
-  \alt \STATIC{} (\FINAL{} | \CONST{}) <type>? <staticFinalDeclarationList>
-  \alt \STATIC{} \LATE{} \FINAL{}? <type>? <initializedIdentifierList>
-  \alt \STATIC{} (\VAR{} | <type>) <initializedIdentifierList>
-  \alt \COVARIANT{} (\VAR{} | \LATE{}) <initializedIdentifierList>
-  \alt \COVARIANT{} \LATE{}? <type> <initializedIdentifierList>
-  \alt \LATE{} \FINAL{}? <type>? <initializedIdentifierList>
-  \alt \FINAL{} <type>? <initializedIdentifierList>
-  \alt (\VAR{} | <type>) <initializedIdentifierList>
+  \alt \STATIC{} \LATE{}? \FINAL{} <type>? <staticFinalDeclarationList>
+  \alt \STATIC{} \LATE{}? (\VAR{} | <type>) <initializedIdentifierList>
+  \alt \STATIC{} \CONST{) <type>? <staticFinalDeclarationList>
+  \alt \COVARIANT{} \LATE{}? (\VAR{} | <type>) <initializedIdentifierList>
+  \alt \LATE{}? \FINAL{} <type>? <initializedIdentifierList>
+  \alt \LATE{}? (\VAR{} | <type>) <initializedIdentifierList>
 
 <staticFinalDeclarationList> ::= \gnewline{}
   <staticFinalDeclaration> (`,' <staticFinalDeclaration>)*
@@ -11512,7 +11509,7 @@ \subsection{Assignable Expressions}
 
 <assignableSelector> ::= <unconditionalAssignableSelector>
   \alt `?.' <identifier>
-  \alt `?.[' <expression> `]'
+  \alt `?[' <expression> `]'
   \alt `!'
 
 \end{grammar}

From b5d301e7b1ea5fb3f29090b737ecce8de91c9dc6 Mon Sep 17 00:00:00 2001
From: Leaf Petersen <leafp@google.com>
Date: Fri, 31 May 2019 17:19:57 -0700
Subject: [PATCH 09/12] Address more comments

---
 .../nnbd/feature-specification.md             |  4 +++-
 specification/dartLangSpec.tex                | 24 +++++++++----------
 2 files changed, 15 insertions(+), 13 deletions(-)

diff --git a/accepted/future-releases/nnbd/feature-specification.md b/accepted/future-releases/nnbd/feature-specification.md
index 8ca99eb57a..0f28693af0 100644
--- a/accepted/future-releases/nnbd/feature-specification.md
+++ b/accepted/future-releases/nnbd/feature-specification.md
@@ -183,6 +183,8 @@ is declared `late` and does not have an initializer.
 It is an error if the type `T` in the **on-catch** clause `on T catch` is
 potentially nullable.
 
+It is a warning to use a null aware operator (`?.`, `?..`, `??`, `??=`, or
+`...?`) on a non-nullable receiver.
 
 ### Assignability
 
@@ -240,7 +242,7 @@ These are extended as per separate proposal.
 
 ### Runtime semantics
 
-#### Null assertion operator
+#### Null check operator
 
 An expression of the form `e!` evaluates `e` to a value `v`, throws a runtime
 error if `v` is `null`, and otherwise evaluates to `v`.
diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index f71a7ef88f..00b434ced5 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -1450,7 +1450,7 @@ \subsubsection{Required Formals}
   \alt <simpleFormalParameter>
 
 <functionFormalParameter> ::= \gnewline{}
-  <metadata> \COVARIANT{}? <type>? <identifier> <formalParameterPart>
+  <metadata> \COVARIANT{}? <type>? <identifier> <formalParameterPart> `?'?
 
 <simpleFormalParameter> ::= <declaredIdentifier>
   \alt <metadata> \COVARIANT{}? <identifier>
@@ -9488,17 +9488,17 @@ \subsubsection{Cascaded Invocations}
 where $e$ is an expression and \metavar{suffix} is a sequence of operator, method, getter or setter invocations.
 
 \begin{grammar}
-<cascadeSequence> ::= (`?..' \alt `..') <cascadeSection> <cascadeSectionContinuation>*
+<cascadeSequence> ::= (`?..' \alt `..') <cascadeSection> (`..' <cascadeSection>)*
 
-<cascadeSection> ::= (<cascadeSelector> <argumentPart>*)
-  \gnewline{} (<assignableSelector> <argumentPart>*)*
-  \gnewline{} (<assignmentOperator> <expressionWithoutCascade>)?
-
-<cascadeSectionContinuation> ::= `..' <cascadeSection>
+<cascadeSection> ::= <cascadeSelector> 
+\gnewline{} (cascadeAssignment \alt
+             <selector>* (<assignableSelector> <cascadeAssignment>)?)
 
 <cascadeSelector> ::= `[' <expression> `]'
   \alt <identifier>
 
+<cascadeAssignment> ::= <assignmentOperator> <expressionWithoutCascade>
+
 <argumentPart> ::=
   <typeArguments>? <arguments>
 \end{grammar}
@@ -11295,7 +11295,8 @@ \subsection{Postfix Expressions}
 <constructorInvocation> ::= \gnewline{}
   <typeName> <typeArguments> `.' <identifier> <arguments>
 
-<selector> ::= <assignableSelector>
+<selector> ::= `!'
+  \alt <assignableSelector>
   \alt <argumentPart>
 
 <incrementOperator> ::= `++'
@@ -11501,16 +11502,15 @@ \subsection{Assignable Expressions}
   \alt \SUPER{} <unconditionalAssignableSelector>
   \alt <constructorInvocation> <assignableSelectorPart>+
   <identifier>
-
-<assignableSelectorPart> ::= <argumentPart>* <assignableSelector>
+ 
+<assignableSelectorPart> ::= (<argumentPart> \alt `!')* <assignableSelector>
 
 <unconditionalAssignableSelector> ::= `[' <expression> `]'
   \alt `.' <identifier>
 
 <assignableSelector> ::= <unconditionalAssignableSelector>
   \alt `?.' <identifier>
-  \alt `?[' <expression> `]'
-  \alt `!'
+  \alt `?.[' <expression> `]'
 
 \end{grammar}
 

From 47016c5682e49a7c22d27993f6becac6a8453cfb Mon Sep 17 00:00:00 2001
From: Leaf Petersen <leafp@google.com>
Date: Fri, 31 May 2019 18:11:36 -0700
Subject: [PATCH 10/12] Address additional comments

---
 .../nnbd/feature-specification.md             | 30 ++++++++++++-------
 1 file changed, 20 insertions(+), 10 deletions(-)

diff --git a/accepted/future-releases/nnbd/feature-specification.md b/accepted/future-releases/nnbd/feature-specification.md
index 0f28693af0..2403379dc6 100644
--- a/accepted/future-releases/nnbd/feature-specification.md
+++ b/accepted/future-releases/nnbd/feature-specification.md
@@ -46,13 +46,12 @@ with a `!`.
 
 The modifier `late` is added as a built-in identifier.  The grammar of top level
 variables, static fields, instance fields, and local variables is extended to
-allow any declaration to include the modifer `late`.  **TODO: consider making
-`late` a keyword**
+allow any declaration to include the modifer `late`.
 
 The modifier `required` is added as a built-in identifier. The grammar of
 function types is extended to allow any named parameter declaration to be
 prefixed by the `required` modifier (e.g. `int Function(int, {int?  y, required
-int z})`. **TODO: consider making `required` a keyword**
+int z})`. 
 
 The grammar of selectors is extended to allow null-aware subscripting using the
 syntax `e1?.[e2]` which evaluates to `null` if `e1` evaluates to `null` and
@@ -87,6 +86,11 @@ The same is true for `{ int ? - 3 : 3 }` if we allow this.
 
 ## Static semantics
 
+### Legacy types
+
+The internal representation of types is extended with a type `T*` for every type
+`T` to represent legacy pre-NNBD types.  This is discussed further in the legacy
+library section below.
 
 ### Static errors
 
@@ -94,6 +98,7 @@ We say that a type `T` is **nullable** if `Null <: T`.  This is equivalent to
 the syntactic criterion that `T` is any of:
   - `Null`
   - `S?` for some `S`
+  - `S*` for some `S` where `S` is nullable
   - `FutureOr<S>` for some `S` where `S` is nullable
   - `dynamic`
   - `void`
@@ -114,12 +119,13 @@ non-nullable.
 We say that a type `T` is **potentially nullable** if `T` is not non-nullable.
 Note that this is different from saying that `T` is nullable.  For example, a
 type variable `X extends Object?` is a type which is potentially nullable but
-not nullable.
+not nullable.  Note that `T*` is always potentially nullable by this definition.
 
 We say that a type `T` is **potentially non-nullable** if `T` is not nullable.
 Note that this is different from saying that `T` is non-nullable.  For example,
 a type variable `X extends Object?` is a type which is potentially non-nullable
-but not non-nullable.
+but not non-nullable. Note that `T*` is potentially non-nullable by this
+definition if `T` is potentially non-nullable.
 
 It is an error to call a method, setter, getter or operator on an expression
 whose type is potentially nullable and not `dynamic`, except for the methods,
@@ -186,6 +192,9 @@ potentially nullable.
 It is a warning to use a null aware operator (`?.`, `?..`, `??`, `??=`, or
 `...?`) on a non-nullable receiver.
 
+It is an error if the object being iterated over by a `for-in` loop has a static
+type which is not `dynamic`, and is not a subtype of `Iterable<dynamic>`.
+
 ### Assignability
 
 The definition of assignability is changed as follows.  
@@ -474,11 +483,12 @@ display the legacy type `T*` in the same way that they would display the type
 purposes of error messages that the type originates in unmigrated code.
 
 When static checking is done in a migrated library, types which are imported
-from unmigrated libraries are seen as legacy types.  However, for the purposes
-of type inference in migrated libraries, types imported from unmigrated
-libraries shall be treated as non-nullable.  As a result, legacy types will
-never appear as type annotations in migrated libraries, nor will they appear in
-reified positions.
+from unmigrated libraries are seen as legacy types.  However, type inference in
+the migrated library "erases" legacy types.  That is, if a missing type
+parameter, local variable type, or closure type is inferred to be a type `T`,
+all occurrences of `S*` in `T` shall be replaced with `S`.  As a result, legacy
+types will never appear as type annotations in migrated libraries, nor will they
+appear in reified positions.
 
 ### Type reification
 

From e721716748fe95927e7bce5bbb81aebd722b5ea9 Mon Sep 17 00:00:00 2001
From: Leaf Petersen <leafp@google.com>
Date: Mon, 3 Jun 2019 13:08:10 -0700
Subject: [PATCH 11/12] Tweaks

---
 .../future-releases/nnbd/feature-specification.md     | 11 ++++-------
 specification/dartLangSpec.tex                        |  2 +-
 2 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/accepted/future-releases/nnbd/feature-specification.md b/accepted/future-releases/nnbd/feature-specification.md
index 2403379dc6..1d3def313b 100644
--- a/accepted/future-releases/nnbd/feature-specification.md
+++ b/accepted/future-releases/nnbd/feature-specification.md
@@ -176,8 +176,8 @@ It is an error to call a method, setter, or getter on a receiver of static type
 It is an error to apply an expression of `Never` in the function position in a
 function call.
 
-It is an error if the static type of `e` in the expression `throw e` is
-potentially nullable.
+It is an error if the static type of `e` in the expression `throw e` is not
+assignable to `Object`.
 
 It is not an error for the body of a `late` field to reference `this`.
 
@@ -186,15 +186,12 @@ It is an error for a formal parameter to be declared `late`.
 It is not a compile time error to write to a `final` variable if that variable
 is declared `late` and does not have an initializer.
 
-It is an error if the type `T` in the **on-catch** clause `on T catch` is
-potentially nullable.
+It is an error if the object being iterated over by a `for-in` loop has a static
+type which is not `dynamic`, and is not a subtype of `Iterable<dynamic>`.
 
 It is a warning to use a null aware operator (`?.`, `?..`, `??`, `??=`, or
 `...?`) on a non-nullable receiver.
 
-It is an error if the object being iterated over by a `for-in` loop has a static
-type which is not `dynamic`, and is not a subtype of `Iterable<dynamic>`.
-
 ### Assignability
 
 The definition of assignability is changed as follows.  
diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex
index 00b434ced5..c82fa43afe 100644
--- a/specification/dartLangSpec.tex
+++ b/specification/dartLangSpec.tex
@@ -11501,7 +11501,7 @@ \subsection{Assignable Expressions}
 <assignableExpression> ::= <primary> <assignableSelectorPart>+
   \alt \SUPER{} <unconditionalAssignableSelector>
   \alt <constructorInvocation> <assignableSelectorPart>+
-  <identifier>
+  \alt <identifier>
  
 <assignableSelectorPart> ::= (<argumentPart> \alt `!')* <assignableSelector>
 

From c2b4c0fbee5cf4229dcc45a2f4776d3348460ecb Mon Sep 17 00:00:00 2001
From: Leaf Petersen <leafp@google.com>
Date: Tue, 4 Jun 2019 15:21:27 -0700
Subject: [PATCH 12/12] Fix wording

---
 accepted/future-releases/nnbd/feature-specification.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/accepted/future-releases/nnbd/feature-specification.md b/accepted/future-releases/nnbd/feature-specification.md
index 1d3def313b..ea9a7cb7fe 100644
--- a/accepted/future-releases/nnbd/feature-specification.md
+++ b/accepted/future-releases/nnbd/feature-specification.md
@@ -173,8 +173,8 @@ It is an error for a class to extend, implement, or mixin the type `Never`.
 It is an error to call a method, setter, or getter on a receiver of static type
 `Never` (including via a null aware operator).
 
-It is an error to apply an expression of `Never` in the function position in a
-function call.
+It is an error to apply an expression of type `Never` in the function position
+of a function call.
 
 It is an error if the static type of `e` in the expression `throw e` is not
 assignable to `Object`.