On this page

How Hindley–Milner Inference "Reads" Your Code in OCaml

Published on July 21, 2026

Enrico Hochkoeppler Profile

By Enrico Hochkoeppler

Web Developer & TutoriaLibre Founder

Every OCaml expression has a precise, correct type without ever needing a single explicit type annotation. This isn't guesswork, and it isn't a simple set of pattern-matching rules bolted onto the compiler — it's Hindley–Milner type inference, an algorithm that reconstructs the exact type of every expression in a program from nothing but how that expression is used. This lesson builds an intuitive, working mental model of how it operates, without the formal proofs a language-theory course would require.

The Core Idea: Placeholders That Get Filled In​

Think of type inference as a two-pass process happening as the compiler reads through code. On the first pass, anything whose type isn't yet known gets a placeholder — a fresh, unconstrained type variable, conventionally written 'a, 'b, 'c, and so on. On the second pass, as the compiler sees how each piece of the program is actually used, it fills in or narrows those placeholders, based on the rules already built into the language: + requires both its arguments and its result to be int, if requires both branches to match, and so on.

Consider a bare function skeleton before anything about its body is examined:


let f x = ...

At this point, x's type is completely unknown — it could be anything — so the compiler assigns it a placeholder, say 'a. Whatever f's body eventually does with x is what determines what 'a actually has to be.

Unification: Forcing Two Types to Agree​

The mechanism that fills in placeholders is called unification: given two types, possibly containing placeholders, the compiler tries to make them equal, either by directly matching them if they already agree, or by pinning down a placeholder to whatever the other type demands. If no assignment of placeholders can make the two types equal, unification fails, and that failure is exactly what surfaces as a type error.

Walking through a slightly more concrete function shows this in action:


let add x y = x + y

x and y both start out as fresh placeholders, say 'a and 'b. The moment the compiler examines x + y, it knows (+) : int -> int -> int, so it unifies 'a with int (forcing x to be int) and unifies 'b with int (forcing y to be int) as well. The result of x + y is therefore int, which becomes the return type of add. Every placeholder introduced at the start has now been resolved by the time the whole function has been read, producing the final, fully concrete type:


# add;;

- : int -> int -> int = <fun>

Nothing about this required guessing — every placeholder was pinned down by a concrete rule already known about some other part of the expression, and the type shown is simply what's left once every one of those constraints has been applied.

When Nothing Constrains a Placeholder: True Polymorphism​

Not every function pins down all of its placeholders. Consider the simplest possible function:


let id x = x

x starts as a placeholder 'a, and the body of the function — just x on its own — never does anything to x that would force 'a to be any particular concrete type. No arithmetic, no comparison, no field access, nothing. Since nothing in the function ever constrains 'a, it stays exactly what it started as: a placeholder, standing for "any type at all." This is what parametric polymorphism actually is under the hood — a type variable that survives all the way through inference unconstrained, rather than a special separate mechanism bolted on afterward.


# id;;

- : 'a -> 'a = <fun>

# id 5;;

- : int = 5

# id "hello";;

- : string = "hello"

id can be applied to an int and, separately, to a string, because its type never demanded one specific type in the first place — the placeholder simply gets filled in with whatever concrete type shows up at each individual call site.

Why let Generalizes, But a Function Parameter Doesn't​

Here's a detail that trips up almost everyone the first time it's noticed: the polymorphism seen with id above comes specifically from how let works, not from something every unconstrained placeholder automatically gets. A placeholder that survives inference for a let-bound name gets generalized — turned into a genuinely reusable, universally quantified type variable, usable at a different concrete type on each separate call. A placeholder belonging to a plain function parameter, used only within that one function body, is not generalized the same way; it's resolved once, consistently, for that single invocation of the function.

This is why the following does not type-check, even though intuitively x is "just being passed along" in both places:


let apply_twice f x y = (f x, f y)


# apply_twice id 5 "hello";;

Error: This expression has type string

       but an expression was expected of type int

Inside apply_twice, f is an ordinary function parameter, not a let-bound name being generalized fresh at each call — so once f x fixes f's type as int -> int (because x is used as 5), that same, now-concrete type of f has to apply to y too, and "hello" doesn't fit. id itself stayed polymorphic because it's let-bound at the top level and re-generalized every time it's referenced; f inside apply_twice is a parameter, resolved once per call to apply_twice, not once per use inside its body.

A Practical Gotcha: The Value Restriction​

A related, genuinely practical surprise shows up with mutable state:


# let r = ref [];;

val r : '_weak1 list ref = {contents = []}

That '_weak1 isn't an ordinary polymorphic type variable — it's a weak type variable, and it exists because generalizing this particular placeholder would be unsound: if r's empty list could be treated as int list ref in one place and string list ref in another, code could insert an int into it in one place and read out a string from that same mutable cell somewhere else, silently breaking the type system's most basic promise. OCaml's rule, called the value restriction, only fully generalizes a let-bound expression when that expression is a syntactic value — think a literal, a variable, or a fully applied constructor — rather than the general result of a computation. ref [] is a function call (to the function ref), so it doesn't qualify, and its placeholder stays weak — resolved to one single concrete type, permanently, the first time it's actually used at some type. Recognizing this pattern makes an otherwise-baffling type error message make immediate sense the first time it's encountered in real code.

Principal Types: OCaml Never Overcommits​

A property worth naming directly: whenever inference succeeds, the type it produces is the principal type — the single most general type consistent with how the expression is actually used. OCaml never picks a needlessly specific type when a more general one would have worked just as well; id's type is 'a -> 'a, not, say, int -> int just because it happened to be tried on an integer first. This is also why type inference in OCaml is complete for the fragment of the language it covers: if a program is genuinely well-typed, inference is guaranteed to find that fact and produce the most general type witnessing it, not merely one type among several that might have worked.

Reading Errors Through This Lens​

This model directly explains the shape of a common family of type errors. A message like "this expression has type X but an expression was expected of type Y" is unification failing to make two types agree — one side's type was already pinned down by an earlier rule, and the other side's value simply didn't match it. Understanding inference as walking through code left to right, filling in placeholders as it goes, is exactly what makes it possible to predict, before even running the compiler, which side of a mismatch is the "expected" one and which side is the unexpected value that broke an otherwise-consistent picture.

Key Takeaways​

Found this helpful? Share the knowledge...

... or support this project to keep it alive!

Buy Me a Coffee

Previous

Type Inference & Higher-Order Functions

Next

Parametric Polymorphism