From: Robert Griesemer Date: Thu, 15 Jun 2023 23:09:52 +0000 (-0700) Subject: spec: update section on type inference for Go 1.21 X-Git-Tag: go1.22rc1~1569 X-Git-Url: http://www.git.cypherpunks.su/?a=commitdiff_plain;h=a04a665a92714c71a039575d27155cd495891799;p=gostls13.git spec: update section on type inference for Go 1.21 The new section describes type inference as the problem of solving a set of type equations for bound type parameters. The next CL will update the section on unification to match the new inference approach. Change-Id: I2cb49bfb588ccc82d645343034096a82b7d602e2 Reviewed-on: https://go-review.googlesource.com/c/go/+/503920 TryBot-Bypass: Robert Griesemer Reviewed-by: Ian Lance Taylor Reviewed-by: Robert Griesemer Auto-Submit: Robert Griesemer --- diff --git a/doc/go_spec.html b/doc/go_spec.html index 9370cf632c..7099f36020 100644 --- a/doc/go_spec.html +++ b/doc/go_spec.html @@ -1,6 +1,6 @@ @@ -2511,7 +2511,7 @@ type (

A type definition creates a new, distinct type with the same -underlying type and operations as the given type +underlying type and operations as the given type and binds an identifier, the type name, to it.

@@ -4343,7 +4343,7 @@ type parameter list type arguments after substitution When using a generic function, type arguments may be provided explicitly, or they may be partially or completely inferred from the context in which the function is used. -Provided that they can be inferred, type arguments may be omitted entirely if the function is: +Provided that they can be inferred, type argument lists may be omitted entirely if the function is:

    @@ -4351,7 +4351,7 @@ Provided that they can be inferred, type arguments may be omitted entirely if th called with ordinary arguments,
  • - assigned to a variable with an explicitly declared type, + assigned to a variable with a known type
  • passed as an argument to another function, or @@ -4371,7 +4371,7 @@ must be inferrable from the context in which the function is used. // sum returns the sum (concatenation, for strings) of its arguments. func sum[T ~int | ~float64 | ~string](x... T) T { … } -x := sum // illegal: sum must have a type argument (x is a variable without a declared type) +x := sum // illegal: the type of x is unknown intSum := sum[int] // intSum has type func(x... int) int a := intSum(2, 3) // a has value 5 of type int b := sum[float64](2.0, 3) // b has value 5.0 of type float64 @@ -4406,71 +4406,223 @@ For a generic type, all type arguments must always be provided explicitly.

    Type inference

    -NOTE: This section is not yet up-to-date for Go 1.21. +A use of a generic function may omit some or all type arguments if they can be +inferred from the context within which the function is used, including +the constraints of the function's type parameters. +Type inference succeeds if it can infer the missing type arguments +and instantiation succeeds with the +inferred type arguments. +Otherwise, type inference fails and the program is invalid.

    -Missing function type arguments may be inferred by a series of steps, described below. -Each step attempts to use known information to infer additional type arguments. -Type inference stops as soon as all type arguments are known. -After type inference is complete, it is still necessary to substitute all type arguments -for type parameters and verify that each type argument -implements the relevant constraint; -it is possible for an inferred type argument to fail to implement a constraint, in which -case instantiation fails. +Type inference uses the type relationships between pairs of types for inference: +For instance, a function argument must be assignable +to its respective function parameter; this establishes a relationship between the +type of the argument and the type of the parameter. +If either of these two types contains type parameters, type inference looks for the +type arguments to substitute the type parameters with such that the assignability +relationship is satisfied. +Similarly, type inference uses the fact that a type argument must +satisfy the constraint of its respective +type parameter.

    -Type inference is based on +Each such pair of matched types corresponds to a type equation containing +one or multiple type parameters, from one or possibly multiple generic functions. +Inferring the missing type arguments means solving the resulting set of type +equations for the respective type parameters. +

    + +

    +For example, given +

    + +
    +// dedup returns a copy of the argument slice with any duplicate entries removed.
