Type Inference: Hindley-Milner and Bidirectional

Key Insights

Hindley-Milner provides complete type inference through unification, but breaks down with advanced features like higher-rank polymorphism and subtyping
Bidirectional type checking splits inference into synthesis (bottom-up) and checking (top-down) modes, enabling better error messages and composability with complex type systems
Modern languages like TypeScript and Rust use hybrid approaches, combining local inference with strategic annotation requirements to balance expressiveness and usability

Introduction to Type Inference

Type inference lets compilers deduce types without explicit annotations. Instead of writing int x = 5, you write let x = 5 and the compiler figures out the rest. This isn’t just syntactic sugar—it fundamentally changes how we interact with type systems.

The story begins with ML in the 1970s, where Robin Milner developed a type system that could infer types for an entire program without a single annotation. This was revolutionary. Today, type inference powers everything from Haskell’s sophisticated type system to TypeScript’s gradual typing to Rust’s ownership inference.

But not all inference is created equal. Understanding the tradeoffs between different approaches helps you write better code and understand why your compiler sometimes demands annotations.

The Hindley-Milner Type System

Hindley-Milner (HM) is the gold standard for complete type inference. Given any well-typed expression, HM finds its most general type—the principal type—without any annotations.

The core insight is that types can contain variables. When you write fun x -> x, HM infers the type 'a -> 'a (a function from any type to the same type). This polymorphism emerges naturally from the inference process.

(* OCaml infers all types automatically *)
let id x = x                          (* val id : 'a -> 'a *)
let compose f g x = f (g x)           (* val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b *)
let apply_twice f x = f (f x)         (* val apply_twice : ('a -> 'a) -> 'a -> 'a *)

