Introduction

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.

Infer the Type

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">Pick an unannotated expression. The engine gives every unknown a fresh type variable, reads off a <b>constraint</b> from each use of a value, then <b>unifies</b> the constraints step by step until one concrete type remains — exactly how Hindley-Milner inference works.</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>Constraints</h4>
    <ul id="constraints"></ul>
  </div>
  <div class="col">
    <h4>Unification</h4>
    <ul id="steps"></ul>
  </div>
</div>
<div class="result" id="result">Inferred type appears here.</div>
<div class="btns">
  <button id="infer" type="button">Infer the type</button>
  <button id="reset" type="button" class="ghost">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; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// A tiny Hindley-Milner unifier. Each example is a list of CONSTRAINTS between
// type terms. A term is either a variable {v:'a'}, a base type {c:'Int'}, or a
// function {fn:[arg,ret]}. unify() solves them; the substitution gives the type.
// Plain unification is ~linear (Paterson-Wegman 1978); HM inference layered on top is decidable but DEXPTIME-complete in the worst case (Mairson 1990).
const V = n => ({ v:n });
const C = n => ({ c:n });
const FN = (a,r) => ({ fn:[a,r] });

// Each example: the expression text, the result type variable, and the constraints "read off" from how each value is used.
const EXAMPLES = {
  "fun x -> x + 1": {
    result: V('t0'),                 // type of the whole function
    // x is used with +, so x:Int; (+) returns Int; the function is x -> result
    constraints: [
      ["x is added with + , so", V('x'), C('Int')],
      ["+ returns", V('r'), C('Int')],
      ["the function is x -> r", V('t0'), FN(V('x'), V('r'))]
    ]
  },
  "fun b -> if b then 1 else 0": {
    result: V('t0'),
    constraints: [
      ["if-condition b must be", V('b'), C('Bool')],
      ["both branches are", V('r'), C('Int')],
      ["the function is b -> r", V('t0'), FN(V('b'), V('r'))]
    ]
  },
  "fun f -> fun x -> f x": {
    result: V('t0'),
    constraints: [
      ["f is applied to x, so f =", V('f'), FN(V('x'), V('y'))],
      ["inner fun is x -> y", V('inner'), FN(V('x'), V('y'))],
      ["outer fun is f -> inner", V('t0'), FN(V('f'), V('inner'))]
    ]
  },
  "if 1 then true else false": {       // a TYPE ERROR on purpose
    result: V('t0'),
    constraints: [
      ["if-condition 1 must be", C('Int'), C('Bool')],   // clash: Int vs Bool
      ["both branches are", V('t0'), C('Bool')]
    ]
  }
};

let current = "fun x -> x + 1";

// ---- unification core ----
function walk(t, s){ // follow substitution chain
  while(t.v && s[t.v]) t = s[t.v];
  return t;
}
function occurs(name, t, s){ // occurs-check
  t = walk(t, s);
  if(t.v) return t.v === name;
  if(t.fn) return occurs(name,t.fn[0],s) || occurs(name,t.fn[1],s);
  return false;
}
function unify(a, b, s){
  a = walk(a,s); b = walk(b,s);
  if(a.v){ if(a.v===b.v) return s; if(occurs(a.v,b,s)) return null;
    s[a.v]=b; return s; }
  if(b.v) return unify(b,a,s);
  if(a.c && b.c) return a.c===b.c ? s : null;     // base types must match
  if(a.fn && b.fn){ const s1=unify(a.fn[0],b.fn[0],s); if(!s1) return null;
    return unify(a.fn[1],b.fn[1],s1); }
  return null;
}
function show(t, s){
  t = walk(t,s);
  if(t.v) return t.v;
  if(t.c) return t.c;
  const [a,r] = t.fn;
  const left = walk(a,s).fn ? "("+show(a,s)+")" : show(a,s);
  return left + " -> " + show(r,s);
}
function termStr(t){ // pretty-print a raw constraint term (pre-solve)
  if(t.v) return t.v; if(t.c) return t.c;
  const a = t.fn[0].fn ? "("+termStr(t.fn[0])+")" : termStr(t.fn[0]);
  return a + " -> " + termStr(t.fn[1]);
}

// ---- rendering ----
function el(id){ return document.getElementById(id); }
function renderPicker(){
  const p = el('picker'); p.innerHTML='';
  Object.keys(EXAMPLES).forEach(name=>{
    const b=document.createElement('button'); b.textContent=name;
    if(name===current) b.className='active';
    b.addEventListener('click',()=>{ current=name; el('expr').textContent=name;
      el('constraints').innerHTML=''; el('steps').innerHTML='';
      el('result').textContent='Inferred type appears here.'; el('result').className='result';
      renderPicker(); });
    p.appendChild(b);
  });
}
function infer(){
  const ex = EXAMPLES[current];
  const cs = el('constraints'); cs.innerHTML='';
  const st = el('steps'); st.innerHTML='';
  // show constraints
  ex.constraints.forEach(([why,a,b])=>{
    const li=document.createElement('li');
    li.textContent = why + "  " + termStr(a) + " = " + termStr(b);
    cs.appendChild(li);
  });
  // unify in order
  let s = {}, ok = true;
  for(const [,a,b] of ex.constraints){
    const before = s;
    s = unify(a,b,Object.assign({},before));
    const li=document.createElement('li');
    if(!s){ li.textContent = fmt('✗ %termStr% = %termStr2%  — cannot unify', { termStr: termStr(a), termStr2: termStr(b) });
      li.className='fail'; st.appendChild(li); ok=false; break; }
    li.textContent = "✓ "+termStr(a)+" = "+termStr(b);
    st.appendChild(li);
  }
  const res = el('result');
  if(!ok){ res.textContent = "Type error: the constraints conflict — no type exists.";
    res.className='result bad';
    console.log('inference failed for:', current); return; }
  const ty = show(ex.result, s);
  res.textContent = current + "  :  " + ty;
  res.className='result';
  console.log('inferred', current, '=>', ty);
}
el('infer').addEventListener('click',infer);
el('reset').addEventListener('click',()=>{ el('constraints').innerHTML='';
  el('steps').innerHTML=''; el('result').textContent='Inferred type appears here.';
  el('result').className='result'; });
renderPicker();
Result
Console

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.

The Real Complexity

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.

Where It Matters

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.

Conclusion

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.

Share this article

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

Comments

Loading comments...

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