# 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