From 590708d2ec269844ef014543799f1e207023a3ed Mon Sep 17 00:00:00 2001 From: Paul Berry Date: Thu, 25 Jul 2024 23:19:17 +0000 Subject: [PATCH] Address review comments --- resources/type-system/inference.md | 169 ++++++++++++++++++++--------- 1 file changed, 118 insertions(+), 51 deletions(-) diff --git a/resources/type-system/inference.md b/resources/type-system/inference.md index a628916f6..57bf0d923 100644 --- a/resources/type-system/inference.md +++ b/resources/type-system/inference.md @@ -1134,25 +1134,58 @@ succintly, the syntax of Dart is extended to allow the following forms: any loss of functionality, provided they are not trying to construct a proof of soundness._ -In addition, the following forms are added to allow constructor invocations, -dynamic method invocations, function object invocations, instance method -invocations, and static/toplevel method invocations to be distinguished: +In addition, forms are added to allow constructor invocations, dynamic method +invocations, function object invocations, instance method invocations, and +static/toplevel method invocations to be distinguished. In these forms, `n_i: +m_i` (where `i` is an integer) is used as a convenient meta-syntax to refer to +an invocation argument `m_i` (an elaborated expression), possibly preceded by a +name selector `n_i:` (where `n_i` is a string). In this document, we use the +string `∅` to represent a name selector which is absent (meaning the +corresponding `m_i` is a positional argument rather than a named argument). + +The new invocation forms are as follows: - `@DYNAMIC_INVOKE(m_0.id(n_1: m_1, n_2: m_2, ...))` + _This covers invocations of user-definable binary and unary operators, method + invocations, and implicit uses of the `call` method, where the target has + static type `dynamic` or `Function`. For example, if `d` has static type + `dynamic`, the following expressions will be elaborated using + `@DYNAMIC_INVOKE`: `d.f()`, `-d`, `d + 0`, and `d()`._ + - `@FUNCTION_INVOKE(m_0.call(n_1: m_1, n_2: m_2, ...))` + _This covers invocations of expressions whose type is a function type (but not + `Function`). For example, if `l` has type `List`, then + `l.first()` will be elaborated using `@FUNCTION_INVOKE`._ + - `@INSTANCE_INVOKE(m_0.id(n_1: m_1, n_2: m_2, ...))` + _This covers invocations of user-definable binary and unary operators, method + invocations, and implicit uses of the `call` method, where the static type of + the target is the interface type of a class, mixin, enum, or extension + type. For example, if `i` has static type `int`, and the static type of `x` is + a class containing a `call` method, then the following expressions will be + elaborated using `@INSTANCE_INVOKE`: `i.abs()`, `-i`, `i + 1`, and `x()`._ + - `@STATIC_INVOKE(f(n_1: m_1, n_2: m_2, ...))` + _This covers invocations of static methods and top level methods. For example, + the following expressions will be elaborated using `@STATIC_INVOKE`: + `print(s)` and `int.tryParse(s)`._ + In each of these forms, each `m_i` represents an elaborated expression, each `T_i` represents a type, and each `n_i` represents an optional argument name identifier. When present, `id` represents an identifier or operator name, and `f` represents a static method or top level function. The semantics of each of these forms is to evaluate the `m_i` in sequence, then -perform the appropriate kind of method or function call. +perform the appropriate kind of method or function call. _The precise runtime +semantics are not specified here, however it should be noted that in the case of +`@DYNAMIC_INVOKE`, the name `id` may not be found in the target's runtime type +information at all (in which case `noSuchMethod` will be invoked), or `id` may +resolve to a getter (in which case the getter will be invoked, and then a +dynamic invocation of `call` will be attempted)._ ## Additional properties satisfied by elaborated expressions @@ -1263,8 +1296,8 @@ non-generic function or method, or when type arguments need to be inferred._ The output of argument part inference is a sequence of elaborated expressions `{m_1, m_2, ...}` (of the same length as the sequence of input expressions), a sequence of zero or more elaborated type arguments `{U_1, U_2, ...}`, and a -result type known as `R`. _(The sequence of optional names is unchanged by -argument part inference.)_ +result type `R`. _(The sequence of optional names is unchanged by argument part +inference.)_ To emphasize the relationship between argument part inference and the syntax of Dart source code, the inputs and outputs of argument part inference are @@ -1281,8 +1314,8 @@ The procedure for argument part inference is as follows: - Let `{X_1, X_2, ...}` be the list of formal type parameters in `F`, or an empty list if `F` is `∅`. -- Let `{P_1, P_2, ...}` be the list of formal parameter types corresponding to - `{e_1, e_2, ...}`, determined as follows: +- Let `{P_1, P_2, ...}` be the list of formal parameter type schemas + corresponding to `{e_1, e_2, ...}`, determined as follows: - If `F` is `∅`, then let each `P_i` be `_`. @@ -1330,17 +1363,17 @@ The procedure for argument part inference is as follows: - Initialize `{U_1, U_2, ...}` to a list of type schemas, of the same length as `{X_1, X_2, ...}`, each of which is `_`. - - Using subtype constraint generation, attempt to match `R_F` as a subtype - of `K` with respect to the list of type variables `{X_1, X_2, ...}`. + - Check whether `R_F` is a subtype match for `K` with respect to the list of + type variables `{X_1, X_2, ...}`. - If this succeeds, then accumulate the resulting list of type constraints into `C`. Then, let `{V_1, V_2, ...}` be the constraint solution for the - set of type variables `{X_1, X_2, ...}` with respect to the constaint - set `C`, with partial solution `{U_1, U_2, ...}`. Replace `{U_1, U_2, - ...}` with `{V_1, V_2, ...}`. _This step is known as "downwards - inference", since it has the effect of passing type information __down__ - the syntax tree from the context of the invocation to the context of the - arguments._ + set of type variables `{X_1, X_2, ...}` with respect to the constraint + set `C`, with partial solution `{U_1, U_2, ...}`. Let the new values of + `{U_1, U_2, ...}` be `{V_1, V_2, ...}`. _This step is known as + "downwards inference", since it has the effect of passing type + information __down__ the syntax tree from the context of the invocation + to the context of the arguments._ - Otherwise, leave `C` and `{U_1, U_2, ...}` unchanged. @@ -1369,18 +1402,27 @@ The procedure for argument part inference is as follows: has the effect that all arguments that are not function expressions are type inferred first, in the order in which they appear in source code, followed by all arguments that __are__ function expressions, possibly in a staged - fashion._ + fashion. The reason for traversing the non-function expressions in stage + zero before the function expressions is to allow any type promotions that + occur in the non-function expressions to carry over into the function + expressions, regardless of the order of the arguments. For example, `f(int? + i) => g(() { print(i+1); }, i!);` is accepted by type inference, because the + null check `i!` is guaranteed to execute before the function expression `() + { print(i+1); }` can ever be invoked. See + https://github.com/dart-lang/language/blob/main/accepted/2.18/horizontal-inference/feature-specification.md#why-do-we-defer-all-function-literals + for more information._ - If `F` has at least one formal type parameter, and there are zero type arguments `T` (_in other words, generic type inference is being performed_), then: - - For each `e_i` in stage _k_: + - For each `e_i` in stage _k_, in the order in which expression inference + was performed: - Let `S_i` be the static type of `m_i_preliminary`. - - Using subtype constraint generation, attempt to match `S_i` as a subtype - of `K_i` with respect to the list of type variables `{X_1, X_2, ...}`. + - Check whether `S_i` is a subtype match for `P_i` with respect to the + list of type variables `{X_1, X_2, ...}`. - If this succeeds, then accumulate the resulting list of type constraints into `C`. @@ -1391,21 +1433,21 @@ The procedure for argument part inference is as follows: - If _k_ is not the last stage in the argument partitioning, then let `{V_1, V_2, ...}` be the constraint solution for the set of type - variables `{X_1, X_2, ...}` with respect to the constaint set `C`, with - partial solution `{U_1, U_2, ...}`. Replace `{U_1, U_2, ...}` with - `{V_1, V_2, ...}`. _This step is known as "horizontal inference", since - it has the effect of passing type information __across__ the syntax tree - from the static type of some arguments to the context of other - arguments._ + variables `{X_1, X_2, ...}` with respect to the constraint set `C`, with + partial solution `{U_1, U_2, ...}`. Let the new values of `{U_1, U_2, + ...}` be `{V_1, V_2, ...}`. _This step is known as "horizontal + inference", since it has the effect of passing type information + __across__ the syntax tree from the static type of some arguments to the + context of other arguments._ - Otherwise (_k_ __is__ the last stage in the argument partitioning), let `{V_1, V_2, ...}` be the _grounded_ constraint solution for the set of - type variables `{X_1, X_2, ...}` with respect to the constaint set `C`, - with partial solution `{U_1, U_2, ...}`. Replace `{U_1, U_2, ...}` with - `{V_1, V_2, ...}`. _This step is known as "upwards inference", since it - has the effect of passing type information __up__ the syntax tree from - the static type of arguments to the inferred type arguments of the - invocation._ + type variables `{X_1, X_2, ...}` with respect to the constraint set `C`, + with partial solution `{U_1, U_2, ...}`. Let the new values of `{U_1, + U_2, ...}` be `{V_1, V_2, ...}`. _This step is known as "upwards + inference", since it has the effect of passing type information __up__ + the syntax tree from the static type of arguments to the inferred type + arguments of the invocation._ - _Note that at this point, all entries in `{U_1, U_2, ...}` have been obtained either from a _grounded_ constraint solution or from explicit types in the @@ -1465,7 +1507,10 @@ _Note that if `F` is `∅`, then the resulting graph has no edges._ _So, for example, if the invocation in question is this:_ ```dart -f((t, u) { ... } /* A */, () { ... } /* B */, (v) { ... } /* C */, (u) { ... } /* D */) +f((t, u) { ... }, // A + () { ... }, // B + (v) { ... }, // C + (u) { ... }) // D ``` _And the target of the invocation is declared like this:_ @@ -1537,6 +1582,16 @@ name identifiers `{n_1, n_2, ...}`, a sequence of zero or more type arguments `{T_1, T_2, ...}`, and a type schema `K`. As with [argument part inference](#Argument-part-inference), the symbol `∅` denotes a missing name. +_Method invocation inference is used for the following constructs:_ + +- _Explicit method invocations (e.g. `[].add(x)`), in which case `id` is the name of the method (`add` in this example)._ + +- _Call invocations (e.g. `f()`, where `f` is a local variable), in which case + `id` is `call`._ + +- _Invocations of user-definable operators (e.g. `1 + 2`), in which case `id` is + the name of the operator._ + The output of method invocation inference is an elaborated expression `m`, with static type `T`, where `m` and `T` are determined as follows: @@ -1550,9 +1605,9 @@ static type `T`, where `m` and `T` are determined as follows: then: - Invoke [argument part inference](#Argument-part-inference) on `(n_1: e_1, n_2: e_2, ...)`, using a target function type of `∅` and a - type schema `K`. Denote the resulting elaborated expressions by `{m_1, m_2, - ...}`. + ...>(n_1: e_1, n_2: e_2, ...)`, using `∅` as the target function type and + `K` as the context. Denote the resulting elaborated expressions by `{m_1, + m_2, ...}`. - Let `m` be `@DYNAMIC_INVOKE(m_0.id(n_1: m_1, n_2: m_2, ...))`. @@ -1583,10 +1638,10 @@ static type `T`, where `m` and `T` are determined as follows: then: - Invoke [argument part inference](#Argument-part-inference) on `(n_1: e_1, n_2: e_2, ...)`, using a target function type of `U_0` and a - type schema `K`. Denote the resulting elaborated expressions by `{m_1, m_2, - ...}`, the resulting elaborated type arguments by `{U_1, U_2, ...}`, and the - result type by `R`. + ...>(n_1: e_1, n_2: e_2, ...)`, using `U_0` as the target function type and + `K` as the context. Denote the resulting elaborated expressions by `{m_1, + m_2, ...}`, the resulting elaborated type arguments by `{U_1, U_2, ...}`, + and the result type by `R`. - Let `m` be `@FUNCTION_INVOKE(m_0.call(n_1: m_1, n_2: m_2, ...))`, and let `T` be `R`. _Soundness follows from the fact that the static @@ -1598,10 +1653,10 @@ static type `T`, where `m` and `T` are determined as follows: - Let `F` be the return type of `U_0`'s accessible instance getter named `id`. - Invoke [argument part inference](#Argument-part-inference) on `(n_1: e_1, n_2: e_2, ...)`, using a target function type of `F` and a - type schema `K`. Denote the resulting elaborated expressions by `{m_1, m_2, - ...}`, the resulting elaborated type arguments by `{U_1, U_2, ...}`, and the - result type by `R`. + ...>(n_1: e_1, n_2: e_2, ...)`, using `F` as the target function type and + `K` as the context. Denote the resulting elaborated expressions by `{m_1, + m_2, ...}`, the resulting elaborated type arguments by `{U_1, U_2, ...}`, + and the result type by `R`. - Let `m` be `@FUNCTION_INVOKE(m_0.id.call(n_1: m_1, n_2: m_2, ...))`, and let `T` be `R`. _Soundness follows from the fact that the static @@ -1614,10 +1669,18 @@ static type `T`, where `m` and `T` are determined as follows: - Let `F` be the type of `U_0`'s accessible instance method named `id`. - Invoke [argument part inference](#Argument-part-inference) on `(n_1: e_1, n_2: e_2, ...)`, using a target function type of `F` and a - type schema `K`. Denote the resulting elaborated expressions by `{m_1, m_2, - ...}`, the resulting elaborated type arguments by `{U_1, U_2, ...}`, and the - result type by `R`. + ...>(n_1: e_1, n_2: e_2, ...)`, using `F` as the target function type and + `K` as the context. Denote the resulting elaborated expressions by `{m_1, + m_2, ...}`, the resulting elaborated type arguments by `{U_1, U_2, ...}`, + and the result type by `R`. + + _TODO(paulberry): handle the possibility that `F` is not a function type (it + might even be `dynamic`). Note that the analyzer and CFE currently behave + slightly differently if `F` is an interface type that declares a getter + called `call`: the analyzer rejects this (`call` must be a method), but the + CFE accepts it, recursively desugaring `.call` invocations to arbitrary + depth. See https://github.com/dart-lang/language/issues/3482 for more + context._ - Let `m` be `@INSTANCE_INVOKE(m_0.id(n_1: m_1, n_2: m_2, ...))`, and let `T` be `R`. _Soundness follows from the fact that the static @@ -1702,11 +1765,15 @@ _TODO(paulberry): specify this._ ### Implicit this invocation If the selector chain consists of _<identifier> <argumentPart>_, and -_<identifier>_ __cannot__ be resolved to the name of a local variable, +_<identifier>_ __cannot__ be resolved using local scope resolution rules, then the result of selector chain type inference in context `K` is the elaborated expression `m`, with static type `T`, where `m` and `T` are determined as follows: +_TODO(paulberry): also handle the situation where <identifier> __can__ be +resolved using local scope resolution rules, but it resolves to a member of the +current class, mixin, enum, extension, or extension type._ + - Let `m_0` be `this`, with static type `T_0`, where `T_0` is the interface type of the immediately enclosing class, enum, mixin, or extension type, or the "on" type of the immediately enclosing extension. _The runtime behavior of `this` is @@ -1853,8 +1920,8 @@ _TODO(paulberry): specify this._ ### Implicit this method tearoff with type arguments If the selector chain consists of _<identifier> <typeArguments>_, -and _<identifier>_ __cannot__ be resolved to the name of a local variable, -then the result of selector chain type inference in context `K` is the +and _<identifier>_ __cannot__ be resolved using local scope resolution +rules, then the result of selector chain type inference in context `K` is the elaborated expression `m`, with static type `T`, where `m` and `T` are determined as follows: