From 7fed33815cf57bf8d6b6ddfbd2ce0f5d8180b4f6 Mon Sep 17 00:00:00 2001 From: Robert Griesemer Date: Fri, 30 Jun 2023 14:54:34 -0700 Subject: [PATCH] spec: update section on type unification for Go 1.21 This leaves the specific unification details out in favor of a (forthcoming) section in an appendix. Change-Id: If984c48bdf71c278e1a2759f9a18c51ef58df999 Reviewed-on: https://go-review.googlesource.com/c/go/+/507417 Reviewed-by: Robert Griesemer Auto-Submit: Robert Griesemer Reviewed-by: Ian Lance Taylor TryBot-Bypass: Robert Griesemer --- doc/go_spec.html | 154 +++++++++++++++++++++++++++-------------------- 1 file changed, 89 insertions(+), 65 deletions(-) diff --git a/doc/go_spec.html b/doc/go_spec.html index 28aba70e4ff..ae747d3a637 100644 --- a/doc/go_spec.html +++ b/doc/go_spec.html @@ -1,6 +1,6 @@ @@ -4457,7 +4457,7 @@ 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 +(see the section on type unification for details). Similarly, the type parameter S must satisfy its constraint ~[]E. This can be expressed as S ≡C ~[]E @@ -4618,84 +4618,108 @@ Otherwise, type inference succeeds.

Type unification

- -Note: This section is not up-to-date for Go 1.21. - +Type inference solves type equations through type unification. +Type unification recursively compares the LHS and RHS types of an +equation, where either or both types may be or contain type parameters, +and looks for type arguments for those type parameters such that the LHS +and RHS match (become identical or assignment-compatible, depending on +context). +To that effect, type inference maintains a map of bound type parameters +to inferred type arguments. +Initially, the type parameters are known but the map is empty. +During type unification, if a new type argument A is inferred, +the respective mapping P ➞ A from type parameter to argument +is added to the map. +Conversely, when comparing types, a known type argument +(a type argument for which a map entry already exists) +takes the place of its corresponding type parameter. +As type inference progresses, the map is populated more and more +until all equations have been considered, or until unification fails. +Type inference succeeds if no unification step fails and the map has +an entry for each type parameter.

-

-Type inference is based on type unification. A single unification step -applies to a substitution map and two types, either -or both of which may be or contain type parameters. The substitution map tracks -the known (explicitly provided or already inferred) type arguments: the map -contains an entry P → A for each type -parameter P and corresponding known type argument A. -During unification, known type arguments take the place of their corresponding type -parameters when comparing types. Unification is the process of finding substitution -map entries that make the two types equivalent. -

- -

-For unification, two types that don't contain any type parameters from the current type -parameter list are equivalent -if they are identical, or if they are channel types that are identical ignoring channel -direction, or if their underlying types are equivalent. -

- -

-Unification works by comparing the structure of pairs of types: their structure -disregarding type parameters must be identical, and types other than type parameters -must be equivalent. -A type parameter in one type may match any complete subtype in the other type; -each successful match causes an entry to be added to the substitution map. -If the structure differs, or types other than type parameters are not equivalent, -unification fails. -

- - - -

-For example, if T1 and T2 are type parameters, -[]map[int]bool can be unified with any of the following: + +For example, given the type equation with the bound type parameter +P 

-[]map[int]bool   // types are identical
-T1               // adds T1 → []map[int]bool to substitution map
-[]T1             // adds T1 → map[int]bool to substitution map
-[]map[T1]T2      // adds T1 → int and T2 → bool to substitution map
+	[10]struct{ elem P, list []P } ≡A [10]struct{ elem string; list []string }

-On the other hand, []map[int]bool cannot be unified with any of +type inference starts with an empty map. +Unification first compares the top-level structure of the LHS and RHS +types. +Both are arrays of the same length; they unify if the element types unify. +Both element types are structs; they unify if they have +the same number of fields with the same names and if the +field types unify. +The type argument for P is not known yet (there is no map entry), +so unifying P with string adds +the mapping P ➞ string to the map. +Unifying the types of the list field requires +unifying []P and []string and +thus P and string. +Since the type argument for P is known at this point +(there is a map entry for P), its type argument +string takes the place of P. +And since string is identical to string, +this unification step succeeds as well. +Unification of the LHS and RHS of the equation is now finished. +Type inference succeeds because there is only one type equation, +no unification step failed, and the map is fully populated.

-
-int              // int is not a slice
-struct{}         // a struct is not a slice
-[]struct{}       // a struct is not a map
-[]map[T1]string  // map element types don't match
-
-

-As an exception to this general rule, because a defined type -D and a type literal L are never equivalent, -unification compares the underlying type of D with L instead. -For example, given the defined type +Unification uses a combination of exact and loose +Unification (see Appendix) depending on whether two types have +to be identical or simply +assignment-compatible:

-
-type Vector []float64
-
+

+For an equation of the form X ≡A Y, +where X and Y are types involved +in an assignment (including parameter passing and return statements), +the top-level type structures may unify loosely but element types +must unify exactly, matching the rules for assignments. +

-and the type literal []E, unification compares []float64 with -[]E and adds an entry E → float64 to -the substitution map. +For an equation of the form P ≡C C, +where P is a type parameter and C +its corresponding constraint, the unification rules are bit +more complicated: +

+ +
    +
  • + If C has a core type + core(C) + and P has a known type argument A, + core(C) and A must unify loosely. + If P does not have a known type argument + and C contains exactly one type term T + that is not an underlying (tilde) type, unification adds the + mapping P ➞ T to the map. +
    • +
  • + If C does not have a core type + and P has a known type argument A, + A must have all methods of C, if any, + and corresponding method types must unify exactly. +
    • +
+ +

+When solving type equations from type constraints, +solving one equation may infer additional type arguments, +which in turn may enable solving other equations that depend +on those type arguments. +Type inference repeats type unification as long as new type +arguments are inferred.

Operators