Introduction

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.

Try It

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.

<!-- Demo layout - controls, expression display, inferred type, inference steps -->
<div class="controls">
  <label for="preset">Expression:</label>
  <select id="preset">
    <option value="identity">λx. x  (identity)</option>
    <option value="const">λx. λy. x  (const)</option>
    <option value="apply">λf. λx. f x  (apply)</option>
    <option value="compose">λf. λg. λx. f (g x)  (compose)</option>
    <option value="twice">λf. λx. f (f x)  (twice)</option>
  </select>
  <button id="btn-infer" type="button">Infer Type</button>
  <button id="btn-reset" type="button" class="ghost">Reset</button>
</div>
<div class="expr-row">
  <span class="expr-label">Expression:</span>
  <code id="expr-display" class="expr-box"></code>
</div>
<div class="result-row" id="result-row" style="display:none">
  <span class="type-label">Principal type:</span>
  <code id="result-type" class="type-box"></code>
</div>
<div class="steps-header" id="steps-header" style="display:none">Inference steps</div>
<ol id="steps" class="steps"></ol>
<div class="status" id="status"></div>

/* Reset browser defaults and set base typography for the demo */
* { 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; }

const i18nFmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Algorithm W: Damas-Milner type inference for the simply-typed lambda calculus
// Generates type constraints and solves them by unification to find the principal type.

// Fresh type variable generator (alpha1, alpha2, ...).
let varCounter = 0;
function freshVar() { return 'α' + (++varCounter); }

// A substitution maps type variables to types.
// applySubst replaces type variables in a type according to a substitution.
function applySubst(subst, type) {
  if (typeof type === 'string') return subst[type] ? applySubst(subst, subst[type]) : type;
  if (type.tag === 'fun') return { tag: 'fun', from: applySubst(subst, type.from), to: applySubst(subst, type.to) };
  if (type.tag === 'list') return { tag: 'list', elem: applySubst(subst, type.elem) };
  return type;
}
function applySubstToSubst(s1, s2) {
  const out = {};
  for (const k in s2) out[k] = applySubst(s1, s2[k]);
  for (const k in s1) if (!(k in out)) out[k] = s1[k];
  return out;
}

// Collect all free type variables in a type.
function freeVars(type) {
  if (typeof type === 'string') return new Set([type]);
  if (type.tag === 'fun') { const s = freeVars(type.from); freeVars(type.to).forEach(v => s.add(v)); return s; }
  if (type.tag === 'list') return freeVars(type.elem);
  return new Set();
}

// Unification - find a substitution that makes two types equal.
// Implements Robinson's unification algorithm with occurs-check.
function unify(t1, t2, subst, steps) {
  t1 = applySubst(subst, t1); t2 = applySubst(subst, t2);
  const s1 = typeStr(t1), s2 = typeStr(t2);
  if (s1 === s2) { steps.push({ action: 'already equal', detail: `${s1} = ${s2}` }); return subst; }
  if (typeof t1 === 'string') {
    if (freeVars(t2).has(t1)) throw new Error('occurs check failed: ' + t1 + ' in ' + s2);
    steps.push({ action: 'bind', detail: `${t1} := ${s2}` });
    return applySubstToSubst({ [t1]: t2 }, subst);
  }
  if (typeof t2 === 'string') return unify(t2, t1, subst, steps);
  if (t1.tag === 'fun' && t2.tag === 'fun') {
    steps.push({ action: 'match →', detail: `(${s1}) ~ (${s2})` });
    subst = unify(t1.from, t2.from, subst, steps);
    return unify(applySubst(subst, t1.to), applySubst(subst, t2.to), subst, steps);
  }
  if (t1.tag === 'list' && t2.tag === 'list') {
    steps.push({ action: 'match list', detail: `List(${typeStr(t1.elem)}) ~ List(${typeStr(t2.elem)})` });
    return unify(t1.elem, t2.elem, subst, steps);
  }
  throw new Error('type mismatch: ' + s1 + ' vs ' + s2);
}

// Pretty-print a type as a human-readable string.
function typeStr(t) {
  if (typeof t === 'string') return t;
  if (t.tag === 'fun') {
    const from = t.from.tag === 'fun' ? '(' + typeStr(t.from) + ')' : typeStr(t.from);
    return from + ' → ' + typeStr(t.to);
  }
  if (t.tag === 'list') return '[' + typeStr(t.elem) + ']';
  return '?';
}

// Infer the type of an expression given an environment of type schemes.
// Returns the inferred type and the updated substitution.
function infer(expr, env, subst, steps) {
  if (expr.tag === 'var') {
    const t = env[expr.name];
    if (!t) throw new Error('unbound variable: ' + expr.name);
    // Instantiate a polymorphic type scheme with fresh type variables.
    const inst = instantiate(t);
    steps.push({ action: 'var', detail: `${expr.name} : ${typeStr(inst)}` });
    return { type: inst, subst };
  }
  if (expr.tag === 'lam') {
    const a = freshVar();
    const newEnv = Object.assign({}, env, { [expr.param]: { vars: [], body: a } });
    steps.push({ action: 'λ-intro', detail: `λ${expr.param}. assume ${expr.param}:${a}` });
    const { type: bt, subst: s2 } = infer(expr.body, newEnv, subst, steps);
    const lamType = { tag: 'fun', from: applySubst(s2, a), to: bt };
    return { type: lamType, subst: s2 };
  }
  if (expr.tag === 'app') {
    const { type: ft, subst: s1 } = infer(expr.fun, env, subst, steps);
    const { type: at, subst: s2 } = infer(expr.arg, env, s1, steps);
    const r = freshVar();
    steps.push({ action: 'app', detail: `${typeStr(applySubst(s2, ft))} applied to ${typeStr(at)}, result ${r}` });
    const s3 = unify(applySubst(s2, ft), { tag: 'fun', from: at, to: r }, s2, steps);
    return { type: applySubst(s3, r), subst: s3 };
  }
  throw new Error('unknown expression node');
}

