Types II: polymorphism and type inference

The simply typed lambda calculus of lesson 7 is safe but rigid. The identity function λx.x needs a separate copy for each type: one for integers, one for Booleans, one for functions from integers to integers. Polymorphism, from the Greek for 'many shapes', lets one piece of code work at many types. This lesson distinguishes the main kinds of polymorphism, then studies the most influential type system in functional programming, Hindley–Milner, which gives ML, OCaml, Haskell, F# and the core of Rust's type checker the ability to infer the most general type of a program without any annotations. We implement unification and type inference from scratch, and then look at subtyping and variance, where object-oriented languages add their own complications.

Kinds of polymorphism

Christopher Strachey distinguished two kinds of polymorphism in 1967, and Luca Cardelli and Peter Wegner refined the picture in 1985. Parametric polymorphism means a single definition works uniformly for all types, as the identity function or a list-reversal function does; the code never inspects the type. Ad-hoc polymorphism means one name has different implementations for different types, chosen by type, as with overloaded + for integers and strings, or Haskell type classes and Rust traits. Subtype polymorphism means a value of a subtype can be used wherever a supertype is expected, the basis of object-oriented programming. Coercion is a fourth, weaker form: values are converted automatically, as when C converts an int to a double.

Type schemes and let-polymorphism

In Hindley–Milner a polymorphic type is written with a type variable and a universal quantifier: the identity function has the type scheme ∀α. α → α, meaning 'for every type α, a function from α to α'. Each use of the function instantiates the scheme with fresh type variables, so id 3 uses it at int → int and id true at bool → bool. Type variables are conventionally written 'a, 'b in ML and a, b in Haskell.

The key design decision of Hindley–Milner is where polymorphism is allowed. A variable bound by let can be generalized to a type scheme; a variable bound by a lambda parameter cannot. So let id = fun x -> x in (id 3, id true) is well typed, but (fun id -> (id 3, id true)) (fun x -> x), which means the same thing, is rejected. This restriction, called let-polymorphism, is exactly what keeps type inference decidable. Allowing polymorphic function parameters gives System F, the polymorphic lambda calculus of Jean-Yves Girard and John Reynolds, for which J. B. Wells proved in 1994 that complete type inference is undecidable.

The generalization step quantifies only type variables that do not appear free in the context. If a variable's type is still constrained by something outside the let, it must not be generalized, because its eventual type is not up to us. This side condition is easy to forget, and forgetting it makes the type system unsound.

Unification

Type inference works by generating equations between types and solving them. If a program applies f to x, then f's type must equal type-of-x → some fresh result type. Solving such equations is unification, introduced by J. A. Robinson in 1965 for automated theorem proving. Unify two types by comparing their structure: identical types unify trivially; a type variable unifies with any type by being bound to it; two function types unify if their parameter types unify and their result types unify; anything else is a type error. The occurs check refuses to bind a variable α to a type that contains α, such as α → int, since that would require an infinite type. It is exactly the check that rejects self-application.

# Unification: find a substitution that makes two types equal (Robinson, 1965).
# Types: "int" | "bool" | ("var", name) | ("->", t1, t2) | ("list", t)
def resolve(t, s):
    while isinstance(t, tuple) and t[0] == "var" and t[1] in s:
        t = s[t[1]]
    return t

def occurs(name, t, s):
    t = resolve(t, s)
    if t == ("var", name): return True
    return isinstance(t, tuple) and t[0] != "var" and any(occurs(name, a, s) for a in t[1:])

def unify(a, b, s):
    a, b = resolve(a, s), resolve(b, s)
    if a == b: return s
    if isinstance(a, tuple) and a[0] == "var":
        if occurs(a[1], b, s): raise TypeError(f"occurs check: {a[1]} appears in {show(b, s)}")
        return {**s, a[1]: b}
    if isinstance(b, tuple) and b[0] == "var": return unify(b, a, s)
    if isinstance(a, tuple) and isinstance(b, tuple) and a[0] == b[0] and len(a) == len(b):
        for x, y in zip(a[1:], b[1:]): s = unify(x, y, s)
        return s
    raise TypeError(f"cannot unify {show(a, s)} with {show(b, s)}")

def show(t, s={}):
    t = resolve(t, s)
    if isinstance(t, str): return t
    if t[0] == "var": return "'" + t[1]
    if t[0] == "list": return show(t[1], s) + " list"
    return f"({show(t[1], s)} -> {show(t[2], s)})"

