spec: add section on type inference

Change-Id: Ic338788d6410ed0d09ad129811377ee9ce5ed496
Reviewed-on: https://go-review.googlesource.com/c/go/+/367954
Trust: Robert Griesemer <gri@golang.org>
Reviewed-by: Ian Lance Taylor <iant@golang.org>

1 files changed, 382 insertions, 3 deletions

diff --git a/doc/go_spec.html b/doc/go_spec.html
index b25cf5fa6e..c653cbffc0 100644
--- a/doc/go_spec.html
+++ b/doc/go_spec.html
@@ -1,6 +1,6 @@
 <!--{
 	"Title": "The Go Programming Language Specification - Go 1.18 Draft (incomplete)",
-	"Subtitle": "Version of Jan 21, 2022",
+	"Subtitle": "Version of Jan 28, 2022",
 	"Path": "/ref/spec"
 }-->
 
@@ -4128,8 +4128,8 @@ with the same underlying array.
 <h3 id="Instantiations">Instantiations</h3>
 
 <p>
-A parameterized function or type is <i>instantiated</i> by substituting
-<i>type arguments</i> for the type parameters.
+A parameterized function or type is <i>instantiated</i> by substituting <i>type arguments</i>
+for the type parameters.
 Instantiation proceeds in two phases:
 </p>
 
@@ -4201,6 +4201,385 @@ b := min[float64](2.0, 3)  // b has value 2.0 of type float64
 c := min(b, -1)            // c has value -1.0 of type float64
 </pre>
 
+<h3 id="Type_inference">Type inference</h3>
+
+<p>
+Missing 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 implements the relevant constraint;
+it is possible for an inferred type argument to fail to implement a constraint, in which
+case instantiation fails.
+</p>
+
+<p>
+Type inference is based on
+</p>
+
+<ul>
+<li>
+	a <a href="#Type_parameter_lists">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</h3>
+
+<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> &RightArrow; <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:
+</p>
+
+<pre>
+[]map[int]bool   // types are identical
+T1               // adds T1 &RightArrow; []map[int]bool to substitution map
+[]T1             // adds T1 &RightArrow; map[int]bool to substitution map
+[]map[T1]T2      // adds T1 &RightArrow; int and T2 &RightArrow; bool to substitution map
+</pre>
+
+<p>
+On the other hand, <code>[]map[int]bool</code> cannot be unified with any of
+</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
+</p>
+
+<pre>
+type Vector []float64
+</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> &RightArrow; <code>float64</code> to
+the substitution map.
+</p>
+
+<h4 id="Function_argument_type_inference">Function argument type inference</h3>
+
+<!-- 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 type-parameterized function
+</p>
+
+<pre>
+func scale[Number ~int64|~float64|~complex128](v []Number, s Number) []Number
+</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> &RightArrow; <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.
+</p>
+
+<p>
+Function argument type inference can be used when the function has ordinary parameters
+whose types are defined using the function's type parameters. Inference happens in two
+separate phases; each phase operates on a specific list of (parameter, argument) pairs:
+</p>
+
+<ol>
+<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>.
+</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.
+</li>
+</ol>
+
+<p>
+Any other (parameter, argument) pair is ignored.
+</p>
+
+<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.
+</p>
+
+<p>
+Each list is processed in a separate phase:
+</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.
+</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.
+</li>
+</ol>
+
+<p>
+Example:
+</p>
+
+<pre>
+func min[T constraints.Ordered](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)
+</pre>
+
+<h4 id="Constraint_type_inference">Constraint type inference</h3>
+
+<!--
+	The next paragraph needs to be updated for the new definition of structural type:
+	The structural type of an interface is the single underlying type of its type set,
+	if it exists. But for constraint type inference, if the type set consists of exactly
+	one type, we want to use that one type (which may be a defined type, different from
+	its underlying == structural type).
+-->
+
+<p>
+Constraint type inference infers type arguments from already known
+type arguments by considering <a href="#Structure_of_interfaces">structural type constraints</a>:
+if the structural type <code>T</code> of a structural constraint is parameterized,
+<a href="#Type_unification">unifying</a> a known type argument with <code>T</code> may
+infer type arguments for other type parameters used by the structural type.
+</p>
+
+<p>
+For instance, consider the type parameter list with type parameters <code>List</code> and
+<code>Elem</code>:
+</p>
+
+<pre>
+[List ~[]Elem, Elem any]
+</pre>
+
+<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 structural constraint
+<code>~[]Elem</code> for <code>List</code>.
+If the type argument is <code>Bytes</code>:
+</p>
+
+<pre>
+type Bytes []byte
+</pre>
+
+<p>
+unifying the underlying type of <code>Bytes</code> with the structural constraint 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> &RightArrow; <code>byte</code>.
+Thus, in this example, constraint type inference can infer the second type argument from the
+first one.
+</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 a structural constraint, unify the type parameter with the structural
+type of its constraint. 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> &RightArrow; <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> &RightArrow; <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
+</p>
+
+<pre>
+[A any, B []C, C *A]
+</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> &RightArrow; <code>int</code>.
+</p>
+
+<p>
+In the first phase, the type parameters <code>B</code> and <code>C</code> are unified
+with the structural type of their respective constraints. This adds the entries
+<code>B</code> &RightArrow; <code>[]C</code> and <code>C</code> &RightArrow; <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> &RightArrow; <code>int</code>,
+<code>B</code> &RightArrow; <code>[]C</code>,
+<code>C</code> &RightArrow; <code>*A</code>
+</p>
+
+<p>
+Replace <code>A</code> on the right-hand side of &RightArrow; with <code>int</code>:
+</p>
+
+<p>
+<code>A</code> &RightArrow; <code>int</code>,
+<code>B</code> &RightArrow; <code>[]C</code>,
+<code>C</code> &RightArrow; <code>*int</code>
+</p>
+
+<p>
+Replace <code>C</code> on the right-hand side of &RightArrow; with <code>*int</code>:
+</p>
+
+<p>
+<code>A</code> &RightArrow; <code>int</code>,
+<code>B</code> &RightArrow; <code>[]*int</code>,
+<code>C</code> &RightArrow; <code>*int</code>
+</p>
+
+<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.
+</p>
+
 <h3 id="Operators">Operators</h3>
 
 <p>