// Generalize a type over variables not free in the environment (let-polymorphism).
function freeVarsEnv(env) {
  const s = new Set();
  for (const k in env) freeVars(env[k].body).forEach(v => env[k].vars.includes(v) || s.add(v));
  return s;
}
function generalize(type, env) {
  const envFree = freeVarsEnv(env);
  const free = [...freeVars(type)].filter(v => !envFree.has(v));
  return { vars: free, body: type };
}
function instantiate(scheme) {
  const mapping = {};
  scheme.vars.forEach(v => { mapping[v] = freshVar(); });
  return applySubst(mapping, scheme.body);
}

// Preset lambda expressions with their AST representations.
const PRESETS = {
  identity: {
    label: '\\u03bbx. x',
    expr: { tag: 'lam', param: 'x', body: { tag: 'var', name: 'x' } }
  },
  const: {
    label: '\\u03bbx. \\u03bby. x',
    expr: { tag: 'lam', param: 'x', body: { tag: 'lam', param: 'y', body: { tag: 'var', name: 'x' } } }
  },
  apply: {
    label: '\\u03bbf. \\u03bbx. f x',
    expr: {
      tag: 'lam', param: 'f', body: {
        tag: 'lam', param: 'x', body: {
          tag: 'app',
          fun: { tag: 'var', name: 'f' },
          arg: { tag: 'var', name: 'x' }
        }
      }
    }
  },
  compose: {
    label: '\\u03bbf. \\u03bbg. \\u03bbx. f (g x)',
    expr: {
      tag: 'lam', param: 'f', body: {
        tag: 'lam', param: 'g', body: {
          tag: 'lam', param: 'x', body: {
            tag: 'app',
            fun: { tag: 'var', name: 'f' },
            arg: {
              tag: 'app',
              fun: { tag: 'var', name: 'g' },
              arg: { tag: 'var', name: 'x' }
            }
          }
        }
      }
    }
  },
  twice: {
    label: '\\u03bbf. \\u03bbx. f (f x)',
    expr: {
      tag: 'lam', param: 'f', body: {
        tag: 'lam', param: 'x', body: {
          tag: 'app',
          fun: { tag: 'var', name: 'f' },
          arg: {
            tag: 'app',
            fun: { tag: 'var', name: 'f' },
            arg: { tag: 'var', name: 'x' }
          }
        }
      }
    }
  }
};

function runInference() {
  varCounter = 0;
  const key = document.getElementById('preset').value;
  const preset = PRESETS[key];
  document.getElementById('expr-display').textContent = preset.label;
  document.getElementById('result-row').style.display = 'none';
  document.getElementById('steps-header').style.display = 'none';
  const stepsList = document.getElementById('steps');
  stepsList.innerHTML = '';
  const statusEl = document.getElementById('status');
  statusEl.textContent = '';
  statusEl.className = 'status';
  try {
    const steps = [];
    const { type, subst } = infer(preset.expr, {}, {}, steps);
    const finalType = applySubst(subst, type);
    // Generalize the final type to a polymorphic scheme.
    const scheme = generalize(finalType, {});
    let typeDisplay = typeStr(finalType);
    if (scheme.vars.length > 0) typeDisplay = '∀' + scheme.vars.join(' ') + '. ' + typeDisplay;
    document.getElementById('result-type').textContent = typeDisplay;
    document.getElementById('result-row').style.display = 'flex';
    document.getElementById('steps-header').style.display = 'block';
    steps.forEach(s => {
      const li = document.createElement('li');
      li.innerHTML = '<span class="action">' + s.action + '</span> <span class="unify">' + s.detail + '</span>';
      stepsList.appendChild(li);
    });
    statusEl.textContent = i18nFmt('Done in %n% step(s).', { n: steps.length });
    statusEl.className = 'status ok';
  } catch (e) {
    statusEl.textContent = 'Type error: ' + e.message;
    statusEl.className = 'status err';
  }
}

function resetAll() {
  varCounter = 0;
  document.getElementById('expr-display').textContent = '';
  document.getElementById('result-row').style.display = 'none';
  document.getElementById('steps-header').style.display = 'none';
  document.getElementById('steps').innerHTML = '';
  const statusEl = document.getElementById('status');
  statusEl.textContent = '';
  statusEl.className = 'status';
}

document.getElementById('btn-infer').addEventListener('click', runInference);
document.getElementById('btn-reset').addEventListener('click', resetAll);

// Show the identity function expression on load.
document.getElementById('preset').value = 'identity';
document.getElementById('expr-display').textContent = PRESETS['identity'].label;
Result
Console

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.

The Real Complexity

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⋅α(n))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.

Where It Matters

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.

Conclusion

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.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/hindley-milner/Content licensed under CC BY-NC 4.0.