Type Inference — Hindley-Milner

Type inference frees programmers from writing explicit type annotations while still providing full type safety. The compiler figures out the types automatically.

The Idea

var x = 42;              // inferred: number
var y = "hello";         // inferred: string
var z = x + 1;           // inferred: number (because x is number and + returns number)

fun double(n) {          // inferred: (number) -> number
    return n * 2;
}

No annotations needed — the compiler deduces everything from how values are used.

The Hindley-Milner Algorithm

Hindley-Milner (HM) type inference, developed by Hindley (1969) and Milner (1978), is the gold standard for type inference. It has two phases:

Phase 1: Constraint Generation

Walk the AST and generate type constraints — equations between types:

var x = 42;        → type(x) = number
var y = x + 1;     → type(+) = (number, number) -> number
                     type(x) = number, type(1) = number
                     type(y) = number
fun f(a) { return a + 1; }
                   → type(a) = T1 (fresh type variable)
                     T1 = number (because a is used with +)
                     type(f) = (number) -> number

Phase 2: Unification

Solve the constraints by unification — substituting type variables until all constraints are satisfied:

unify(T1, number):
    T1 := number       // substitute T1 with number everywhere

unify(T2, T3 -> T4):
    T2 := T3 -> T4     // T2 is a function type

Unification fails if incompatible types are unified: unify(number, string) produces a type error.

The Union-Find Data Structure

Efficient unification uses a union-find (disjoint set) data structure. Each type variable points to its representative. Unification merges two sets. Finding a variable's type follows the chain to the root.

Occurs Check

We must prevent infinite types. If T1 = List<T1>, the type is infinitely recursive. The occurs check detects this: before unifying T = ..., check that T does not appear in the right-hand side.

How Languages Use HM

• ML, OCaml, Haskell: full HM inference — rarely need annotations
• Rust: local inference within functions, but function signatures require annotations
• TypeScript: bi-directional type inference (contextual typing)
• Python (mypy): inference within functions, annotations at boundaries

Your Task

Implement type inference using constraint generation and unification. The compiler should infer types for variables and function parameters that lack explicit annotations.