Automatic Type Deduction

Types Without Annotations

The type checker from the last lesson only works where a programmer wrote an annotation. But var x = 42; should still be understood as number — nobody wants to annotate every single local variable. Type inference figures out types the checker can then verify, using the same technique that gives ML, Haskell, and (in restricted form) Rust and TypeScript their "it just knows the types" feel: Hindley-Milner inference via unification.

Fresh Type Variables for the Unknown

Every time you encounter a binding whose type isn't yet known, invent a brand-new type variable — a placeholder that stands for "some type, to be determined":

let add = fun(a, b) { return a + b; } starts by assigning a: t0, b: t1, and the whole function t0 -> t1 -> t2 (using t2 for the inferred return type) — none of these are known yet, but they're now named, which means you can write equations about them.

Constraint Generation

Walking the expression generates constraints — equations between types that must hold for the program to type-check. a + b (assuming + here is monomorphic over number) generates:

a  = number
b  = number
t2 = number          -- the type of a + b, hence the return type

Each constraint is just a pair (type1, type2) that a unify call will later reconcile.

Unification: Solving the Constraints

Unification takes two types and a substitution map (tv name -> type built up so far) and either extends the substitution to make the two types equal, or fails with a type error:

Two concrete types unify only if they're identical (number unifies with number, not with string). A type variable unifies with anything by recording that substitution — t0 = number — which is how a's inferred type becomes concrete. Function types are compound ((param_types, ret)), so unifying two of them means unifying every corresponding piece.

The Occurs Check

Before binding a type variable t0 to some type T, you must confirm t0 doesn't appear inside T itself:

Without this check, a program like let f = fun(x) { return f(x); } (self-application without a base case) could produce an infinite type — t0 = t0 -> t1 — which would make apply_sub loop forever trying to fully resolve it. The occurs check turns that into a proper Type error: occurs check t0 in ... instead of a hang.

Working Through add

For fun add(a, b) { return a + b; }: generate a = number, b = number (from +), infer the return expression's type as number, so the function's type resolves to (number, number) -> number once you apply_sub across every type variable involved. No annotation was needed anywhere — the constraints pinned every variable down.

What to build

Implement fresh, occurs, apply_sub, and unify (including the function-type/arity case), then a small constraint generator for let bindings and single-expression function bodies that calls unify as it walks. Confirm let x = 42 infers number, a function using its parameters in a number-only context infers number -> number -> number, and a genuine mismatch (e.g., adding a number to a string) produces a Type error: cannot unify message rather than succeeding silently. (Full Hindley-Milner also generalizes inferred types into polymorphic schemes at let-bindings so a single function can be reused at multiple types — worth knowing exists, even though this exercise stays monomorphic.)