Polymorphism & Type Inference

In a monomorphic type system, every expression has exactly one concrete type. C is monomorphic: int add(int a, int b) works only for int. If you want to add floats, you write a separate float fadd(float a, float b). This is tedious and violates the DRY principle, but worse, it means the type system cannot express the idea that addition is the same operation at its core.

The simplest polymorphism demand arises from the identity function. Logically, id(x) = x is the same function regardless of what x is — it does nothing to its argument. Yet in a monomorphic system you need one id per type. This explosion of identical code for structurally identical operations is the core problem polymorphism solves.

Ad-hoc polymorphism (overloading) is one escape hatch: you write multiple definitions under one name and the compiler picks the right one by the argument type. C++ and Java do this. But overloaded functions can behave differently for different types — + on strings concatenates, on ints adds. This is not the same as saying a single implementation works uniformly.

Parametric polymorphism is the stronger, cleaner notion: a single implementation that works uniformly for all types because it never inspects the type of its argument. The identity function id : ∀α. α → α is the canonical example. The ∀α says 'for any type α you choose to substitute here, this function accepts a value of that type and returns one of the same type.' The implementation is oblivious to what α actually is.

-- Monomorphic C-style: one function per type
int    id_int(int x)    { return x; }
char*  id_str(char* x)  { return x; }
double id_dbl(double x) { return x; }

-- Haskell: one parametrically polymorphic function
id :: forall a. a -> a
id x = x

-- Works for any type -- the type variable 'a' is a placeholder
id 42        -- a ~ Int
id "hello"   -- a ~ String
id id        -- a ~ (forall b. b -> b)

System F (also called the second-order polymorphic lambda calculus) is the formal language that makes parametric polymorphism precise. It was discovered independently by Jean-Yves Girard (1972, in proof theory) and John Reynolds (1974, in computer science).

System F extends the simply-typed lambda calculus with two new forms:

1. Type abstraction Λα. e — a term that abstracts over a type variable α
2. Type application e [τ] — instantiating a type-abstract term with a concrete type τ

The typing rules are:

• If e : τ and α does not appear free in the context, then Λα. e : ∀α. τ
• If e : ∀α. τ, then e [σ] : τ[σ/α] (substituting σ for α in τ)

The identity function in System F is written:

id = Λα. λ(x:α). x

and has type ∀α. α → α. To use it on integers you write id [Int] 42, which first instantiates the type variable (getting λ(x:Int). x : Int → Int) and then applies it to 42.

