The type checker lends a pencil

I gave the type checker an unnamed type. It sharpened a pencil.

A promise with an unknown in it

An unnamed type is not necessarily a missing annotation. Sometimes it is a perfectly reasonable question waiting for the rest of the program.

identity(value: a) -> a {
  value
}

main() {
  assert identity(12) == 12
  assert identity(True) == True
}

The a says the argument and result have the same type. It does not say every call to identity must accept the same thing forever.

Fresh paper for every call

first call:   identity : a1 -> a1
              a1 = Int

second call:  identity : a2 -> a2
              a2 = Bool

The numbers stand for separate inference variables, not two spellings of one shared unknown.

For each use of a polymorphic function, inference needs fresh unknowns. In the first call, an unknown meets Int. In the second, a different unknown meets Bool. Reusing one mutable inference variable for both calls would make the compiler object to a promise the program never made.

Unification is the part that reconciles these requirements. Two compatible types contribute information to the same answer. A function returning Int cannot quietly become a function returning String because the caller has arranged a welcoming vase of flowers.

When the pencil must stop

There are awkward cases. If solving a constraint would require a type variable to contain itself, the checker needs to notice. Otherwise an apparently small question grows a type with no end, and the pencil disappears into the wallpaper.

The implementation language helps here too. In Gleam, explicit constructors can distinguish a function type, a named type and an inference variable. The solver can inspect those shapes rather than guessing from printed names.

Readable type errors are the second half of this work. The user wants the conflicting requirements explained in terms of their program, not a transcript of the solver’s private bookkeeping.

A useful type checker can be strict without being mysterious. Most evenings, that is the larger ambition.

— Peregrine Finch