Hindley-Milner Type Inference

Every time you write map f xs in Haskell or List.map f xs in OCaml and the compiler accepts it without a single type annotation, you are watching Hindley-Milner type inference at work. The compiler deduces that f must be a function, that xs must be a list whose elements match f's input, and that the result is a list of whatever f produces — all from the expression alone, with no help from you.

The algorithm was discovered independently by J. Roger Hindley (1969) and Robin Milner (1978), and later refined by Luis Damas (1982) into the form used today, often called Damas-Milner or Algorithm W. It is one of the most influential results in programming-language theory: a solved problem with a clean, complete answer.

The core idea is unification: when the algorithm sees f x, it generates the constraint that the type of f must be of the form $\alpha \to \beta$ for some type variables $\alpha$ and $\beta$, that the type of x must unify with $\alpha$, and that the whole expression has type $\beta$. Solving all such constraints simultaneously yields the principal type — the most general type that the expression can have. Any other valid type is just a specialization of it.

What makes this remarkable is the guarantee: if a principal type exists, Algorithm W finds it in nearly linear time. If no type exists, the algorithm reports a type error. There is no ambiguity and no need to guess.

Select a preset expression or type your own, then watch Algorithm W infer its principal type step by step. Each step generates a type constraint, and unification solves them all together.

<!-- {{c_html_structure}} -->
<div class="controls">
  <label for="preset">{{label_preset}}</label>
  <select id="preset">
    <option value="identity">{{opt_identity}}</option>
    <option value="const">{{opt_const}}</option>
    <option value="apply">{{opt_apply}}</option>
    <option value="compose">{{opt_compose}}</option>
    <option value="twice">{{opt_twice}}</option>
  </select>
  <button id="btn-infer" type="button">{{btn_infer}}</button>
  <button id="btn-reset" type="button" class="ghost">{{btn_reset}}</button>
</div>
<div class="expr-row">
  <span class="expr-label">{{label_expr}}</span>
  <code id="expr-display" class="expr-box"></code>
</div>
<div class="result-row" id="result-row" style="display:none">
  <span class="type-label">{{label_type}}</span>
  <code id="result-type" class="type-box"></code>
</div>
<div class="steps-header" id="steps-header" style="display:none">{{label_steps}}</div>
<ol id="steps" class="steps"></ol>
<div class="status" id="status"></div>

/* {{c_css_reset}} */
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; padding: .5rem; }
.controls { display: flex; flex-wrap: wrap; gap: .5rem; align-items: center; margin-bottom: .7rem; }
label { font-size: .85rem; color: #555; }
select { font-size: .9rem; padding: .35rem .5rem; border: 1px solid #bbb; border-radius: 6px; background: #fafafa; }
button { font: 600 14px system-ui; padding: .4rem .85rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 7px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
.expr-row, .result-row { display: flex; align-items: baseline; gap: .6rem; margin: .35rem 0; flex-wrap: wrap; }
.expr-label, .type-label { font-size: .82rem; color: #666; min-width: 4.5rem; }
.expr-box, .type-box { font: 1rem ui-monospace, monospace; background: #f0f4f8; border: 1px solid #d0d9e3;
                       border-radius: 6px; padding: .2rem .6rem; color: #1d3557; }
.type-box { background: #e6f4ea; border-color: #9ecfb0; color: #0a5c2d; font-weight: 600; }
.steps-header { font-size: .8rem; font-weight: 600; color: #666; margin: .7rem 0 .2rem; text-transform: uppercase; letter-spacing: .04em; }
.steps { margin: 0; padding-left: 1.4rem; }
.steps li { font-size: .82rem; font-family: ui-monospace, monospace; margin: .15rem 0; color: #333; line-height: 1.5; }
.steps li .action { color: #1d3557; font-weight: 600; }
.steps li .unify { color: #b56800; }
.steps li .result { color: #0a5c2d; font-weight: 600; }
.status { font-size: .95rem; font-weight: 600; margin-top: .5rem; min-height: 1.3em; }
.status.ok { color: #0a7d33; }
.status.err { color: #c92f3c; }

// Code not found

Notice how the same function can be used at different types in different contexts — this is parametric polymorphism. The inferred type uses variables like $\alpha$ and $\beta$ to stand for any concrete type, and a single inference run produces the most general answer, not just one instance of it.

Hindley-Milner type inference is a solved problem — but its complexity is subtler than it first appears.

• Algorithm W is nearly linear for programs that arise in practice. The bottleneck is the union-find data structure used to track which type variables have been merged, and with path compression it runs in nearly $O(n \cdot \alpha(n))$ time, where $\alpha$ is the inverse Ackermann function — essentially constant.
• The worst case is exponential. Through deeply nested let bindings, you can force the inferred types to grow exponentially in the nesting depth. This is not a bug in the algorithm; it reflects a genuine property of the Hindley-Milner type language. In practice, compilers impose a depth limit and warn instead of hanging.
• The full decision problem is DEXPTIME-complete. Determining whether an ML-style expression is typeable (with full let-polymorphism) is hard in theory, though this bound is never hit in real codebases.
• Extensions can break decidability. Adding first-class polymorphism (rank-2 or higher types) makes type inference undecidable; languages like Haskell that support it require explicit annotations at the polymorphic site.

So the pleasant story is: Algorithm W solves a problem that, in its worst theoretical form, is exponentially hard — and it does so in nearly linear time for every program any real programmer writes. The gap between theory and practice here is unusually large, and unusually fortunate.

Hindley-Milner is not a curiosity — it is the engine powering the type systems of the most type-safe languages in use today:

• Haskell and OCaml use Damas-Milner as their core type system. Every function you write is inferred to its most general type, enabling fearless refactoring and catching entire classes of bugs at compile time.
• F# and Elm bring the same inference to .NET and the web, making typed functional programming accessible to mainstream audiences.
• Rust uses a variant of Hindley-Milner extended with traits and lifetimes. The borrow checker itself is a constraint-solving system in the same spirit.
• TypeScript uses bidirectional type inference inspired by Hindley-Milner, though it relaxes the guarantee of always finding the principal type in exchange for ergonomics.
• Type-driven development: because the inferred type of a partially written function describes exactly what is missing, types become a live specification — the compiler tells you what to fill in.

Beyond languages, the unification machinery at the core of Hindley-Milner appears in SAT solvers, logic programming (Prolog's resolution is unification), and constraint propagation systems. Understanding one is a key to understanding all.

Hindley-Milner type inference occupies a rare position in computer science: it is a fully solved problem with an algorithm that is both complete and efficient in practice. Algorithm W always finds the most general type of any typeable expression — and it does so in nearly linear time, using nothing more than constraint generation and unification.

The next time a compiler catches a bug you haven't thought of yet, or infers the type of a function you just wrote without asking for a single annotation, that is Hindley-Milner at work. It is one of the clearest examples of how a deep theoretical result — the existence of a principal type — translates directly into a better, safer programming experience.