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>
This commit is contained in:
Robert Griesemer 2021-11-30 09:29:45 -08:00
parent 8314544bd6
commit 654d5f4b5d
1 changed files with 382 additions and 3 deletions

View File

@ -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>