V = lambda n: ("var", n)
cases = [
    (("->", V("a"), "int"), ("->", "bool", V("b"))),
    (("->", V("a"), V("a")), ("->", "int", V("b"))),
    (("list", V("a")), ("list", ("->", "int", "bool"))),
    (("->", V("a"), V("a")), ("->", "int", "bool")),
    (V("a"), ("->", V("a"), "int")),
]
for t1, t2 in cases:
    try:
        s = unify(t1, t2, {})
        print(f"{show(t1):18} ~ {show(t2):22} solved: {{{', '.join(f'{k} = {show(v, s)}' for k, v in s.items())}}}")
    except TypeError as e:
        print(f"{show(t1):18} ~ {show(t2):22} fails: {e}")

('a -> int)        ~ (bool -> 'b)           solved: {a = bool, b = int}
('a -> 'a)         ~ (int -> 'b)            solved: {a = int, b = int}
'a list            ~ (int -> bool) list     solved: {a = (int -> bool)}
('a -> 'a)         ~ (int -> bool)          fails: cannot unify int with bool
'a                 ~ ('a -> int)            fails: occurs check: a appears in ('a -> int)

Algorithm W

Roger Hindley (1969) showed that every typable term of a certain system has a most general, or principal, type, and Robin Milner (1978) gave an algorithm, Algorithm W, to compute it, proving that it is sound and complete: it finds a type whenever one exists, and the type it finds is the most general. Luis Damas completed the proofs in 1982, so the system is often called Damas–Hindley–Milner. The algorithm walks the abstract syntax tree. For a variable, it instantiates the variable's scheme with fresh type variables. For a lambda, it invents a fresh type variable for the parameter. For an application, it unifies the function's type with argument type → fresh result. For let, it infers the bound expression's type, generalizes it, and continues with the body.

# Hindley–Milner type inference (Algorithm W style) for a small ML-like language.
#   e ::= n | True | False | x | ("lam", x, e) | ("app", e, e) | ("let", x, e, e) | ("if", e, e, e)
#         | ("pair", e, e)
import itertools
counter = itertools.count()
def fresh(): return ("var", f"t{next(counter)}")

def resolve(t, s):
    while isinstance(t, tuple) and t[0] == "var" and t[1] in s: t = s[t[1]]
    return t
def apply(t, s):
    t = resolve(t, s)
    if isinstance(t, tuple) and t[0] != "var": return (t[0],) + tuple(apply(a, s) for a in t[1:])
    return t
def ftv(t):
    if isinstance(t, str): return set()
    if t[0] == "var": return {t[1]}
    return set().union(*(ftv(a) for a in t[1:]))
def unify(a, b, s):
    a, b = resolve(a, s), resolve(b, s)
    if a == b: return s
    if isinstance(a, tuple) and a[0] == "var":
        if a[1] in ftv(apply(b, s)): raise TypeError("occurs check failed: infinite type")
        return {**s, a[1]: b}
    if isinstance(b, tuple) and b[0] == "var": return unify(b, a, s)
    if isinstance(a, tuple) and isinstance(b, tuple) and a[0] == b[0]:
        for x, y in zip(a[1:], b[1:]): s = unify(x, y, s)
        return s
    raise TypeError(f"type mismatch: {pretty(apply(a, s))} vs {pretty(apply(b, s))}")

def generalize(t, env, s):
    t = apply(t, s)
    env_vars = set().union(*(ftv(apply(sch[1], s)) - set(sch[0]) for sch in env.values())) if env else set()
    return (sorted(ftv(t) - env_vars), t)                  # a type scheme: forall vars. type
def instantiate(scheme):
    vars_, t = scheme
    m = {v: fresh() for v in vars_}
    def go(t):
        if isinstance(t, str): return t
        if t[0] == "var": return m.get(t[1], t)
        return (t[0],) + tuple(go(a) for a in t[1:])
    return go(t)

def infer(env, e, s):
    if isinstance(e, bool): return "bool", s
    if isinstance(e, int): return "int", s
    if isinstance(e, str):
        if e not in env: raise TypeError(f"unbound variable {e}")
        return instantiate(env[e]), s
    tag = e[0]
    if tag == "lam":
        a = fresh()
        tb, s = infer({**env, e[1]: ([], a)}, e[2], s)          # lambda-bound: monomorphic
        return ("->", a, tb), s
    if tag == "app":
        tf, s = infer(env, e[1], s); ta, s = infer(env, e[2], s); r = fresh()
        return r, unify(tf, ("->", ta, r), s)
    if tag == "let":
        t1, s = infer(env, e[2], s)
        return infer({**env, e[1]: generalize(t1, env, s)}, e[3], s)   # let-bound: polymorphic
    if tag == "if":
        tc, s = infer(env, e[1], s); s = unify(tc, "bool", s)
        t1, s = infer(env, e[2], s); t2, s = infer(env, e[3], s)
        return t1, unify(t1, t2, s)
    if tag == "pair":
        t1, s = infer(env, e[1], s); t2, s = infer(env, e[2], s)
        return ("*", t1, t2), s

def pretty(t):
    names = {}
    def go(t):
        if isinstance(t, str): return t
        if t[0] == "var": return names.setdefault(t[1], "'" + "abcdefgh"[len(names)])
        if t[0] == "*": return f"{go(t[1])} * {go(t[2])}"
        left = go(t[1]); left = f"({left})" if isinstance(t[1], tuple) and t[1][0] == "->" else left
        return f"{left} -> {go(t[2])}"
    return go(t)

BUILTINS = {"add": ([], ("->", "int", ("->", "int", "int"))),
            "eq":  ([], ("->", "int", ("->", "int", "bool")))}
def type_of(e):
    t, s = infer(BUILTINS, e, {})
    return pretty(apply(t, s))

progs = {
    "fun x -> x":                          ("lam", "x", "x"),
    "fun f -> fun x -> f (f x)":           ("lam", "f", ("lam", "x", ("app", "f", ("app", "f", "x")))),
    "fun f -> fun g -> fun x -> f (g x)":  ("lam", "f", ("lam", "g", ("lam", "x", ("app", "f", ("app", "g", "x"))))),
    "fun x -> add x 1":                    ("lam", "x", ("app", ("app", "add", "x"), 1)),
    "let id = fun x -> x in (id 3, id true)":
        ("let", "id", ("lam", "x", "x"), ("pair", ("app", "id", 3), ("app", "id", True))),
    "(fun id -> (id 3, id true)) (fun x -> x)":
        ("app", ("lam", "id", ("pair", ("app", "id", 3), ("app", "id", True))), ("lam", "x", "x")),
    "fun x -> x x":                        ("lam", "x", ("app", "x", "x")),
    "if true then 1 else false":           ("if", True, 1, False),
}
for text, e in progs.items():
    try:
        print(f"{text:42} : {type_of(e)}")
    except TypeError as err:
        print(f"{text:42} rejected: {err}")

fun x -> x                                 : 'a -> 'a
fun f -> fun x -> f (f x)                  : ('a -> 'a) -> 'a -> 'a
fun f -> fun g -> fun x -> f (g x)         : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
fun x -> add x 1                           : int -> int
let id = fun x -> x in (id 3, id true)     : int * bool
(fun id -> (id 3, id true)) (fun x -> x)   rejected: type mismatch: int vs bool
fun x -> x x                               rejected: occurs check failed: infinite type
if true then 1 else false                  rejected: type mismatch: int vs bool

The output shows the most general types: twice has type ('a -> 'a) -> 'a -> 'a and compose has type ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b, exactly what OCaml or Haskell would report up to the naming of variables. It also shows the let-polymorphism rule at work: the let version of id is used at two types, while the lambda-bound version is rejected. And it shows the occurs check rejecting fun x -> x x.

In theory Hindley–Milner inference can take exponential time on carefully constructed programs with deeply nested lets, a result due to Harry Mairson and others in 1990, but in practice it runs in nearly linear time, which is why ML programmers almost never write type annotations. Two practical refinements matter. ML's value restriction generalizes only syntactic values, because generalizing the type of a mutable reference cell would be unsound. Haskell's type classes extend inference with constraints, so that the inferred type of a function using + becomes Num a => a -> a -> a, read 'for any numeric type a'.

Ad-hoc polymorphism: type classes and traits

Haskell's type classes, introduced by Philip Wadler and Stephen Blott in 1989, make overloading principled. A class such as Eq or Show declares operations; each type provides an instance; and a function that uses those operations gets a constraint in its type. Rust's traits, Swift's protocols, Scala's implicits and C++20's concepts are close relatives. There are two implementation strategies. Monomorphization, used by Rust and C++, compiles a separate copy of a generic function for each type it is used at, giving fast code and larger binaries. Dictionary passing, used by Haskell and in effect by Go's generics and Java's interfaces, compiles one copy that receives a table of the needed operations at run time.

use std::fmt::Display;

// Bounded parametric polymorphism: T can be any type that implements Display + PartialOrd.
fn largest<T: PartialOrd + Display + Copy>(xs: &[T]) -> T {
    let mut best = xs[0];
    for &x in xs {
        if x > best { best = x; }
    }
    best
}

// Ad-hoc polymorphism through a trait: each type supplies its own implementation.
trait Describe { fn describe(&self) -> String; }
impl Describe for i32  { fn describe(&self) -> String { format!("the integer {}", self) } }
impl Describe for bool { fn describe(&self) -> String { format!("the Boolean {}", self) } }

fn main() {
    println!("{}", largest(&[3, 9, 4]));
    println!("{}", largest(&[2.5, -1.0]));
    println!("{}", largest(&['q', 'z', 'a']));
    println!("{} / {}", 7.describe(), true.describe());
}

9
2.5
z
the integer 7 / the Boolean true

Java takes a third route for generics: type erasure. The compiler checks List<String> statically and then erases the type argument, so at run time there is only List. This kept compatibility with pre-generic code in 2004, at the price that Java cannot create a new T() or a T[] and cannot have List<int>, only List<Integer>. C# keeps type arguments at run time (reified generics) and specializes code for value types. Project Valhalla in Java has been working for years to add value types and specialized generics.

Subtyping and variance

Subtyping says that a value of type S may be used where a T is expected, written S <: T. For object types, S is a subtype if it has at least the fields and methods of T. The interesting question is how subtyping interacts with type constructors. A constructor is covariant if it preserves the direction of subtyping (if Dog <: Animal then ImmutableList<Dog> <: ImmutableList<Animal>), contravariant if it reverses it, and invariant if neither holds. Functions are the classic case: a function type is contravariant in its parameter and covariant in its result.

In words: a function that accepts any Animal can be used where a function on Dogs is needed, because it can certainly handle Dogs, but not the other way around. A function returning Dogs can be used where one returning Animals is needed. Mutable containers must be invariant: a mutable list of Dogs is not a list of Animals, because someone could insert a Cat. That is exactly the hole Java's covariant arrays leave open (lesson 7). Java generics are invariant and recover flexibility with use-site wildcards (? extends T for reading, ? super T for writing); Kotlin, C# and Scala add declaration-site annotations such as out and in.

import java.util.ArrayList;
import java.util.List;

public class Variance {
    static double sum(List<? extends Number> xs) {      // covariant use: read only
        double t = 0;
        for (Number n : xs) t += n.doubleValue();
        return t;
    }
    public static void main(String[] args) {
        List<Integer> ints = new ArrayList<>(List.of(1, 2, 3));
        System.out.println(sum(ints));                   // fine with the wildcard
        List<Number> nums = ints;                        // rejected: generics are invariant
    }
}

$ javac Variance.java
Variance.java:13: error: incompatible types: List<Integer> cannot be converted to List<Number>
        List<Number> nums = ints;                        // rejected: generics are invariant
                            ^
1 error

from typing import Callable

class Animal: ...
class Dog(Animal):
    def bark(self) -> str: return "woof"

def walk_all(handler: Callable[[Dog], str]) -> None: ...

def any_animal(a: Animal) -> str: return "an animal"
def dog_only(d: Dog) -> str: return d.bark()

walk_all(any_animal)    # accepted: a function on Animals can handle Dogs (contravariant parameters)

def feed_all(handler: Callable[[Animal], str]) -> None: ...
feed_all(dog_only)      # rejected: a Dog-only function cannot handle every Animal

$ mypy --strict handlers.py
handlers.py:15: error: Argument 1 to "feed_all" has incompatible type "Callable[[Dog], str]"; expected "Callable[[Animal], str]"  [arg-type]

Local type inference in mainstream languages

Most mainstream languages do not use full Hindley–Milner inference, partly because subtyping and overloading make it much harder. Instead they use local type inference: the type of a variable is inferred from its initializer (auto in C++11, var in Java 10 and C#, let in Swift, := in Go), and lambda parameter types are inferred from the expected function type. TypeScript, Kotlin and Scala use bidirectional type checking, which alternates between checking an expression against an expected type and inferring a type from an expression, and which scales to rich type systems while keeping error messages local. Rust uses Hindley–Milner-style unification within a function body but requires annotations on function signatures, a deliberate choice so that a function's interface is always written down.

Worked examples