Type Inference

In languages like Haskell, OCaml, Rust and TypeScript, you can write a function without ever saying what type it takes or returns — and the compiler will still tell you, with total confidence, that you applied it to the wrong thing. How can it know a type you never wrote down?

The answer is type inference: the compiler treats every unknown type as a placeholder, watches how you use each value, and from that usage deduces the only types that could make the program consistent. Pass a value to + and it must be a number; return it from an if, and both branches must agree.

The classic engine for this is Hindley-Milner (Roger Hindley, 1969; rediscovered by Robin Milner in 1978). It is famous for a near-magical property: with no annotations at all, it finds the most general type of any expression — or proves no type exists. The trick has a name, and it is wonderfully simple: unification.

Below is a tiny Hindley-Milner engine. Pick an unannotated expression — like fun x -> x + 1 — and the engine will assign a fresh type variable to every unknown, generate constraints from how each value is used, and then unify them step by step until a concrete type drops out.

<p class="hint">{{hint}}</p>
<div class="picker" id="picker"></div>
<div class="expr" id="expr">fun x -&gt; x + 1</div>
<div class="panel">
  <div class="col">
    <h4>{{h_constraints}}</h4>
    <ul id="constraints"></ul>
  </div>
  <div class="col">
    <h4>{{h_unification}}</h4>
    <ul id="steps"></ul>
  </div>
</div>
<div class="result" id="result">{{initial_result}}</div>
<div class="btns">
  <button id="infer" type="button">{{btn_infer}}</button>
  <button id="reset" type="button" class="ghost">{{btn_reset}}</button>
</div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .9rem; color: #444; margin: 0 0 .7rem; line-height: 1.45; }
.picker { display: flex; gap: .4rem; flex-wrap: wrap; margin-bottom: .6rem; }
.picker button { font: 600 13px ui-monospace, monospace; padding: .35rem .6rem;
  border: 1px solid #cdd9e3; background: #fff; color: #1d3557; border-radius: 7px; cursor: pointer; }
.picker button.active { background: #1d3557; color: #fff; border-color: #1d3557; }
.expr { font: 700 18px ui-monospace, monospace; background: #f3f6f9; border: 1px solid #cdd9e3;
  border-radius: 8px; padding: .6rem .8rem; color: #1d3557; margin-bottom: .6rem; }
.panel { display: grid; grid-template-columns: 1fr 1fr; gap: .8rem; }
@media (max-width: 480px) { .panel { grid-template-columns: 1fr; } }
.col h4 { margin: 0 0 .35rem; font-size: .8rem; text-transform: uppercase; letter-spacing: .05em; color: #5a7088; }
.col ul { list-style: none; margin: 0; padding: 0; }
.col li { font: 600 13px ui-monospace, monospace; padding: .3rem .5rem; margin-bottom: .3rem;
  background: #fff; border: 1px solid #e2e8ef; border-radius: 6px; color: #1d3557; }
.col li.fail { background: #fdecee; border-color: #f0b3ba; color: #c92f3c; }
.result { font: 700 16px ui-monospace, monospace; margin: .7rem 0; min-height: 1.4em; padding: .55rem .8rem;
  border-radius: 8px; background: #eef7f0; color: #0a7d33; border: 1px solid #bfe3c9; }
.result.bad { background: #fdecee; color: #c92f3c; border-color: #f0b3ba; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; }
button { font: 600 14px system-ui, sans-serif; padding: .45rem .9rem; border: 1px solid #1d3557;
  background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }

// Code not found

Notice that you wrote no types, yet a complete type appears. Watch the constraints: each use of a value (+, if, function application) pins down one more unknown. When two constraints clash — say a value is used both as a number and as a boolean — unification fails, and that is exactly the type error your compiler reports.

How hard is it to infer types? The answer depends sharply on how expressive the type system is.

• Plain unification is easy. Solving a set of equations between type terms takes essentially linear time (Paterson-Wegman, 1978). This is the core engine in the demo.
• Hindley-Milner is decidable. Inference always terminates and returns the most general type or a definite error. In practice it is fast — but in the worst case the type can blow up: HM type inference is DEXPTIME-complete (Mairson; Kfoury-Tiuryn-Urzyczyn, 1990), because nested let definitions can make types double in size at each level.
• System F inference is undecidable. Add first-class polymorphism (rank-N types) and the question "does this unannotated term have a type?" becomes undecidable — proven by J. B. Wells in 1994. No algorithm can always answer it.
• That is why annotations exist. Modern languages keep full inference for the easy HM core and ask you to annotate exactly where they cross into the undecidable territory.

So type inference lives on a knife's edge: easy and complete for the HM fragment, and provably impossible the moment the type system gets too powerful — a concrete cousin of the halting problem and the limits explored in P vs NP.

The unification engine you just watched is one of the most quietly load-bearing algorithms in all of software:

• Compilers: Haskell, OCaml, Rust, Swift, Scala and Elm all run Hindley-Milner-style inference so you can write less and still get full static checking.
• TypeScript and gradual typing: inference fills the gaps where you didn't annotate, turning loose JavaScript into checked code without forcing types everywhere.
• IDE tooling: autocomplete, "go to type", inline hints and safe refactors all ask the inference engine "what type is this, really?".
• Theorem provers and proof assistants: Coq, Agda and Lean lean on the same unification core to elaborate the types you left implicit.

Learn how inference unifies constraints and you've met the same machinery behind logic programming and the constraint reasoning in SAT — solving for unknowns until only one consistent answer remains.

Type inference hides a beautiful idea: you never have to tell the compiler the types, because the way you use each value already determines them. Generate one constraint per use, unify them all, and the most general type falls out — or a clash reveals your bug.

But the same elegance has a hard ceiling. Push the type system far enough — to full first-class polymorphism — and deciding whether a term even has a type becomes undecidable. The annotations you occasionally still write are not a failure of the compiler; they are the precise point where it would otherwise be asked to solve the unsolvable.