+func dedup[S ~[]E, E comparable](S) S { … }
+
+type Slice []int
+var s Slice
+s = dedup(s)   // same as s = dedup[Slice, int](s)
+
    + +

    +the variable s of type Slice must be assignable to +the function parameter type S for the program to be valid. +To reduce complexity, type inference ignores the directionality of assignments, +so the type relationship between Slice and S can be +expressed via the (symmetric) type equation Slice ≡A S +(or S ≡A Slice for that matter), +where the A in ≡A +indicates that the LHS and RHS types must match per assignability rules +(see the section on type unifcation for +details). +Similarly, the type parameter S must satisfy its constraint +~[]E. This can be expressed as S ≡C ~[]E +where X ≡C Y stands for +"X satisfies constraint Y". +These observations lead to a set of two equations +

    + +
    +	Slice ≡A S      (1)
+	S     ≡C ~[]E   (2)
+
    + +

    +which now can be solved for the type parameters S and E. +From (1) a compiler can infer that the type argument for S is Slice. +Similarly, because the underlying type of Slice is []int +and []int must match []E of the constraint, +a compiler can infer that E must be int. +Thus, for these two equations, type inference infers +

    + +
    +	S ➞ Slice
+	E ➞ int
+
    + +

    +Given a set of type equations, the type parameters to solve for are +the type parameters of the functions that need to be instantiated +and for which no explicit type arguments is provided. +These type parameters are called bound type parameters. +For instance, in the dedup example above, the type parameters +P and E are bound to dedup. +An argument to a generic function call may be a generic function itself. +The type parameters of that function are included in the set of bound +type parameters. +The types of function arguments may contain type parameters from other +functions (such as a generic function enclosing a function call). +Those type parameters may also appear in type equations but they are +not bound in that context. +Type equations are always solved for the bound type parameters only. +

    + +

    +Type inference supports calls of generic functions and assignments +of generic functions to (explicitly function-typed) variables. +This includes passing generic functions as arguments to other +(possibly also generic) functions, and returning generic functions +as results. +Type inference operates on a set of equations specific to each of +these cases. +The equations are as follows (type argument lists are omitted for clarity):

    • - a type parameter list +

      + For a function call f(a0, a1, …) where + f or a function argument ai is + a generic function: +
      + Each pair (ai, pi) of corresponding + function arguments and parameters where ai is not an + untyped constant yields an equation + typeof(pi) ≡A typeof(ai). +
      + If ai is an untyped constant cj, + and pi is a bound type parameter Pk, + the pair (cj, Pk) is collected separately from + the type equations. +

    • - a substitution map M initialized with the known type arguments, if any +

      + For an assignment v = f of a generic function f to a + (non-generic) variable v of function type: +
      + typeof(v) ≡A typeof(f). +

    • - a (possibly empty) list of ordinary function arguments (in case of a function call only) +

      + For a return statement return …, f, … where f is a + generic function returned as a result to a (non-generic) result variable + of function type: +
      + typeof(r) ≡A typeof(f). +

    -and then proceeds with the following steps: +Additionally, each type parameter Pk and corresponding type constraint +Ck yields the type equation +Pk ≡C Ck. +

    + +

    +Type inference gives precedence to type information obtained from typed operands +before considering untyped constants. +Therefore, inference proceeds in two phases:

    1. - apply function argument type inference - to all typed ordinary function arguments -
      2. -
    2. - apply constraint type inference -
      3. -
    3. - apply function argument type inference to all untyped ordinary function arguments - using the default type for each of the untyped function arguments +

      + The type equations are solved for the bound + type parameters using type unification. + If unification fails, type inference fails. +

    4. - apply constraint type inference +

      + For each bound type parameter Pk for which no type argument + has been inferred yet and for which one or more pairs + (cj, Pk) with that same type parameter + were collected, determine the constant kind + of the constants cj in all those pairs the same way as for + constant expressions. + The type argument for Pk is the + default type for the determined constant kind. + If a constant kind cannot be determined due to conflicting constant kinds, + type inference fails. +

    -If there are no ordinary or untyped function arguments, the respective steps are skipped. -Constraint type inference is skipped if the previous step didn't infer any new type arguments, -but it is run at least once if there are missing type arguments. +If not all type arguments have been found after these two phases, type inference fails.

    -The substitution map M is carried through all steps, and each step may add entries to M. -The process stops as soon as M has a type argument for each type parameter or if an inference step fails. -If an inference step fails, or if M is still missing type arguments after the last step, type inference fails. +If the two phases are successful, type inference determined a type argument for each +bound type parameter: +

    + +
    +	Pk ➞ Ak
