Exact & loose type unification

January 23, 2024

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.e. two structs or slices) and the elements of said type are identical, and other similar cases.

Loose unification is a bit more forgiving in a few situations.

You shouldn’t need to care about these details when writing code, really, but if you’re curious, the appendix explains it all.

For an equation of the form X ≡A Y, where X and Y 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.

So if we’re trying to unify []struct{ Foo P } and []struct{ Foo string}, the top-level type structures (i.e. []struct{ Foo _ } and []struct{ Foo _ }) may loosely unify, but the element types (the types of Foo and Foo) must unify exactly.

For an equation of the form P ≡C C, where P is a type parameter and C its corresponding constraint, the unification rules are bit more complicated:

  • If C has a core type core(C) and P has a known type argument A, core(C) and A must unify loosely. If P does not have a known type argument and C contains exactly one type term T that is not an underlying (tilde) type, unification adds the mapping P ➞ T to the map.
  • If C does not have a core type and P has a known type argument A, A must have all methods of C, if any, and corresponding method types must unify exactly.

Man. I hope there’s not a quiz after this one.

So a (slightly simplified) refresher on core types:

  • Each non-interface type has a core type, which is the same as its underlying type.

    For example, given type Name string, Name’s underlying type and core type is string.

  • An interface has a core type if there is a single type which is the underlying type of all types in its typeset.

    For example, given an interface type of interface { int } has a core type of int, while interface { int | float64 } has no core type.

Now with this knowledge freshly in mind, we have three scenarios:

  • C has a core type, and P has a known type argument: OK if they unify loosely
  • C has a core type, and P does not have a known type argument and C contains one non-underlying type term: OK
  • C does not have a core type, and P has a known type argument: OK if method types unify exactly

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.

Man.

I hope I never have to care about this again!

Let’s talk about something more directly useful starting tomorrow: Operators!

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


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.


Precedence of type inference

Type inference … Type inference gives precedence to type information obtained from typed operands before considering untyped constants. Therefore, inference proceeds in two phases: The type equations are solved for the bound type parameters using type unification. If unification fails, type inference fails. Type unification comes up next in the spec, so we’ll learn exactly what that means soon. For each bound type parameter Pk for which no type argument has been inferred yet and for which one or more pairs (cj, Pk) with that same type parameter were collected, determine the constant kind of the constants cj in all those pairs the same way as for constant expressions.