diff --git a/doc/go_spec.html b/doc/go_spec.html index 28aba70e4ffb3e..ae747d3a637cf7 100644 --- a/doc/go_spec.html +++ b/doc/go_spec.html @@ -1,6 +1,6 @@ @@ -4457,7 +4457,7 @@
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 @@
-
-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 example, given the type equation with the bound type parameter
+P
-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. -
++ [10]struct{ elem P, list []P } ≡A [10]struct{ elem string; list []string } +
-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.
+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.
-For example, if T1
and T2
are type parameters,
-[]map[int]bool
can be unified with any of the following:
+Unification uses a combination of exact and loose
+Unification (see Appendix) depending on whether two types have
+to be identical or simply
+assignment-compatible:
-[]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 --
-On the other hand, []map[int]bool
cannot be unified with any of
+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.
-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
+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:
-type Vector []float64 -+
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.
+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.
+
-and the type literal []E
, unification compares []float64
with
-[]E
and adds an entry E
→ float64
to
-the substitution map.
+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.