+
    + +

    +A type argument Ak may be a composite type, +containing other bound type parameters Pk as element types +(or even be just another bound type parameter). +In a process of repeated simplification, the bound type parameters in each type +argument are substituted with the respective type arguments for those type +parameters until each type argument is free of bound type parameters. +

    + +

    +If type arguments contain cyclic references to themselves +through bound type parameters, simplification and thus type +inference fails. +Otherwise, type inference succeeds.

    Type unification

    +

    + +Note: This section is not up-to-date for Go 1.21. + +

    +

    Type inference is based on type unification. A single unification step applies to a substitution map and two types, either @@ -4546,264 +4698,6 @@ and the type literal []E, unification compares []float64 -

    Function argument type inference

    - - - -

    -Function argument type inference infers type arguments from function arguments: -if a function parameter is declared with a type T that uses -type parameters, -unifying the type of the corresponding -function argument with T may infer type arguments for the type -parameters used by T. -

    - -

    -For instance, given the generic function -

    - -
    -func scale[Number ~int64|~float64|~complex128](v []Number, s Number) []Number
-
    - -

    -and the call -

    - -
    -var vector []float64
-scaledVector := scale(vector, 42)
-
    - -

    -the type argument for Number can be inferred from the function argument -vector by unifying the type of vector with the corresponding -parameter type: []float64 and []Number -match in structure and float64 matches with Number. -This adds the entry Number → float64 to the -substitution map. -Untyped arguments, such as the second function argument 42 here, are ignored -in the first round of function argument type inference and only considered if there are -unresolved type parameters left. -

    - -

    -Inference happens in two separate phases; each phase operates on a specific list of -(parameter, argument) pairs: -

    - -
      -
    1. - The list Lt contains all (parameter, argument) pairs where the parameter - type uses type parameters and where the function argument is typed. -
      2. -
    2. - The list Lu contains all remaining pairs where the parameter type is a single - type parameter. In this list, the respective function arguments are untyped. -
      3. -
    - -

    -Any other (parameter, argument) pair is ignored. -

    - -

    -By construction, the arguments of the pairs in Lu are untyped constants -(or the untyped boolean result of a comparison). And because default types -of untyped values are always predeclared non-composite types, they can never match against -a composite type, so it is sufficient to only consider parameter types that are single type -parameters. -

    - -

    -Each list is processed in a separate phase: -

    - -
      -
    1. - In the first phase, the parameter and argument types of each pair in Lt - are unified. If unification succeeds for a pair, it may yield new entries that - are added to the substitution map M. If unification fails, type inference - fails. -
      2. -
    2. - The second phase considers the entries of list Lu. Type parameters for - which the type argument has already been determined are ignored in this phase. - For each remaining pair, the parameter type (which is a single type parameter) and - the default type of the corresponding untyped argument is - unified. If unification fails, type inference fails. -
      3. -
    - -

    -While unification is successful, processing of each list continues until all list elements -are considered, even if all type arguments are inferred before the last list element has -been processed. -

    - -

    -Example: -

    - -
    -func min[T ~int|~float64](x, y T) T
