diff options
author | Robert Griesemer <gri@golang.org> | 2023-07-31 09:41:33 -0700 |
---|---|---|
committer | Gopher Robot <gobot@golang.org> | 2023-07-31 17:13:23 +0000 |
commit | 4a14d9c9af995061723487d3a9f749246863078b (patch) | |
tree | 337a79d224cdc283a06b88298399fb35308f261b | |
parent | 978616433392369fbe26a189f00b078d2c4856fa (diff) | |
download | go-4a14d9c9af995061723487d3a9f749246863078b.tar.gz go-4a14d9c9af995061723487d3a9f749246863078b.zip |
[release-branch.go1.21] spec: update spec to version at tip
This updates the spec by copying over several recent CLs
describing the new type inference mechanisms.
Fixes #61659.
Change-Id: I750c901e73e0404f782a3632f5cd936e3775ae13
Reviewed-on: https://go-review.googlesource.com/c/go/+/514435
Reviewed-by: Robert Griesemer <gri@google.com>
Auto-Submit: Robert Griesemer <gri@google.com>
TryBot-Bypass: Robert Griesemer <gri@google.com>
Reviewed-by: Ian Lance Taylor <iant@google.com>
-rw-r--r-- | doc/go_spec.html | 695 |
1 files changed, 381 insertions, 314 deletions
diff --git a/doc/go_spec.html b/doc/go_spec.html index c2fa871eaa..d1b8bf2a91 100644 --- a/doc/go_spec.html +++ b/doc/go_spec.html @@ -1,6 +1,6 @@ <!--{ "Title": "The Go Programming Language Specification", - "Subtitle": "Version of June 14, 2023", + "Subtitle": "Version of July 31, 2023", "Path": "/ref/spec" }--> @@ -2511,7 +2511,7 @@ type ( <p> A type definition creates a new, distinct type with the same -<a href="#Types">underlying type</a> and operations as the given type +<a href="#Underlying_types">underlying type</a> and operations as the given type and binds an identifier, the <i>type name</i>, to it. </p> @@ -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 <a href="#Type_inference">inferred</a> 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: </p> <ul> @@ -4351,7 +4351,7 @@ Provided that they can be inferred, type arguments may be omitted entirely if th <a href="#Calls">called</a> with ordinary arguments, </li> <li> - <a href="#Assignment_statements">assigned</a> to a variable with an explicitly declared type, + <a href="#Assignment_statements">assigned</a> to a variable with a known type </li> <li> <a href="#Calls">passed as an argument</a> 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,402 +4406,323 @@ For a generic type, all type arguments must always be provided explicitly. <h3 id="Type_inference">Type inference</h3> <p> -<em>NOTE: This section is not yet up-to-date for Go 1.21.</em> +A use of a generic function may omit some or all type arguments if they can be +<i>inferred</i> 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 <a href="#Instantiations">instantiation</a> succeeds with the +inferred type arguments. +Otherwise, type inference fails and the program is invalid. </p> <p> -Missing function type arguments may be <i>inferred</i> 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 -<a href="#Implementing_an_interface">implements</a> 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 <a href="#Assignability">assignable</a> +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 +<a href="#Satisfying_a_type_constraint">satisfy</a> the constraint of its respective +type parameter. </p> <p> -Type inference is based on +Each such pair of matched types corresponds to a <i>type equation</i> 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. </p> -<ul> -<li> - a <a href="#Type_parameter_declarations">type parameter list</a> -</li> -<li> - a substitution map <i>M</i> initialized with the known type arguments, if any -</li> -<li> - a (possibly empty) list of ordinary function arguments (in case of a function call only) -</li> -</ul> - -<p> -and then proceeds with the following steps: -</p> - -<ol> -<li> - apply <a href="#Function_argument_type_inference"><i>function argument type inference</i></a> - to all <i>typed</i> ordinary function arguments -</li> -<li> - apply <a href="#Constraint_type_inference"><i>constraint type inference</i></a> -</li> -<li> - apply function argument type inference to all <i>untyped</i> ordinary function arguments - using the default type for each of the untyped function arguments -</li> -<li> - apply constraint type inference -</li> -</ol> - <p> -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. -</p> - -<p> -The substitution map <i>M</i> is carried through all steps, and each step may add entries to <i>M</i>. -The process stops as soon as <i>M</i> has a type argument for each type parameter or if an inference step fails. -If an inference step fails, or if <i>M</i> is still missing type arguments after the last step, type inference fails. -</p> - -<h4 id="Type_unification">Type unification</h4> - -<p> -Type inference is based on <i>type unification</i>. A single unification step -applies to a <a href="#Type_inference">substitution map</a> 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 <code>P</code> → <code>A</code> for each type -parameter <code>P</code> and corresponding known type argument <code>A</code>. -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. -</p> - -<p> -For unification, two types that don't contain any type parameters from the current type -parameter list are <i>equivalent</i> -if they are identical, or if they are channel types that are identical ignoring channel -direction, or if their underlying types are equivalent. -</p> - -<p> -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. -</p> - -<!-- -TODO(gri) Somewhere we need to describe the process of adding an entry to the - substitution map: if the entry is already present, the type argument - values are themselves unified. ---> - -<p> -For example, if <code>T1</code> and <code>T2</code> are type parameters, -<code>[]map[int]bool</code> can be unified with any of the following: +For example, given </p> <pre> -[]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 -</pre> - -<p> -On the other hand, <code>[]map[int]bool</code> cannot be unified with any of -</p> +// dedup returns a copy of the argument slice with any duplicate entries removed. +func dedup[S ~[]E, E comparable](S) S { … } -<pre> -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 +type Slice []int +var s Slice +s = dedup(s) // same as s = dedup[Slice, int](s) </pre> <p> -As an exception to this general rule, because a <a href="#Type_definitions">defined type</a> -<code>D</code> and a type literal <code>L</code> are never equivalent, -unification compares the underlying type of <code>D</code> with <code>L</code> instead. -For example, given the defined type +the variable <code>s</code> of type <code>Slice</code> must be assignable to +the function parameter type <code>S</code> for the program to be valid. +To reduce complexity, type inference ignores the directionality of assignments, +so the type relationship between <code>Slice</code> and <code>S</code> can be +expressed via the (symmetric) type equation <code>Slice ≡<sub>A</sub> S</code> +(or <code>S ≡<sub>A</sub> Slice</code> for that matter), +where the <code><sub>A</sub></code> in <code>≡<sub>A</sub></code> +indicates that the LHS and RHS types must match per assignability rules +(see the section on <a href="#Type_unification">type unification</a> for +details). +Similarly, the type parameter <code>S</code> must satisfy its constraint +<code>~[]E</code>. This can be expressed as <code>S ≡<sub>C</sub> ~[]E</code> +where <code>X ≡<sub>C</sub> Y</code> stands for +"<code>X</code> satisfies constraint <code>Y</code>". +These observations lead to a set of two equations </p> <pre> -type Vector []float64 + Slice ≡<sub>A</sub> S (1) + S ≡<sub>C</sub> ~[]E (2) </pre> <p> -and the type literal <code>[]E</code>, unification compares <code>[]float64</code> with -<code>[]E</code> and adds an entry <code>E</code> → <code>float64</code> to -the substitution map. -</p> - -<h4 id="Function_argument_type_inference">Function argument type inference</h4> - -<!-- In this section and the section on constraint type inference we start with examples -rather than have the examples follow the rules as is customary elsewhere in spec. -Hopefully this helps building an intuition and makes the rules easier to follow. --> - -<p> -Function argument type inference infers type arguments from function arguments: -if a function parameter is declared with a type <code>T</code> that uses -type parameters, -<a href="#Type_unification">unifying</a> the type of the corresponding -function argument with <code>T</code> may infer type arguments for the type -parameters used by <code>T</code>. -</p> - -<p> -For instance, given the generic function +which now can be solved for the type parameters <code>S</code> and <code>E</code>. +From (1) a compiler can infer that the type argument for <code>S</code> is <code>Slice</code>. +Similarly, because the underlying type of <code>Slice</code> is <code>[]int</code> +and <code>[]int</code> must match <code>[]E</code> of the constraint, +a compiler can infer that <code>E</code> must be <code>int</code>. +Thus, for these two equations, type inference infers </p> <pre> -func scale[Number ~int64|~float64|~complex128](v []Number, s Number) []Number + S ➞ Slice + E ➞ int </pre> <p> -and the call -</p> - -<pre> -var vector []float64 -scaledVector := scale(vector, 42) -</pre> - -<p> -the type argument for <code>Number</code> can be inferred from the function argument -<code>vector</code> by unifying the type of <code>vector</code> with the corresponding -parameter type: <code>[]float64</code> and <code>[]Number</code> -match in structure and <code>float64</code> matches with <code>Number</code>. -This adds the entry <code>Number</code> → <code>float64</code> to the -<a href="#Type_unification">substitution map</a>. -Untyped arguments, such as the second function argument <code>42</code> here, are ignored -in the first round of function argument type inference and only considered if there are -unresolved type parameters left. +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 <i>bound</i> type parameters. +For instance, in the <code>dedup</code> example above, the type parameters +<code>P</code> and <code>E</code> are bound to <code>dedup</code>. +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. </p> <p> -Inference happens in two separate phases; each phase operates on a specific list of -(parameter, argument) pairs: +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): </p> -<ol> +<ul> <li> - The list <i>Lt</i> contains all (parameter, argument) pairs where the parameter - type uses type parameters and where the function argument is <i>typed</i>. + <p> + For a function call <code>f(a<sub>0</sub>, a<sub>1</sub>, …)</code> where + <code>f</code> or a function argument <code>a<sub>i</sub></code> is + a generic function: + <br> + Each pair <code>(a<sub>i</sub>, p<sub>i</sub>)</code> of corresponding + function arguments and parameters where <code>a<sub>i</sub></code> is not an + <a href="#Constants">untyped constant</a> yields an equation + <code>typeof(p<sub>i</sub>) ≡<sub>A</sub> typeof(a<sub>i</sub>)</code>. + <br> + If <code>a<sub>i</sub></code> is an untyped constant <code>c<sub>j</sub></code>, + and <code>typeof(p<sub>i</sub>)</code> is a bound type parameter <code>P<sub>k</sub></code>, + the pair <code>(c<sub>j</sub>, P<sub>k</sub>)</code> is collected separately from + the type equations. + </p> </li> <li> - The list <i>Lu</i> contains all remaining pairs where the parameter type is a single - type parameter. In this list, the respective function arguments are untyped. + <p> + For an assignment <code>v = f</code> of a generic function <code>f</code> to a + (non-generic) variable <code>v</code> of function type: + <br> + <code>typeof(v) ≡<sub>A</sub> typeof(f)</code>. + </p> </li> -</ol> - -<p> -Any other (parameter, argument) pair is ignored. -</p> +<li> + <p> + For a return statement <code>return …, f, … </code> where <code>f</code> is a + generic function returned as a result to a (non-generic) result variable + <code>r</code> of function type: + <br> + <code>typeof(r) ≡<sub>A</sub> typeof(f)</code>. + </p> +</li> +</ul> <p> -By construction, the arguments of the pairs in <i>Lu</i> are <i>untyped</i> constants -(or the untyped boolean result of a comparison). And because <a href="#Constants">default types</a> -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. +Additionally, each type parameter <code>P<sub>k</sub></code> and corresponding type constraint +<code>C<sub>k</sub></code> yields the type equation +<code>P<sub>k</sub> ≡<sub>C</sub> C<sub>k</sub></code>. </p> <p> -Each list is processed in a separate phase: +Type inference gives precedence to type information obtained from typed operands +before considering untyped constants. +Therefore, inference proceeds in two phases: </p> <ol> <li> - In the first phase, the parameter and argument types of each pair in <i>Lt</i> - are unified. If unification succeeds for a pair, it may yield new entries that - are added to the substitution map <i>M</i>. If unification fails, type inference - fails. + <p> + The type equations are solved for the bound + type parameters using <a href="#Type_unification">type unification</a>. + If unification fails, type inference fails. + </p> </li> <li> - The second phase considers the entries of list <i>Lu</i>. 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 <a href="#Constants">default type</a> of the corresponding untyped argument is - unified. If unification fails, type inference fails. + <p> + For each bound type parameter <code>P<sub>k</sub></code> for which no type argument + has been inferred yet and for which one or more pairs + <code>(c<sub>j</sub>, P<sub>k</sub>)</code> with that same type parameter + were collected, determine the <a href="#Constant_expressions">constant kind</a> + of the constants <code>c<sub>j</sub></code> in all those pairs the same way as for + <a href="#Constant_expressions">constant expressions</a>. + The type argument for <code>P<sub>k</sub></code> is the + <a href="#Constants">default type</a> for the determined constant kind. + If a constant kind cannot be determined due to conflicting constant kinds, + type inference fails. + </p> </li> </ol> <p> -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. +If not all type arguments have been found after these two phases, type inference fails. </p> <p> -Example: +If the two phases are successful, type inference determined a type argument for each +bound type parameter: </p> <pre> -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) + P<sub>k</sub> ➞ A<sub>k</sub> </pre> <p> -In the example <code>min(1.0, 2)</code>, processing the function argument <code>1.0</code> -yields the substitution map entry <code>T</code> → <code>float64</code>. 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. -</p> - -<h4 id="Constraint_type_inference">Constraint type inference</h4> - -<p> -Constraint type inference infers type arguments by considering type constraints. -If a type parameter <code>P</code> has a constraint with a -<a href="#Core_types">core type</a> <code>C</code>, -<a href="#Type_unification">unifying</a> <code>P</code> with <code>C</code> -may infer additional type arguments, either the type argument for <code>P</code>, -or if that is already known, possibly the type arguments for type parameters -used in <code>C</code>. +A type argument <code>A<sub>k</sub></code> may be a composite type, +containing other bound type parameters <code>P<sub>k</sub></code> 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. </p> <p> -For instance, consider the type parameter list with type parameters <code>List</code> and -<code>Elem</code>: +If type arguments contain cyclic references to themselves +through bound type parameters, simplification and thus type +inference fails. +Otherwise, type inference succeeds. </p> -<pre> -[List ~[]Elem, Elem any] -</pre> +<h4 id="Type_unification">Type unification</h4> <p> -Constraint type inference can deduce the type of <code>Elem</code> from the type argument -for <code>List</code> because <code>Elem</code> is a type parameter in the core type -<code>[]Elem</code> of <code>List</code>. -If the type argument is <code>Bytes</code>: +Type inference solves type equations through <i>type unification</i>. +Type unification recursively compares the LHS and RHS types of an +equation, where either or both types may be or contain bound 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; this map is consulted and updated during type unification. +Initially, the bound type parameters are known but the map is empty. +During type unification, if a new type argument <code>A</code> is inferred, +the respective mapping <code>P ➞ A</code> 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. </p> -<pre> -type Bytes []byte </pre> - -<p> -unifying the underlying type of <code>Bytes</code> with the core type means -unifying <code>[]byte</code> with <code>[]Elem</code>. That unification succeeds and yields -the <a href="#Type_unification">substitution map</a> entry -<code>Elem</code> → <code>byte</code>. -Thus, in this example, constraint type inference can infer the second type argument from the -first one. -</p> - -<p> -Using the core type of a constraint may lose some information: In the (unlikely) case that -the constraint's type set contains a single <a href="#Type_definitions">defined type</a> -<code>N</code>, the corresponding core type is <code>N</code>'s underlying type rather than -<code>N</code> 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 <i>adjusted core type</i> of -a constraint: if the type set contains a single type, use that type; otherwise use the -constraint's core type. -</p> - -<p> -Generally, constraint type inference proceeds in two phases: Starting with a given -substitution map <i>M</i> -</p> - -<ol> -<li> -For all type parameters with an adjusted core type, unify the type parameter with that -type. If any unification fails, constraint type inference fails. -</li> - -<li> -At this point, some entries in <i>M</i> may map type parameters to other -type parameters or to types containing type parameters. For each entry -<code>P</code> → <code>A</code> in <i>M</i> where <code>A</code> is or -contains type parameters <code>Q</code> for which there exist entries -<code>Q</code> → <code>B</code> in <i>M</i>, substitute those -<code>Q</code> with the respective <code>B</code> in <code>A</code>. -Stop when no further substitution is possible. -</li> -</ol> - -<p> -The result of constraint type inference is the final substitution map <i>M</i> from type -parameters <code>P</code> to type arguments <code>A</code> where no type parameter <code>P</code> -appears in any of the <code>A</code>. -</p> - -<p> -For instance, given the type parameter list +For example, given the type equation with the bound type parameter +<code>P</code> </p> <pre> -[A any, B []C, C *A] + [10]struct{ elem P, list []P } ≡<sub>A</sub> [10]struct{ elem string; list []string } </pre> <p> -and the single provided type argument <code>int</code> for type parameter <code>A</code>, -the initial substitution map <i>M</i> contains the entry <code>A</code> → <code>int</code>. -</p> - -<p> -In the first phase, the type parameters <code>B</code> and <code>C</code> are unified -with the core type of their respective constraints. This adds the entries -<code>B</code> → <code>[]C</code> and <code>C</code> → <code>*A</code> -to <i>M</i>. - -<p> -At this point there are two entries in <i>M</i> where the right-hand side -is or contains type parameters for which there exists other entries in <i>M</i>: -<code>[]C</code> and <code>*A</code>. -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 <i>M</i> after the first phase: -</p> - -<p> -<code>A</code> → <code>int</code>, -<code>B</code> → <code>[]C</code>, -<code>C</code> → <code>*A</code> +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 <code>P</code> is not known yet (there is no map entry), +so unifying <code>P</code> with <code>string</code> adds +the mapping <code>P ➞ string</code> to the map. +Unifying the types of the <code>list</code> field requires +unifying <code>[]P</code> and <code>[]string</code> and +thus <code>P</code> and <code>string</code>. +Since the type argument for <code>P</code> is known at this point +(there is a map entry for <code>P</code>), its type argument +<code>string</code> takes the place of <code>P</code>. +And since <code>string</code> is identical to <code>string</code>, +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. </p> <p> -Replace <code>A</code> on the right-hand side of → with <code>int</code>: +Unification uses a combination of <i>exact</i> and <i>loose</i> +unification depending on whether two types have to be +<a href="#Type_identity">identical</a>, +<a href="#Assignability">assignment-compatible</a>, or +only structurally equal. +The respective <a href="#Type_unification_rules">type unification rules</a> +are spelled out in detail in the <a href="#Appendix">Appendix</a>. </p> <p> -<code>A</code> → <code>int</code>, -<code>B</code> → <code>[]C</code>, -<code>C</code> → <code>*int</code> +For an equation of the form <code>X ≡<sub>A</sub> Y</code>, +where <code>X</code> and <code>Y</code> 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. </p> <p> -Replace <code>C</code> on the right-hand side of → with <code>*int</code>: +For an equation of the form <code>P ≡<sub>C</sub> C</code>, +where <code>P</code> is a type parameter and <code>C</code> +its corresponding constraint, the unification rules are bit +more complicated: </p> -<p> -<code>A</code> → <code>int</code>, -<code>B</code> → <code>[]*int</code>, -<code>C</code> → <code>*int</code> -</p> +<ul> +<li> + If <code>C</code> has a <a href="#Core_types">core type</a> + <code>core(C)</code> + and <code>P</code> has a known type argument <code>A</code>, + <code>core(C)</code> and <code>A</code> must unify loosely. + If <code>P</code> does not have a known type argument + and <code>C</code> contains exactly one type term <code>T</code> + that is not an underlying (tilde) type, unification adds the + mapping <code>P ➞ T</code> to the map. +</li> +<li> + If <code>C</code> does not have a core type + and <code>P</code> has a known type argument <code>A</code>, + <code>A</code> must have all methods of <code>C</code>, if any, + and corresponding method types must unify exactly. +</li> +</ul> <p> -At this point no further substitution is possible and the map is full. -Therefore, <code>M</code> represents the final map of type parameters -to type arguments for the given type parameter list. +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. </p> <h3 id="Operators">Operators</h3> @@ -5479,7 +5400,7 @@ in any of these cases: ignoring struct tags (see below), <code>x</code>'s type and <code>T</code> are not <a href="#Type_parameter_declarations">type parameters</a> but have - <a href="#Type_identity">identical</a> <a href="#Types">underlying types</a>. + <a href="#Type_identity">identical</a> <a href="#Underlying_types">underlying types</a>. </li> <li> ignoring struct tags (see below), @@ -7324,7 +7245,8 @@ clear(t) type parameter see below </pre> <p> -If the argument type is a <a href="#Type_parameter_declarations">type parameter</a>, +If the type of the argument to <code>clear</code> is a +<a href="#Type_parameter_declarations">type parameter</a>, all types in its type set must be maps or slices, and <code>clear</code> performs the operation corresponding to the actual type argument. </p> @@ -8290,7 +8212,7 @@ of if the general conversion rules take care of this. <p> A <code>Pointer</code> is a <a href="#Pointer_types">pointer type</a> but a <code>Pointer</code> value may not be <a href="#Address_operators">dereferenced</a>. -Any pointer or value of <a href="#Types">underlying type</a> <code>uintptr</code> can be +Any pointer or value of <a href="#Underlying_types">underlying type</a> <code>uintptr</code> can be <a href="#Conversions">converted</a> to a type of underlying type <code>Pointer</code> and vice versa. The effect of converting between <code>Pointer</code> and <code>uintptr</code> is implementation-defined. </p> @@ -8438,3 +8360,148 @@ The following minimal alignment properties are guaranteed: <p> A struct or array type has size zero if it contains no fields (or elements, respectively) that have a size greater than zero. Two distinct zero-size variables may have the same address in memory. </p> + +<h2 id="Appendix">Appendix</h2> + +<h3 id="Type_unification_rules">Type unification rules</h3> + +<p> +The type unification rules describe if and how two types unify. +The precise details are relevant for Go implementations, +affect the specifics of error messages (such as whether +a compiler reports a type inference or other error), +and may explain why type inference fails in unusual code situations. +But by and large these rules can be ignored when writing Go code: +type inference is designed to mostly "work as expected", +and the unification rules are fine-tuned accordingly. +</p> + +<p> +Type unification is controlled by a <i>matching mode</i>, which may +be <i>exact</i> or <i>loose</i>. +As unification recursively descends a composite type structure, +the matching mode used for elements of the type, the <i>element matching mode</i>, +remains the same as the matching mode except when two types are unified for +<a href="#Assignability">assignability</a> (<code>≡<sub>A</sub></code>): +in this case, the matching mode is <i>loose</i> at the top level but +then changes to <i>exact</i> for element types, reflecting the fact +that types don't have to be identical to be assignable. +</p> + +<p> +Two types that are not bound type parameters unify exactly if any of +following conditions is true: +</p> + +<ul> +<li> + Both types are <a href="#Type_identity">identical</a>. +</li> +<li> + Both types have identical structure and their element types + unify exactly. +</li> +<li> + Exactly one type is an <a href="#Type_inference">unbound</a> + type parameter with a <a href="#Core_types">core type</a>, + and that core type unifies with the other type per the + unification rules for <code>≡<sub>A</sub></code> + (loose unification at the top level and exact unification + for element types). +</li> +</ul> + +<p> +If both types are bound type parameters, they unify per the given +matching modes if: +</p> + +<ul> +<li> + Both type parameters are identical. +</li> +<li> + At most one of the type parameters has a known type argument. + In this case, the type parameters are <i>joined</i>: + they both stand for the same type argument. + If neither type parameter has a known type argument yet, + a future type argument inferred for one the type parameters + is simultaneously inferred for both of them. +</li> +<li> + Both type parameters have a known type argument + and the type arguments unify per the given matching modes. +</li> +</ul> + +<p> +A single bound type parameter <code>P</code> and another type <code>T</code> unify +per the given matching modes if: +</p> + +<ul> +<li> + <code>P</code> doesn't have a known type argument. + In this case, <code>T</code> is inferred as the type argument for <code>P</code>. +</li> +<li> + <code>P</code> does have a known type argument <code>A</code>, + <code>A</code> and <code>T</code> unify per the given matching modes, + and one of the following conditions is true: + <ul> + <li> + Both <code>A</code> and <code>T</code> are interface types: + In this case, if both <code>A</code> and <code>T</code> are + also <a href="#Type_definitions">defined</a> types, + they must be <a href="#Type_identity">identical</a>. + Otherwise, if neither of them is a defined type, they must + have the same number of methods + (unification of <code>A</code> and <code>T</code> already + established that the methods match). + </li> + <li> + Neither <code>A</code> nor <code>T</code> are interface types: + In this case, if <code>T</code> is a defined type, <code>T</code> + replaces <code>A</code> as the inferred type argument for <code>P</code>. + </li> + <li> + In all other cases unification of <code>P</code> and <code>T</code> fails. + </li> + </ul> +</li> +</ul> + +<p> +Finally, two types that are not bound type parameters unify loosely +(and per the element matching mode) if: +</p> + +<ul> +<li> + Both types unify exactly. +</li> +<li> + One type is a <a href="#Type_definitions">defined type</a>, + the other type is a type literal, but not an interface, + and their underlying types unify per the element matching mode. +</li> +<li> + Both types are interfaces (but not type parameters) with + identical <a href="#Interface_types">type terms</a>, + both or neither embed the predeclared type + <a href="#Predeclared_identifiers">comparable</a>, + corresponding method types unify per the element matching mode, + and the method set of one of the interfaces is a subset of + the method set of the other interface. +</li> +<li> + Only one type is an interface (but not a type parameter), + corresponding methods of the two types unify per the element matching mode, + and the method set of the interface is a subset of + the method set of the other type. +</li> +<li> + Both types have the same structure and their element types + unify per the element matching mode. +</li> +</ul> |