Clean-ups to horizontal inference feature specification. (#2236)

Author: stereotype441

accepted/future-releases/horizontal-inference/feature-specification.md

@@ -1,6 +1,6 @@
 # Horizontal inference
 
-Author: [email protected], Version: 1.0 (See [Changelog](#Changelog) at end)
+Author: [email protected], Version: 1.2 (See [Changelog](#Changelog) at end)
 
 Horizontal inference allows certain arguments of an invocation (specifically
 function literals) to be type inferred in a context derived from the type of
@@ -38,7 +38,7 @@ var largestValue = values.fold(0, (a, b) => a < b ? b : a);
 Today this doesn't work, because without the leading `int`, the downwards
 inference phase of type inference has no information with which to choose a
 preliminary type for the type parameter `T`, so the type context used for
-inference of the function literal `(a, b) => a < b ? b : a` is `? Function(?,
+inference of the function literal `(a, b) => a < b ? b : a` is `_ Function(_,
 int)`.  Hence, `a` gets assigned a static type of `Object?`, and this leads to a
 compile error at `a < b`.
 
@@ -114,11 +114,15 @@ In this document we make use of the following terms:
   normal Dart type syntax, extended with a type known as "the unknown type"
   (denoted `_`), which allows representation of incomplete type information.
 
-- An expression's "type context" is a type schema representing what is known
-  about the probable type of the expression just before the portion of the type
-  inference algorithm that visits it.  This, together with other information
-  defined in [flow analysis][], constitutes the _input_ to the corresponding
-  type inference step.
+- An expression's "type context" is a type schema representing information
+  captured by the type inference algorithm from the context surrounding it.  In
+  most circumstances, it represents the set of static types that the expression
+  could have without provoking a static error.  _(There are a few exceptions;
+  for example the context of the RHS of an assignment to a promoted variable is
+  the set of types that the expression could have without causing the variable
+  to be demoted)._ The type context of an expression, together with other
+  information defined in [flow analysis][], constitutes the **input** to the
+  corresponding type inference step.
 
 - An "implicit type argument" is a type argument to a generic invocation whose
   precise value is not directly specified in code, but is instead determined
@@ -141,22 +145,27 @@ In this document we make use of the following terms:
   a type variable based on a set of constraints.  It may contain occurrences of
   the unknown type.
 
+- The "constraint solution for a set of type variables" (defined
+  [here][constraint solution for a set of type variables]) is a mapping from
+  type variables to type schemas, formed from a set of constraints and a partial
+  solution.  Typically, each type variable is mapped to the result of solving
+  the constraints that apply to it (according to the bullet above), plus an
+  additional constraint based on the bound of the type variable.  The partial
+  solution is used to break loops when the bound of one type variable refers to
+  others, and to effectively "freeze" the solution of each variable at the time
+  it becomes fully known (that is, it does not contain `_`).
+
 - The "grounded constraint solution for a type variable" (defined
   [here][grounded constraint solution for a type variable]) is a final
-  assignment of a type to a type schema based on a set of constraints.  It is a
-  type, not a type schema, so it may not contain occurrences of the unknown
+  assignment of a type to a type variable based on a set of constraints.  It is
+  a type, not a type schema, so it may not contain occurrences of the unknown
   type.
 
-- The "(possibly grounded) constraint solution for a set of type variables,
-  considering bounds" is a mapping from type variables to type schemas (or, in
-  the grounded case, types), formed from a set of constraints.  Each type
-  variable is mapped to the result of solving the constraints that apply to it
-  (according to one of the two bullets above), plus an additional constraint
-  based on the bound of the type variable.  Since the bounds of some type
-  variables may depend on the values of others, the exact algorithm for this is
-  subtle, and depends on the order in which the type variables are considered.
-  The exact algorithm is outside the scope of this document; unfortunately I
-  haven't found an exact specification for it.
+- The "grounded constraint solution for a set of type variables" (defined
+  [here][grounded constraint solution for a set of type variables]) is a final
+  mapping from type variables to types, formed from a set of constraints and a
+  partial solution.  It parallels the corresponding definition for the
+  non-grounded constraint solution.
 
 - A "function literal expression" is a syntactic construct that consists of a
   _\<functionExpression\>_, possibly enclosed in parentheses, and possibly
@@ -178,7 +187,9 @@ In this document we make use of the following terms:
 [type constraints]: https://github.com/dart-lang/language/blob/master/resources/type-system/inference.md#type-constraints
 [subtype constraint generation]: https://github.com/dart-lang/language/blob/master/resources/type-system/inference.md#subtype-constraint-generation
 [constraint solution for a type variable]: https://github.com/dart-lang/language/blob/master/resources/type-system/inference.md#constraint-solution-for-a-type-variable
+[constraint solution for a set of type variables]: https://github.com/dart-lang/language/blob/master/resources/type-system/inference.md#constraint-solution-for-a-set-of-type-variables
 [grounded constraint solution for a type variable]: https://github.com/dart-lang/language/blob/master/resources/type-system/inference.md#grounded-constraint-solution-for-a-type-variable
+[grounded constraint solution for a set of type variables]: https://github.com/dart-lang/language/blob/master/resources/type-system/inference.md#grounded-constraint-solution-for-a-set-of-type-variables
 
 ## Type inference algorithm for invocations
 
@@ -209,8 +220,10 @@ Performing type inference on an invocation consists of the following steps:
    try to match the return type of the target function type as a subtype of the
    invocation's type context.  This produces an initial set of type constraints.
    Then, using those constraints, find the constraint solution for the target
-   function type's type variables, considering bounds.  This produces a
-   preliminary mapping of type variables to type schemas.
+   function type's type variables, using an initial partial solution that maps
+   all type variables to the unknown type.  This produces a preliminary partial
+   solution for the inferred types, which will be updated in later type
+   inference steps.
 
 4. Visit arguments: Partition the arguments into stages (see [argument
    partitioning](#Argument-partitioning) below), and then for each stage _k_, do
@@ -246,15 +259,17 @@ Performing type inference on an invocation consists of the following steps:
 
    * Horizontal inference: if generic inference is needed, and this is not the
      last stage, use all the type constraints gathered so far to find the
-     constraint solution for the target function's type variables, considering
-     bounds.  This produces an updated preliminary mapping of type parameters to
-     type schemas.
+     constraint solution for the target function's type variables, using the
+     preliminary partial solution from the most recent previous execution of
+     either this step or step 3.  This produces an updated partial solution for
+     the inferred types.
 
 5. Upwards inference: if generic inference is needed, use all the type
    constraints gathered so far to find the **grounded** constraint solution for
-   the target function's type variables, considering bounds.  This produces the
-   final mapping of type parameters to type schemas.  Check that each type is a
-   subtype of the bound of its corresponding type parameter.
+   the target function's type variables, using the preliminary partial solution
+   from the most recent execution of step 4.  This produces the final solution
+   for the inferred types.  Check that each inferred type is a subtype of the
+   bound of its corresponding type parameter.
 
 6. Type checking: Check that the static type of each argument is assignable to
    the type obtained by substituting the final mapping (from step 5) into the
@@ -464,6 +479,17 @@ invocation target isn’t generic._
 
 ## Changelog
 
+### 1.2
+
+- Use `_` consistently to refer to the "unknown" type schema.
+
+- Clarify what is meant by the term "type schema".
+
+- Clarify the notions of "constraint solution for a set of type variables" and
+  "grounded constraint solution for a set of type variables".  These are now
+  defined in `resources/type-system/inference.md`, so we include links to their
+  definitions.
+
 ### 1.1
 
 - Add "terminology" section, with references to other docs, and improve

resources/type-system/inference.md

@@ -6,6 +6,12 @@ Status: Draft
 
 ## CHANGELOG
 
+2022.05.12
+  - Define the notions of "constraint solution for a set of type variables" and
+    "Grounded constraint solution for a set of type variables".  These
+    definitions capture how type inference handles type variable bounds, as well
+    as how inferred types become "frozen" once they are fully known.
+
 2019.09.01
   - Fix incorrect placement of left top rule in constraint solving.
 
@@ -680,6 +686,39 @@ The constraint solution for a type variable `X` with respect to a constraint set
 Note that the constraint solution is a type schema, and hence may contain
 occurences of the unknown type.
 
+#### Constraint solution for a set of type variables
+
+The constraint solution for a set of type variables `{X0, ..., Xn}` with respect
+to a constraint set `C` and partial solution `{T0, ..., Tn}`, is defined to be
+the set of type schemas `{U0, ..., Un}` such that:
+  - If `Ti` is known (that is, does not contain `_`), then `Ui = Ti`.  _(Note
+    that the upcoming "variance" feature will relax this rule so that it only
+    applies to type variables without an explicitly declared variance.)_
+  - Otherwise, let `Vi` be the constraint solution for the type variable `Xi`
+    with respect to the constraint set `C`.
+  - If `Vi` is not known (that is, it contains `_`), then `Ui = Vi`.
+  - Otherwise, if `Xi` does not have an explicit bound, then `Ui = Vi`.
+  - Otherwise, let `Bi` be the bound of `Xi`.  Then, let `Bi'` be the type
+    schema formed by substituting type schemas `{U0, ..., Ui-1, Ti, ..., Tn}` in
+    place of the type variables `{X0, ..., Xn}` in `Bi`.  _(That is, we
+    substitute `Uj` for `Xj` when `j < i` and `Tj` for `Xj` when `j >= i`)._
+    Then `Ui` is the constraint solution for the type variable `Xi` with respect
+    to the constraint set `C + (X <: Bi')`.
+
+_This definition can perhaps be better understood in terms of the practical
+consequences it has on type inference:_
+  - _Once type inference has determined a known type for a type variable (that
+    is, a type that does not contain `_`), that choice is frozen and is not
+    affected by later type inference steps.  (Type inference accomplishes this
+    by passing in any frozen choices as part of the partial solution)._
+  - _The bound of a type variable is only included as a constraint when the
+    choice of type for that type variable is about to be frozen._
+  - _During each round of type inference, type variables are inferred left to
+    right.  If the bound of one type variable refers to one or more type
+    variables, then at the time the bound is included as a constraint, the type
+    variables it refers to are assumed to take on the type schemas most recently
+    assigned to them by type inference._
+
 #### Grounded constraint solution for a type variable
 
 The grounded constraint solution for a type variable `X` with respect to a
@@ -696,6 +735,26 @@ constraint set `C` is define as follows:
 Note that the grounded constraint solution is a type, and hence may not contain
 occurences of the unknown type.
 
+#### Grounded constraint solution for a set of type variables
+
+The grounded constraint solution for a set of type variables `{X0, ..., Xn}`
+with respect to a constraint set `C`, with partial solution `{T0, ..., Tn}`, is
+defined to be the set of types `{U0, ..., Un}` such that:
+  - If `Ti` is known (that is, does not contain `_`), then `Ui = Ti`.  _(Note
+    that the upcoming "variance" feature will relax this rule so that it only
+    applies to type variables without an explicitly declared variance.)_
+  - Otherwise, if `Xi` does not have an explicit bound, then `Ui` is the
+    grounded constraint solution for the type variable `Xi` with respect to the
+    constraint set `C`.
+  - Otherwise, let `Bi` be the bound of `Xi`.  Then, let `Bi'` be the type
+    schema formed by substituting type schemas `{U0, ..., Ui-1, Ti, ..., Tn}` in
+    place of the type variables `{X0, ..., Xn}` in `Bi`.  _(That is, we
+    substitute `Uj` for `Xj` when `j < i` and `Tj` for `Xj` when `j >= i`)._
+    Then `Ui` is the grounded constraint solution for the type variable `Xi`
+    with respect to the constraint set `C + (X <: Bi')`.
+
+_This definition parallels the definition of the (non-grounded) constraint
+solution for a set of type variables._
 
 #### Constrained type variables