Key property — parametricity (Reynolds's theorem): Any term of type ∀α. α → α in System F must be the identity function. You cannot write a different function at this type. This is because the implementation cannot inspect α — it has no operations to apply to a value of unknown type — so the only thing it can do with its argument is return it. This free theorem is enormously powerful: the type alone tells you what the function does.

The bad news about System F: Full type inference for System F is undecidable (Wells, 1994). You cannot always reconstruct the type of an arbitrary System F term without annotations. This is why real languages do not implement full System F directly — they use the decidable fragment called Hindley-Milner.

-- System F identity, written out explicitly (Haskell with RankNTypes)
{-# LANGUAGE RankNTypes #-}

-- The type forall a. a -> a is a first-class type in System F
id :: forall a. a -> a
id = \x -> x

-- A rank-2 function: takes a polymorphic function as argument
-- This requires going BEYOND Hindley-Milner (needs explicit annotation)
applyToIntAndBool :: (forall a. a -> a) -> (Int, Bool)
applyToIntAndBool f = (f 42, f True)

-- Without the annotation, HM cannot infer the rank-2 type

Hindley-Milner (HM) is a restriction of System F that sacrifices some expressiveness to gain complete type inference — the ability to reconstruct the unique principal type of any expression without any annotations. It was described by Roger Hindley (1969) and Robin Milner (1978), with Damas and Milner giving the formal completeness proof in 1982.

The key restriction is that type variables can only be universally quantified at the outermost level of a let binding, not inside function types. This is called prenex or rank-1 polymorphism. Concretely:

• ✓ id : ∀α. α → α — polymorphic at top level
• ✗ (∀α. α → α) → Int — polymorphic inside a function argument (rank-2)

The two syntactic layers in HM are:

• Monotypes (τ): concrete types with no ∀ — Int, Bool, τ₁ → τ₂, [τ], etc., plus type variables α which act as unknowns to be solved
• Type schemes (σ): ∀α₁...αₙ. τ — a monotype with some variables universally quantified

The crucial rule is let-polymorphism: when you write let f = e₁ in e₂, the compiler generalizes the type of e₁ by universally quantifying all free type variables, producing a scheme. Inside e₂, each use of f gets a fresh copy of the scheme with new type variables, so each use can be instantiated independently.

This is why let id = λx. x in (id 1, id True) typechecks: the first id gets α₁ → α₁ with α₁ ~ Int, the second gets α₂ → α₂ with α₂ ~ Bool, and they don't interfere. But (λid. (id 1, id True)) (λx. x) fails in HM — here id is a lambda-bound variable, not a let-bound one, so it gets a monomorphic type variable, and using it at both Int and Bool creates a contradiction.

-- let-polymorphism works:
let myId = \x -> x
in (myId 1, myId True)   -- OK: two independent instantiations

-- lambda-bound: does NOT get generalized in HM
-- The expression below fails to typecheck in strict HM:
-- (\myId -> (myId 1, myId True)) (\x -> x)
-- Error: cannot unify Int with Bool

-- In OCaml:
let id x = x in
let _ = id 1 in          (* id : int -> int *)
let _ = id true in       (* id : bool -> bool *)
()  (* These look at first like contradictions -- but
       each use of id freshly instantiates the scheme *)

-- The let/lambda distinction is fundamental to HM
let polymorphic_ok = fun () ->
  let f = fun x -> x in  (* f : 'a -> 'a, a type scheme *)
  (f 1, f true)          (* fine *)

(* monomorphic because lambda-bound, not let-bound *)
let monomorphic_fail = fun f -> (f 1, f true)
(* OCaml infers f : int -> int, then rejects f true *)

At the heart of type inference is unification — an algorithm for finding a substitution that makes two terms identical. Robinson's unification algorithm (1965) solves equations over first-order terms, and it is exactly what HM uses to solve type equations.

A substitution S is a mapping from type variables to types. Applying S to a type replaces each variable with its mapped type. The unification problem is: given two types τ₁ and τ₂, find a most general unifier (mgu) — a substitution S such that S(τ₁) = S(τ₂), and S is as general as possible (any other unifier is a specialization of S).

Robinson's algorithm (structural recursion):

unify(τ₁, τ₂):
  if τ₁ == τ₂: return empty substitution
  if τ₁ is a type variable α:
    occurs_check(α, τ₂)   -- see below
    return {α ↦ τ₂}
  if τ₂ is a type variable α:
    occurs_check(α, τ₁)
    return {α ↦ τ₁}
  if τ₁ = C τ₁₁...τ₁ₙ and τ₂ = C τ₂₁...τ₂ₙ (same constructor C, same arity):
    S = unify(τ₁₁, τ₂₁)
    for i = 2..n: S = compose(S, unify(S(τ₁ᵢ), S(τ₂ᵢ)))
    return S
  else: FAIL (types are incompatible)

The occurs check: Before substituting α ↦ τ, we verify that α does not appear free in τ. Without this check, unify(α, α → β) would produce α = α → β, an infinite type. With the check, we reject this — most HM implementations correctly report a type error here. (Prolog historically skips the occurs check for performance, which is unsound.)

Example: Unify (α → Bool) with (Int → β):

• Both are → applied to two arguments
• Unify α with Int: S₁ = {α ↦ Int}
• Unify Bool with β: S₂ = {β ↦ Bool}
• Result: {α ↦ Int, β ↦ Bool}
• Substituted: (Int → Bool) on both sides ✓

Unification is complete: if a unifier exists, Robinson's algorithm finds the most general one. The mgu is unique up to renaming of variables.

# Robinson's unification in Python (simplified, no occurs check for brevity)
from dataclasses import dataclass
from typing import Optional

@dataclass(frozen=True)
class TVar:
    name: str

@dataclass(frozen=True)
class TApp:
    constructor: str
    args: tuple  # of Type

Type = TVar | TApp

def apply_subst(subst: dict, t: Type) -> Type:
    if isinstance(t, TVar):
        return apply_subst(subst, subst[t.name]) if t.name in subst else t
    return TApp(t.constructor, tuple(apply_subst(subst, a) for a in t.args))

def compose(s1: dict, s2: dict) -> dict:
    result = {k: apply_subst(s1, v) for k, v in s2.items()}
    result.update(s1)
    return result

def occurs(var_name: str, t: Type) -> bool:
    if isinstance(t, TVar): return t.name == var_name
    return any(occurs(var_name, a) for a in t.args)

def unify(t1: Type, t2: Type) -> dict:
    t1, t2 = apply_subst({}, t1), apply_subst({}, t2)
    if t1 == t2:
        return {}
    if isinstance(t1, TVar):
        if occurs(t1.name, t2): raise TypeError(f"Occurs check: {t1.name} in {t2}")
        return {t1.name: t2}
    if isinstance(t2, TVar):
        if occurs(t2.name, t1): raise TypeError(f"Occurs check: {t2.name} in {t1}")
        return {t2.name: t1}
    if isinstance(t1, TApp) and isinstance(t2, TApp):
        if t1.constructor != t2.constructor or len(t1.args) != len(t2.args):
            raise TypeError(f"Cannot unify {t1} with {t2}")
        subst = {}
        for a1, a2 in zip(t1.args, t2.args):
            subst = compose(unify(apply_subst(subst, a1),
                                  apply_subst(subst, a2)), subst)
        return subst
    raise TypeError("Unification failed")

# Example: unify (a -> Bool) with (Int -> b)
arrow = lambda x, y: TApp("->", (x, y))
alpha, beta = TVar("a"), TVar("b")
Int, Bool = TApp("Int", ()), TApp("Bool", ())
result = unify(arrow(alpha, Bool), arrow(Int, beta))
print(result)  # {'a': TApp('Int',...), 'b': TApp('Bool',...)}

Algorithm W is Damas and Milner's type inference algorithm for HM. Given a typing context Γ (mapping variable names to type schemes) and an expression e, it returns a substitution S and a type τ such that S(Γ) ⊢ e : τ.

The algorithm is defined by recursion on the expression structure:

Variables x: Look up the scheme ∀α₁...αₙ. τ for x in Γ. Create fresh type variables β₁...βₙ and return (id_substitution, τ[β₁/α₁,...,βₙ/αₙ]). This instantiation is where polymorphism is exploited — each use of a polymorphic function gets fresh variables.

Lambda λx. e: Create a fresh type variable α. Infer the type of e in Γ extended with x : α. Return the function type (possibly substituted α) → (inferred type of e).

Application e₁ e₂: Infer type τ₁ for e₁ and τ₂ for e₂. Create a fresh variable β. Unify τ₁ with (τ₂ → β). Return S(β) as the result type.

Let let x = e₁ in e₂: This is the critical case for polymorphism. Infer type τ₁ for e₁. Generalize τ₁ by quantifying all type variables that are free in τ₁ but not in Γ — this produces a type scheme σ. Infer the type of e₂ in Γ extended with x : σ. Return that type.

Generalization is what creates new polymorphic bindings. Variables that appear free in the context Γ cannot be generalized — they are constrained by an enclosing binding. Only the new free variables in τ₁ become ∀-quantified.

Algorithm W runs in nearly-linear time (almost linear in the expression size due to the union-find data structure used for efficient substitution). Its correctness has two parts:

• Soundness: if W returns (S, τ), then S(Γ) ⊢ e : τ is a valid derivation
• Completeness: if S(Γ) ⊢ e : τ for any S and τ, then W succeeds and returns the principal (most general) type

-- Tracing Algorithm W on: let f = \x -> x in f f

-- Step 1: infer type of  \x -> x  in empty context
--   Fresh variable: a0
--   Infer body x in {x : a0}  --> returns a0
--   Type of lambda: a0 -> a0
--   Substitution: empty

-- Step 2: generalize  a0 -> a0  in empty context
--   Free vars in type: {a0}
--   Free vars in context: {}
--   Quantify all: scheme = forall a0. a0 -> a0

-- Step 3: infer type of  f f  in {f : forall a0. a0 -> a0}
--   Infer f (function position):
--     instantiate scheme with fresh a1: type = a1 -> a1
--   Infer f (argument position):
--     instantiate scheme with fresh a2: type = a2 -> a2
--   Create fresh result variable a3
--   Unify (a1 -> a1) with ((a2 -> a2) -> a3)
--     Unify a1 with (a2 -> a2): S1 = {a1 |-> a2 -> a2}
--     Unify a1 with a3:         S2 = {a3 |-> a1} = {a3 |-> a2 -> a2}
--   Result type: S(a3) = a2 -> a2

-- Final principal type of the whole expression:
-- forall a. a -> a
-- (renaming a2 to a)

main :: IO ()
main = do
  let f = \x -> x
  print (f f 42)   -- = 42, type is Int

The distinction between monotypes and type schemes is not just formal bookkeeping — it has deep consequences for what programs typecheck.

Generalization happens only at let-bindings, and only for type variables that are not constrained by the outer context. The rule is:

gen(Γ, τ) = ∀(ftv(τ) − ftv(Γ)). τ

where ftv(τ) is the set of free type variables in τ. The intuition: variables already constrained by the surrounding context represent specific types chosen by the caller. Only truly unconstrained variables represent genuine polymorphism.

The value restriction is a crucial soundness constraint that arises when polymorphism interacts with mutable state. Consider this ML code:

let r = ref []  (* What is the type? *)

Naively, Algorithm W would give r : ∀α. α list ref — a polymorphic mutable cell. But then:

r := [1];        (* instantiate α ~ int *)
let x = !r in   (* instantiate α ~ string??? *)

This would be unsound: we store an int list, then read it as string list, allowing a segfault.

The value restriction (Wright, 1995) fixes this: generalization is only performed when the right-hand side of a let is a syntactic value (a lambda, a literal, a constructor applied to values — not a function application or a ref creation). ref [] is an application, not a value, so the type variable cannot be generalized. The compiler either infers a monomorphic int list ref based on usage, or reports an ambiguity error.

ML and OCaml both enforce the value restriction. Haskell sidesteps it differently — IO types and the type class system prevent the problematic pattern at a different level. Understanding the value restriction tells you why you sometimes see confusing "this type cannot be generalized" errors in OCaml.

-- OCaml: value restriction in action
let ok_poly = fun x -> x       (* value: a lambda *)
(* ok_poly : 'a -> 'a, properly polymorphic *)

let r = ref []  (* NOT a value: it is an application of 'ref' *)
(* r : '_weak1 list ref  -- weak type variable, not polymorphic *)

(* Fixing it: make it a function (a value) *)
let poly_ref () = ref []
(* poly_ref : unit -> 'a list ref  -- polymorphic! *)
(* Each CALL creates a new ref, so no aliasing problem *)

(* Why the value restriction is needed: unsound example
   (would typecheck without the restriction) *)
let evil () =
  let r = ref [] in              (* suppose: r : forall a. a list ref *)
  r := [1];                      (* use r : int list ref, store [1]   *)
  let x : string list = !r in   (* use r : string list ref, BOOM      *)
  List.hd x

One of the most beautiful consequences of parametric polymorphism is parametricity: the type of a polymorphic function places strong constraints on what the function can possibly do. Reynolds formalized this as the abstraction theorem (1983): every polymorphic function preserves all relations between types.

Practically, this gives rise to free theorems (Wadler, 1989): theorems you get for free just from the type, without looking at the implementation.

Example 1: Any function f : ∀α. [α] → [α] (takes a list of α, returns a list of α) must satisfy: for any function g : A → B, map g (f xs) = f (map g xs). That is, f commutes with map. Why? Because f cannot inspect the elements of the list (it does not know their type), so it can only rearrange, duplicate, or drop elements. The only way to rearrange and then map is the same as mapping and then rearranging.

Example 2: Any function f : ∀α. α → α must be the identity. (There is nothing else you can do with a value of unknown type.)

Example 3: Any function f : ∀α. α → [α] must return a list containing only copies of its input. It cannot conjure new α-values from nowhere.

Free theorems are not just theoretical curiosities. GHC uses them for optimization: if a function has a parametric type, the compiler can apply equational rewrites (like the map fusion law) knowing they are universally valid. The whole stream fusion optimization in Haskell's standard library relies on free theorems.

Parametricity also provides a security property: if a module exports a value of an abstract type T, and T is opaque to clients, then parametricity guarantees that clients cannot forge or inspect values of T — this is the type-theoretic foundation of data abstraction.

-- Free theorem for reverse : forall a. [a] -> [a]
-- For any f : a -> b:
--   map f (reverse xs) = reverse (map f xs)

-- We can VERIFY this holds without reading reverse's source:
import Data.List (reverse)

verify :: Eq b => (a -> b) -> [a] -> Bool
verify f xs = map f (reverse xs) == reverse (map f xs)

-- This is true for ALL f and xs by parametricity.

-- Another free theorem:
-- head . map f = f . head   (when list is non-empty)
-- Proof sketch: head can only look at position, not value.
-- map f changes values but not positions.
-- So head after map == map-then-head.

-- GHC uses this style of reasoning for rewrite rules:
{-# RULES "map/map" forall f g xs.
    map f (map g xs) = map (f . g) xs #-}
-- This rewrite is safe to apply because it is a free theorem!
-- No need to examine what f and g actually do.

How do real compilers implement Hindley-Milner inference? The modern approach uses constraint generation followed by constraint solving, which is more amenable to good error messages than the original Algorithm W (which can report errors far from their source).

Two-phase approach:

1. Constraint generation: Walk the AST and generate type equations τ₁ = τ₂ and instance constraints τ ≺ σ (τ is an instance of scheme σ). Each subexpression gets a fresh type variable; constraints express how subexpressions relate.
2. Constraint solving: Run unification on the equations, propagating substitutions. Solve instance constraints by generalization.

OCaml implements a close variant of Algorithm W with mutable unification variables (refs to optional types). When you unify two types, you mutate the unification variables in place — this is far more efficient than building explicit substitution maps. GHC Haskell uses a similar approach with IORef-based unification variables internally.

Type error messages: One of the famous weaknesses of HM-based inference is error message quality. When unification fails, the error can be reported at the unification site, which may be far from where the programmer made the mistake. Modern systems use constraint origin tracking to report errors at the original source location.

Haskell extensions beyond HM:

• Type classes: add qualified types (Show a) => a -> String. Inference is still mostly HM but now must also solve class constraints via dictionary passing.
• GADTs (Generalised Algebraic Data Types): require bidirectional type-checking; pure inference is undecidable, so type annotations are required.
• Rank-N types (forall under arrows): require explicit annotations and go beyond HM.
• Type families and functional dependencies: add type-level computation; inference becomes complex and can fail to terminate.

Rust uses a bidirectional variant of HM with a second pass for trait resolution. The lifetime system is inferred separately via a region-inference algorithm that is also unification-based at its core.

-- Demonstrating HM inference in OCaml step by step
-- Consider: let compose f g x = f (g x)

-- Step 1: Assign fresh vars
--   f : a, g : b, x : c, result : d
-- Step 2: g x  --> generates constraint: b = c -> e (fresh e)
--   type of (g x): e
-- Step 3: f (g x) --> generates constraint: a = e -> d
--   type of f(g x): d
-- Step 4: lambda x.  : c -> d
-- Step 5: lambda g.  : b -> c -> d = (c->e) -> c -> d
-- Step 6: lambda f.  : a -> ... = (e->d) -> (c->e) -> c -> d
-- Step 7: generalize all free vars {a,b,c,d,e} -> renamed to a,b,c

-- OCaml confirms:
(* # let compose f g x = f (g x) ;; *)
(* val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b = <fun> *)

(* Note: OCaml uses 'a not forall a -- the scheme is implicit *)

(* Haskell makes it explicit with ScopedTypeVariables: *)
{- 
compose :: forall a b c. (b -> c) -> (a -> b) -> a -> c
compose f g x = f (g x)
-}

Hindley-Milner achieves complete inference only for rank-1 (prenex) polymorphism. Understanding its limits reveals why modern languages sometimes require annotations and what the cost of richer type systems is.

Rank of a type: The rank of a type is the maximum depth at which ∀ appears to the left of an arrow (in a contravariant position). Rank-1 types have ∀ only at the outermost level. Rank-2 types have ∀ at most one arrow deep. Full System F has no restriction.

Why does rank matter for inference? In rank-1 HM, when you apply a polymorphic function to an argument, you always instantiate a scheme from the context — you know statically which polymorphic binding is being used. In rank-2, the argument itself may be polymorphic, and the compiler needs to figure out how it should be polymorphic from context — this is underdetermined without annotations.

Impredicativity is the related issue where a type variable is instantiated with a polymorphic type (one containing ∀). HM allows instantiating ∀α. α → α with Int → Int, but not with ∀β. β → β. Impredicative instantiation makes unification much harder (it becomes undecidable in general).

Practical consequence: In Haskell, if you need to pass a polymorphic function as an argument (rank-2), you must write the type signature:

runOnBoth :: (forall a. a -> a) -> (Int, Bool)
runOnBoth f = (f 1, f True)  -- requires annotation

Without the annotation, GHC cannot infer this type. This is not a GHC limitation — it is a fundamental limit of any HM-style inference.

MLF and other extensions: Researchers have developed type systems like MLF (Botlan & Rémy, 2003) and HMF that extend HM to support impredicativity with a minimal annotation burden, but they are more complex and not widely deployed in production compilers.

{-# LANGUAGE RankNTypes #-}

-- Rank-1: OK in HM, no annotation needed
length' :: [a] -> Int        -- forall a. [a] -> Int
length' = length

-- Rank-2: needs explicit annotation
runOnBoth :: (forall a. a -> a) -> (Int, Bool)
runOnBoth f = (f 42, f True)   -- f used at two different types
-- Without the annotation, GHC says:
-- "Cannot instantiate unification variable with a type involving foralls"

-- Rank-2 in practice: ST monad's runST
-- runST :: (forall s. ST s a) -> a
-- The 'forall s' prevents the state thread from escaping!
-- This is a beautiful use of rank-2 types for safety.
import Control.Monad.ST
import Data.STRef

example :: Int
example = runST $ do
  ref <- newSTRef 0
  writeSTRef ref 42
  readSTRef ref
-- The 's' in 'ST s Int' is a phantom type that links the ref
-- to the runST scope -- it CANNOT escape because of rank-2.

A natural extension of parametric polymorphism is row polymorphism, which applies polymorphism to the fields of record and variant types. This is the type-theoretic foundation of structural subtyping in languages like TypeScript.

The problem: In HM, record types are concrete — {x: Int, y: Int} and {x: Int, y: Int, z: Bool} are different types. A function getX : {x: Int} → Int cannot accept a three-field record. This forces languages toward either inheritance (Java/C++) or entirely structural typing.

Row polymorphism (Wand, 1987; Rémy, 1989) extends types with row variables that stand for an unknown set of additional fields:

getX : ∀ρ. {x : Int | ρ} → Int

The row variable ρ represents "any additional fields." The function accepts {x: Int, y: String}, {x: Int}, {x: Int, z: Bool, w: Char} — any record that has at least an x: Int field. Inference extends naturally: unification now must unify rows as well as simple types.

TypeScript uses structural typing without formal row polymorphism, but the intent is similar: an object with at least the required fields is assignable to a record type. TypeScript's inference engine handles this through subtyping rather than unification.

OCaml's polymorphic variants and object types implement a form of row polymorphism. An OCaml method call obj#method infers a row-polymorphic type for obj — it accepts any object that has at least the method method.

Elm uses row polymorphism for records, and it is one of the reasons Elm can give such excellent type error messages: the compiler knows exactly which fields are required vs. which are extra.

-- OCaml object types use row polymorphism
(* A function that works on any object with a 'name' method *)
let greet obj = "Hello, " ^ obj#name
(* Inferred: greet : < name : string; .. > -> string *)
(* The '..' is the row variable! Accepts any object with name field *)

(* TypeScript equivalent -- structural typing *)
type HasName = { name: string }  -- minimum requirement

function greet(obj: HasName): string {
  return `Hello, ${obj.name}`
}

// Works with any object that has at least 'name'
greet({ name: "Alice" })                       // exact match
greet({ name: "Bob", age: 30, job: "dev" })   // extra fields OK

// Haskell Records (without row poly -- more rigid)
data Named = Named { name :: String }
greetH :: Named -> String
greetH obj = "Hello, " ++ name obj
-- This ONLY works for Named, not any record with a name field