From 23b085f187e72ab6d73767134463b632c802ec88 Mon Sep 17 00:00:00 2001 From: Leaf Petersen Date: Tue, 2 Jun 2020 21:39:27 -0700 Subject: [PATCH 1/2] Batched small updates --- .../nnbd/feature-specification.md | 39 +++++++++++++- resources/type-system/flow-analysis.md | 51 ++++++++----------- resources/type-system/inference.md | 21 ++++++-- 3 files changed, 73 insertions(+), 38 deletions(-) diff --git a/accepted/future-releases/nnbd/feature-specification.md b/accepted/future-releases/nnbd/feature-specification.md index 54089d3a01..76dd35441f 100644 --- a/accepted/future-releases/nnbd/feature-specification.md +++ b/accepted/future-releases/nnbd/feature-specification.md @@ -6,6 +6,11 @@ Status: Draft ## CHANGELOG +2020..06.02 + - Fix the diff to the spec for potentially constant instance checks + - Specify that extensions do not apply to values of type `Never` + - Specify the treatment of typedefs from legacy libraries + 2020.05.20 - Turn new references to `CastError` into being dynamic type errors. @@ -702,9 +707,13 @@ class G { For the purposes of extension method resolution, there is no special treatment of nullable types with respect to what members are considered accessible. That -is, the only members of a nullable tyhpe that are considered accessible +is, the only members of a nullable type that are considered accessible (and hence which take precedence over extensions) are the members on `Object`. +For the purposes of extension method resolution, the type `Never` is considered +to implement all members, and hence no extension may apply to an expression of +type `Never`. + ### Assignability The definition of assignability is changed as follows. @@ -756,7 +765,8 @@ We change the following specification text: to ``` -\item An expression of the form \code{$e$\,\,as\,\,$T$} is potentially constant +\item An expression of the form \code{$e$\,\,as\,\,$T$} or + \code{$e$\,\,is\,\,$T$} is potentially constant if $e$ is a potentially constant expression and $T$ is a potentially constant type expression, and it is further constant if $e$ is constant. @@ -1215,6 +1225,31 @@ all occurrences of `S*` in `T` shall be replaced with `S`. As a result, legacy types will never appear as type annotations in opted-in libraries, nor will they appear in reified positions. +### Typedefs defined in legacy libraries used in opted-in libraries + +A typedef which is define in a legacy library and used in an opted-in library is +treated defining a function type all of the components of which are treated as +legacy, but which is treated as non-nullable at the top level. Hence given the +following program, it is an error to assign a nullable value to a variable of +type `F` in an opted-in library, but any function which is compatible with a +legacy function of type `int* Function(int*)` may be assigned to such a +variable. + +```dart +// Opted-out library "opted_out.dart". +typedef F = int Function(int); + +// Opted-in library "main.dart" +import "opted_out.dart"; + +int? f1(int x) => x; + +void test() { + F f = null; // Static error + f = f1; // No error +} +``` + ### Exports If a legacy library re-exports an opted-in library, the re-exported symbols diff --git a/resources/type-system/flow-analysis.md b/resources/type-system/flow-analysis.md index 4f999f4ff2..05c804a85e 100644 --- a/resources/type-system/flow-analysis.md +++ b/resources/type-system/flow-analysis.md @@ -9,7 +9,10 @@ https://docs.google.com/document/d/11Xs0b4bzH6DwDlcJMUcbx4BpvEKGz8MVuJWEfo_mirE/ ## CHANGELOG -2019.01.16 +2020.06.02 + - Specify the interaction between downwards inference and promotion/demotion. + +2020.01.16 - Modify `restrictV` to make a variable definitely assigned in a try block or a finally block definitely assigned after the block. - Clarify that initialization promotion does not apply to formal parameters. @@ -432,36 +435,22 @@ Definitions: - Else if `T` is `FutureOr` and `R <: S` then `factor(Future, S)` - Else `T` -Questions: - - The interaction between assignment based **promotion** and downwards inference is - probably managable. I think doing downwards inference using the current - type, and then promoting the variable afterwards is fine for all reasonable - cases. - - The interaction between assignment based **demotion** and downwards inference is - a bit trickier. In so far as it is manageable, I think it would need to be - done as follows, given `x = E` where `x` has current type `S`. - - Infer `E` in context `S` - - if the inferred type of `E` is `T` and `S <: T` and the demotion policy - applies, then instead of treating this as `x = (E as S)` (or an error), - then instead treat `x` as promoted to `S` in the scope of the assigment. - - - if a variable is tested before it is initialized, we must choose whether to - honor the type test or the assignment. Above I've chosen to prefer type - test based promotion. Examples: - ``` - test1() { - var x; - if (x is num) { - x = 3; // not an initializing promotion, since it's already promoted - } - } - test2() { - var x; - if (x is String) { - x = 3; // not an initializing promotion, nor an assignment promotion - } - } - ``` +#### Interactions between downwards inference and promotion + +Given an assignment (or composite assignment) `x = E` where `x` has current type +`S` (possibly the result of promotion), inference and promotion interact as +follows. + - Inference for `E` is done as usual, using `S` as the downwards typing + context. All reference to `x` within `E` are treated as having type `S` as + usual. + - Let `T` be the resulting inferred type of `E`. + - If `T` is assignable to `S` then no further work is required. + - Otherwise, the assignment is treated as an assignment of an expression of + type `T` to a variable of type `S`, that is: + - If the demotion policy applies, treat the assignment as a demoting + assignment which demotes `x` to `T`. + - Otherwise, it is an error, unless `T` is dynamic, in which case it is an + implicit downcast. ## Flow analysis diff --git a/resources/type-system/inference.md b/resources/type-system/inference.md index 88e7166d29..574503688f 100644 --- a/resources/type-system/inference.md +++ b/resources/type-system/inference.md @@ -6,6 +6,10 @@ Status: Draft ## CHANGELOG +2020.06.02 + - Account for the special treatment of bottom types during function literal + inference. + 2020.05.27 - Update function literal return type inference to use **futureValueTypeSchema**. @@ -212,15 +216,22 @@ unlike normal fields, the initializer for a `late` field may reference `this`. Function literals which are inferred in an empty typing context (see below) are inferred using the declared type for all of their parameters. If a parameter -has no declared type, it is treated as if it was declared with type `dynamic`. +has no declared type, it is treated as if it was declared with type `dynamic. Inference for each returned expression in the body of the function literal is done in an empty typing context (see below). Function literals which are inferred in an non-empty typing context where the -context type is a function type are inferred as follows. Each parameter is -assumed to have its declared type if present, or the type taken from the -corresponding parameter (if any) from the typing context if not present. The -return type of the context function type is used at several points during +context type is a function type are inferred as described below. + +Each parameter is assumed to have its declared type if present. If no type is +declared for a parameter and there is a corresponding parameter in the context +type schema with type schema `K`, the parameter is given an inferred type `T` +where `T` is derived from `K` as follows. If the greatest closure of `K` is `S` +and `S` is a subtype of `Null`, then `T` is `Object?`. Otherwise, `T` is `S`. +If there is no corresponding parameter in the context type schema, the variable +is treated as having type `dynamic`. + +The return type of the context function type is used at several points during inference. We refer to this type as the **imposed return type schema**. Inference for each returned or yielded expression in the body of the function literal is done using a context type derived from the imposed return From f8104ca1cadbf21cb82ba0a2b015236f69502cfb Mon Sep 17 00:00:00 2001 From: Leaf Petersen Date: Wed, 3 Jun 2020 16:23:40 -0700 Subject: [PATCH 2/2] Address comments --- .../future-releases/nnbd/feature-specification.md | 12 ++++++------ resources/type-system/flow-analysis.md | 9 ++------- resources/type-system/inference.md | 2 +- 3 files changed, 9 insertions(+), 14 deletions(-) diff --git a/accepted/future-releases/nnbd/feature-specification.md b/accepted/future-releases/nnbd/feature-specification.md index 76dd35441f..e539dc4572 100644 --- a/accepted/future-releases/nnbd/feature-specification.md +++ b/accepted/future-releases/nnbd/feature-specification.md @@ -1228,12 +1228,12 @@ appear in reified positions. ### Typedefs defined in legacy libraries used in opted-in libraries A typedef which is define in a legacy library and used in an opted-in library is -treated defining a function type all of the components of which are treated as -legacy, but which is treated as non-nullable at the top level. Hence given the -following program, it is an error to assign a nullable value to a variable of -type `F` in an opted-in library, but any function which is compatible with a -legacy function of type `int* Function(int*)` may be assigned to such a -variable. +treated as defining a function type, all of the components of which are +legacy. The function type itself is treated as non-nullable (and not legacy) at +the top level. Hence given the following program, it is an error to assign a +nullable value to a variable of type `F` in an opted-in library, but any +function which is compatible with a legacy function of type `int* +Function(int*)` may be assigned to such a variable. ```dart // Opted-out library "opted_out.dart". diff --git a/resources/type-system/flow-analysis.md b/resources/type-system/flow-analysis.md index 05c804a85e..78f2404438 100644 --- a/resources/type-system/flow-analysis.md +++ b/resources/type-system/flow-analysis.md @@ -444,13 +444,8 @@ follows. context. All reference to `x` within `E` are treated as having type `S` as usual. - Let `T` be the resulting inferred type of `E`. - - If `T` is assignable to `S` then no further work is required. - - Otherwise, the assignment is treated as an assignment of an expression of - type `T` to a variable of type `S`, that is: - - If the demotion policy applies, treat the assignment as a demoting - assignment which demotes `x` to `T`. - - Otherwise, it is an error, unless `T` is dynamic, in which case it is an - implicit downcast. + - The assignment is treated as an assignment of an expression of type `T` to a + variable of type `S`, with the usual promotion, demotion and errors applied. ## Flow analysis diff --git a/resources/type-system/inference.md b/resources/type-system/inference.md index 574503688f..89a4f7b2ef 100644 --- a/resources/type-system/inference.md +++ b/resources/type-system/inference.md @@ -216,7 +216,7 @@ unlike normal fields, the initializer for a `late` field may reference `this`. Function literals which are inferred in an empty typing context (see below) are inferred using the declared type for all of their parameters. If a parameter -has no declared type, it is treated as if it was declared with type `dynamic. +has no declared type, it is treated as if it was declared with type `dynamic`. Inference for each returned expression in the body of the function literal is done in an empty typing context (see below).