Type equations

January 5, 2024

I don’t have a lot to expand on in this section, except to offer a pre-amble about some technical terms and symbols that won’t be familiar to everyone:

  • is a symbol from mathematics that means “identical to”. It’s similar to = which we’re all famliar with, but “stricter”. The spec uses variants of this symbol in some following equations, so it’s nice to understand what the symbol means originally.
  • A means “are assignable to each other”, as in: X ≡A Y means “X is assignable to Y and Y is assignable to X”
  • C means “satisifes constraint”, as in: X ≡C ~int means “X satisfies constraint ~int”.
  • LHS & RHS stand for Left-Hand Side and Right-Hand Side, and refer to the different halves of an equation. In the equation x = y + 3, the Left-Hand Side (LHS) is x and the Right-Hand Side (RHS) is y + 3

So with that down, let’s read through what the spec has to say about type equations

Type inference

Each such pair of matched types corresponds to a type equation 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.

For example, given

// dedup returns a copy of the argument slice with any duplicate entries removed.
func dedup[S ~[]E, E comparable](S) S { … }

type Slice []int
var s Slice
s = dedup(s)   // same as s = dedup[Slice, int](s)

the variable s of type Slice must be assignable to the function parameter type S for the program to be valid. To reduce complexity, type inference ignores the directionality of assignments, so the type relationship between Slice and S can be expressed via the (symmetric) type equation Slice ≡A S (or 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 unification for details). Similarly, the type parameter S must satisfy its constraint ~[]E. This can be expressed as S ≡C ~[]E where X ≡C Y stands for “X satisfies constraint Y”. These observations lead to a set of two equations

  Slice ≡A S      (1)
  S     ≡C ~[]E   (2)

which now can be solved for the type parameters S and E. From (1) a compiler can infer that the type argument for S is Slice. Similarly, because the underlying type of Slice is []int and []int must match []E of the constraint, a compiler can infer that E must be int. Thus, for these two equations, type inference infers

	S ➞ Slice
	E ➞ int

Quotes from The Go Programming Language Specification Version of August 2, 2023

Share this

Direct to your inbox, daily. I respect your privacy .

Unsure? Browse the archive .

Related Content

Exact & loose type unification

Type unification … Unification uses a combination of exact and loose unification depending on whether two types have to be identical, assignment-compatible, or only structurally equal. The respective type unification rules are spelled out in detail in the Appendix. The precise definitions of “exact” and “loose” unification are buried in the appendix, and depend on the specific types involved. In general, I think it’s not terribly inaccurate to say that exact unification applies when the two types are identical, for composite types with identical structure (i.

Type unification

A couple of days ago we saw the spec reference the concept of “type unification”. Today we start through that explanation…. Type unification 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 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).

Successful type inference

Today we finish up the discussion on type inference. So we’ve now Type inference … If the two phases are successful, type inference determined a type argument for each bound type parameter: Pk ➞ Ak A type argument Ak may be a composite type, containing other bound type parameters Pk 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.