(* Even complex expressions need no annotations *)
let mystery f g h x = f (g x) (h x)   
(* val mystery : ('a -> 'b -> 'c) -> ('d -> 'a) -> ('d -> 'b) -> 'd -> 'c *)

Algorithm W, the standard HM inference algorithm, works by generating type equations as it traverses the syntax tree, then solving them through unification. The algorithm is both sound (inferred types are correct) and complete (if a type exists, it will be found).

Unification: The Engine of HM Inference

Unification is the process of finding a substitution that makes two types equal. When you apply a function of type 'a -> 'b to an argument of type int, unification determines that 'a = int.

Here’s a minimal unification implementation:

from dataclasses import dataclass
from typing import Dict, Optional

@dataclass
class TVar:
    name: str

@dataclass  
class TCon:
    name: str

@dataclass
class TApp:
    func: 'Type'
    arg: 'Type'

Type = TVar | TCon | TApp
Substitution = Dict[str, Type]

def apply_subst(subst: Substitution, ty: Type) -> Type:
    match ty:
        case TVar(name) if name in subst:
            return apply_subst(subst, subst[name])
        case TVar(_) | TCon(_):
            return ty
        case TApp(func, arg):
            return TApp(apply_subst(subst, func), apply_subst(subst, arg))

def occurs_check(var: str, ty: Type) -> bool:
    """Prevent infinite types like 'a = List['a]"""
    match ty:
        case TVar(name):
            return var == name
        case TCon(_):
            return False
        case TApp(func, arg):
            return occurs_check(var, func) or occurs_check(var, arg)

def unify(t1: Type, t2: Type, subst: Substitution) -> Optional[Substitution]:
    t1, t2 = apply_subst(subst, t1), apply_subst(subst, t2)
    
    match (t1, t2):
        case (TVar(n1), TVar(n2)) if n1 == n2:
            return subst
        case (TVar(name), ty) | (ty, TVar(name)):
            if occurs_check(name, ty):
                return None  # Infinite type error
            return {**subst, name: ty}
        case (TCon(n1), TCon(n2)) if n1 == n2:
            return subst
        case (TApp(f1, a1), TApp(f2, a2)):
            subst = unify(f1, f2, subst)
            return unify(a1, a2, subst) if subst else None
        case _:
            return None  # Type mismatch

The occurs check is crucial—it prevents infinite types. Without it, unifying 'a with List['a] would create 'a = List[List[List[...]]].

Limitations of Hindley-Milner

HM’s elegance comes with constraints. Several features break complete inference:

Higher-rank polymorphism requires annotations because inference becomes undecidable:

{-# LANGUAGE RankNTypes #-}

-- This REQUIRES an annotation - HM cannot infer it
applyToBoth :: (forall a. a -> a) -> (Int, Bool) -> (Int, Bool)
applyToBoth f (x, y) = (f x, f y)

-- Without the annotation, GHC would infer a less general type
-- that doesn't allow 'f' to be applied to both Int and Bool

Subtyping creates ambiguity. If Cat <: Animal, should [Cat] have type List[Cat] or List[Animal]? Both are valid, so there’s no principal type.

Overloading (type classes, traits) introduces similar ambiguity:

-- What's the type of this expression?
show (read "42")

-- It could be String for any readable/showable type
-- Haskell requires disambiguation through context or annotation

These limitations pushed language designers toward more sophisticated approaches.

Bidirectional Type Checking

Bidirectional type checking splits inference into two modes:

Synthesis (↑): Given an expression, compute its type
Checking (↓): Given an expression and an expected type, verify they match

Information flows in both directions through the AST. This simple distinction enables clean handling of features that break HM.

Synthesis rules (computing types):
  x : T ∈ Γ
  ─────────── Var↑
  Γ ⊢ x ↑ T

  Γ ⊢ e ↑ A → B    Γ ⊢ arg ↓ A
  ───────────────────────────── App↑
  Γ ⊢ e arg ↑ B

Checking rules (verifying types):
  Γ, x : A ⊢ body ↓ B
  ─────────────────────── Lam↓
  Γ ⊢ λx. body ↓ A → B

  Γ ⊢ e ↑ A    A = B
  ─────────────────── Switch
  Γ ⊢ e ↓ B

The key insight: lambdas are checked against expected types, while applications synthesize types. This matches how programmers think—you know what type a function should have when you write it, but you discover what type an expression has when you use it.

TypeScript demonstrates this practically:

// Synthesis: TS infers the parameter type from usage
const numbers = [1, 2, 3];
const doubled = numbers.map(x => x * 2);  // x inferred as number

// Checking: Expected type flows into the lambda
const handler: (event: MouseEvent) => void = (e) => {
    console.log(e.clientX);  // e is MouseEvent, no annotation needed
};

// Without context, annotation required
const mystery = (e) => e.clientX;  // Error: parameter 'e' implicitly has 'any' type

Implementing a Bidirectional Type Checker

Here’s a complete bidirectional type checker for a minimal language:

use std::collections::HashMap;

#[derive(Clone, Debug, PartialEq)]
enum Type {
    Int,
    Bool,
    Func(Box<Type>, Box<Type>),
}

#[derive(Clone)]
enum Expr {
    Var(String),
    Int(i64),
    Bool(bool),
    Lam(String, Box<Expr>),           // λx. body
    Ann(Box<Expr>, Type),              // (e : T)
    App(Box<Expr>, Box<Expr>),         // e1 e2
    If(Box<Expr>, Box<Expr>, Box<Expr>),
}

type Context = HashMap<String, Type>;

#[derive(Debug)]
struct TypeError(String);

// Synthesis: Γ ⊢ e ↑ T
fn synthesize(ctx: &Context, expr: &Expr) -> Result<Type, TypeError> {
    match expr {
        Expr::Var(name) => ctx
            .get(name)
            .cloned()
            .ok_or_else(|| TypeError(format!("Unbound variable: {}", name))),

        Expr::Int(_) => Ok(Type::Int),
        Expr::Bool(_) => Ok(Type::Bool),

        // Annotations allow synthesis of lambdas
        Expr::Ann(e, ty) => {
            check(ctx, e, ty)?;
            Ok(ty.clone())
        }

        Expr::App(func, arg) => {
            let func_ty = synthesize(ctx, func)?;
            match func_ty {
                Type::Func(param_ty, ret_ty) => {
                    check(ctx, arg, &param_ty)?;
                    Ok(*ret_ty)
                }
                _ => Err(TypeError("Expected function type".into())),
            }
        }

        Expr::Lam(_, _) => Err(TypeError(
            "Cannot synthesize lambda type; add annotation".into(),
        )),

        Expr::If(cond, then_br, else_br) => {
            check(ctx, cond, &Type::Bool)?;
            let ty = synthesize(ctx, then_br)?;
            check(ctx, else_br, &ty)?;
            Ok(ty)
        }
    }
}

// Checking: Γ ⊢ e ↓ T
fn check(ctx: &Context, expr: &Expr, expected: &Type) -> Result<(), TypeError> {
    match (expr, expected) {
        // Lambdas check against function types
        (Expr::Lam(param, body), Type::Func(param_ty, ret_ty)) => {
            let mut new_ctx = ctx.clone();
            new_ctx.insert(param.clone(), (**param_ty).clone());
            check(&new_ctx, body, ret_ty)
        }

        // Fall back to synthesis and compare
        _ => {
            let inferred = synthesize(ctx, expr)?;
            if &inferred == expected {
                Ok(())
            } else {
                Err(TypeError(format!(
                    "Expected {:?}, got {:?}",
                    expected, inferred
                )))
            }
        }
    }
}

This 80-line implementation handles variables, literals, lambdas, applications, annotations, and conditionals. The bidirectional structure keeps the code clean and extensible.

Practical Tradeoffs and Modern Approaches

Real languages blend multiple strategies:

TypeScript uses bidirectional checking with contextual typing. Type information flows from variable declarations, return types, and callback signatures into expressions. This is why array.map(x => x.foo) works—the array’s element type flows into the callback parameter.

Rust employs local type inference with mandatory function signatures. Within a function body, inference is powerful (including lifetime inference), but API boundaries require explicit types. This balances internal convenience with external clarity.

Scala 3 introduced a sophisticated bidirectional system that handles union types, intersection types, and dependent functions. It demonstrates how far bidirectional checking can scale.

The trend is clear: pure HM is too limited for modern type systems, but complete inference isn’t the goal anyway. Strategic annotation requirements improve code readability and error messages. The art is finding the right balance.

When designing a language or choosing one for a project, consider:

Inference scope: Function-local (Rust) vs. module-wide (OCaml) vs. whole-program (Haskell)
Annotation philosophy: Required at boundaries vs. only when ambiguous
Error quality: More inference often means more confusing error messages

Type inference isn’t magic—it’s a carefully designed system with tradeoffs. Understanding Hindley-Milner and bidirectional checking gives you the mental model to work with these systems effectively, whether you’re writing code or designing languages.