diff options
author | Robert Griesemer <gri@golang.org> | 2023-06-30 14:54:34 -0700 |
---|---|---|
committer | Gopher Robot <gobot@golang.org> | 2023-07-26 00:02:26 +0000 |
commit | 7fed33815cf57bf8d6b6ddfbd2ce0f5d8180b4f6 (patch) | |
tree | 68f22866ec247604612653c5192bbc044134ad2e /doc/go_spec.html | |
parent | 12bd2445afffbf229bafc538260c37b5dc176479 (diff) | |
download | go-7fed33815cf57bf8d6b6ddfbd2ce0f5d8180b4f6.tar.gz go-7fed33815cf57bf8d6b6ddfbd2ce0f5d8180b4f6.zip |
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 <gri@google.com>
Auto-Submit: Robert Griesemer <gri@google.com>
Reviewed-by: Ian Lance Taylor <iant@google.com>
TryBot-Bypass: Robert Griesemer <gri@google.com>
Diffstat (limited to 'doc/go_spec.html')
-rw-r--r-- | doc/go_spec.html | 146 |
1 files changed, 85 insertions, 61 deletions
diff --git a/doc/go_spec.html b/doc/go_spec.html index 28aba70e4f..ae747d3a63 100644 --- a/doc/go_spec.html +++ b/doc/go_spec.html @@ -1,6 +1,6 @@ <!--{ "Title": "The Go Programming Language Specification", - "Subtitle": "Version of July 20, 2023", + "Subtitle": "Version of July 25, 2023", "Path": "/ref/spec" }--> @@ -4457,7 +4457,7 @@ 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 unifcation</a> for +(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> @@ -4618,84 +4618,108 @@ Otherwise, type inference succeeds. <h4 id="Type_unification">Type unification</h4> <p> -<em> -Note: This section is not up-to-date for Go 1.21. -</em> +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 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 <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> -<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. +</pre> +For example, given the type equation with the bound type parameter +<code>P</code> </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> +<pre> + [10]struct{ elem P, list []P } ≡<sub>A</sub> [10]struct{ elem string; list []string } +</pre> <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. +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> -<!-- -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: +Unification uses a combination of <i>exact</i> and <i>loose</i> +Unification (see Appendix) depending on whether two types have +to be <a href="#Type_identity">identical</a> or simply +<a href="#Assignability">assignment-compatible</a>: </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 +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> -<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 -</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 +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> -<pre> -type Vector []float64 -</pre> +<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> -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. +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> |