-
-var x int
-min(x, 2.0)    // T is int, inferred from typed argument x; 2.0 is assignable to int
-min(1.0, 2.0)  // T is float64, inferred from default type for 1.0 and matches default type for 2.0
-min(1.0, 2)    // illegal: default type float64 (for 1.0) doesn't match default type int (for 2)
-
    - -

    -In the example min(1.0, 2), processing the function argument 1.0 -yields the substitution map entry T → float64. Because -processing continues until all untyped arguments are considered, an error is reported. This -ensures that type inference does not depend on the order of the untyped arguments. -

    - -

    Constraint type inference

    - -

    -Constraint type inference infers type arguments by considering type constraints. -If a type parameter P has a constraint with a -core type C, -unifying P with C -may infer additional type arguments, either the type argument for P, -or if that is already known, possibly the type arguments for type parameters -used in C. -

    - -

    -For instance, consider the type parameter list with type parameters List and -Elem: -

    - -
    -[List ~[]Elem, Elem any]
-
    - -

    -Constraint type inference can deduce the type of Elem from the type argument -for List because Elem is a type parameter in the core type -[]Elem of List. -If the type argument is Bytes: -

    - -
    -type Bytes []byte
-
    - -

    -unifying the underlying type of Bytes with the core type means -unifying []byte with []Elem. That unification succeeds and yields -the substitution map entry -Elem → byte. -Thus, in this example, constraint type inference can infer the second type argument from the -first one. -

    - -

    -Using the core type of a constraint may lose some information: In the (unlikely) case that -the constraint's type set contains a single defined type -N, the corresponding core type is N's underlying type rather than -N itself. In this case, constraint type inference may succeed but instantiation -will fail because the inferred type is not in the type set of the constraint. -Thus, constraint type inference uses the adjusted core type of -a constraint: if the type set contains a single type, use that type; otherwise use the -constraint's core type. -

    - -

    -Generally, constraint type inference proceeds in two phases: Starting with a given -substitution map M -

    - -
      -
    1. -For all type parameters with an adjusted core type, unify the type parameter with that -type. If any unification fails, constraint type inference fails. -
      2. - -
    2. -At this point, some entries in M may map type parameters to other -type parameters or to types containing type parameters. For each entry -P → A in M where A is or -contains type parameters Q for which there exist entries -Q → B in M, substitute those -Q with the respective B in A. -Stop when no further substitution is possible. -
      3. -
    - -

    -The result of constraint type inference is the final substitution map M from type -parameters P to type arguments A where no type parameter P -appears in any of the A. -

    - -

    -For instance, given the type parameter list -

    - -
    -[A any, B []C, C *A]
-
    - -

    -and the single provided type argument int for type parameter A, -the initial substitution map M contains the entry A → int. -

    - -

    -In the first phase, the type parameters B and C are unified -with the core type of their respective constraints. This adds the entries -B → []C and C → *A -to M. - -

    -At this point there are two entries in M where the right-hand side -is or contains type parameters for which there exists other entries in M: -[]C and *A. -In the second phase, these type parameters are replaced with their respective -types. It doesn't matter in which order this happens. Starting with the state -of M after the first phase: -

    - -

    -A → int, -B → []C, -C → *A -

    - -

    -Replace A on the right-hand side of → with int: -

    - -

    -A → int, -B → []C, -C → *int -

    - -

    -Replace C on the right-hand side of → with *int: -

    - -

    -A → int, -B → []*int, -C → *int -

    - -

    -At this point no further substitution is possible and the map is full. -Therefore, M represents the final map of type parameters -to type arguments for the given type parameter list. -

    -

    Operators

    @@ -5479,7 +5373,7 @@ in any of these cases: ignoring struct tags (see below), x's type and T are not type parameters but have - identical underlying types. + identical underlying types.

  • ignoring struct tags (see below), @@ -8291,7 +8185,7 @@ of if the general conversion rules take care of this.

    A Pointer is a pointer type but a Pointer value may not be dereferenced. -Any pointer or value of underlying type uintptr can be +Any pointer or value of underlying type uintptr can be converted to a type of underlying type Pointer and vice versa. The effect of converting between Pointer and uintptr is implementation-defined.