Type checking and type inference

A type system classifies the values a program manipulates and the operations allowed on them, so that whole categories of errors, such as adding a boolean to an integer, calling a function with the wrong number of arguments or indexing something that is not an array, are caught before the program runs. For a compiler writer, types are also the information that drives code generation: they say how many bytes a variable occupies, which machine instruction implements +, and how arguments are passed. This lesson implements a type checker for Tern, then shows how a compiler can infer types that the programmer did not write. CMPUT-325 (lessons 7 and 8) covered type systems, polymorphism and the Hindley–Milner algorithm from the language designer's point of view; here we concentrate on how a checker is built and how inference is implemented inside a compiler.

Static and dynamic typing, strong and weak

A statically typed language checks types at compile time; a dynamically typed one checks them at run time, attaching a type tag to each value. C, Java, Rust, Go and Tern are static; Python, JavaScript and Ruby are dynamic. Static typing finds errors earlier and lets the compiler generate faster code because it knows representations in advance; dynamic typing is more flexible and needs no annotations. The distinction is blurring: TypeScript adds static types to JavaScript, Python's optional type hints are checked by separate tools such as mypy, and JIT compilers for dynamic languages recover static type information at run time by observing values. A separate axis is whether the type system is sound, guaranteeing that a well-typed program never performs an operation on the wrong kind of value. Java and Rust (outside unsafe code) aim for soundness; C does not, because casts and unions let a program reinterpret memory freely; TypeScript deliberately trades some soundness for convenience.

Type rules

Type systems are specified by inference rules, which say when an expression has a type in a given environment Γ that maps variables to types. The judgment \(\Gamma \vdash e : \tau\) reads: in environment Γ, expression e has type τ. A rule has premises above a line and a conclusion below. The rule for addition in Tern says that if both operands are integers, so is the sum; the rule for a variable says its type is whatever the environment records; the rule for a function call checks each argument against the parameter types.

Such rules translate almost directly into code. A type checker is a recursive function over the AST that, for each expression, checks its subexpressions and applies the rule for its node kind, returning the expression's type. Statements do not have types, but they are checked against context: a return statement must return a value of the enclosing function's declared return type, and the condition of an if must be a bool. In attribute grammar terms (lesson 5), expression types are synthesized and the expected return type is inherited.

Implementing a checker

The checker below implements those rules. It keeps a stack of scopes mapping variable names to types, much like lesson 5's resolver, and a table of function signatures collected in a first pass, so functions may call each other in any order. Three details are worth noting. First, when it finds an error, it returns a special error type that every rule accepts silently, so a single mistake does not trigger a cascade of messages about everything built from it. Second, var declarations without a type take the type of their initializer, a simple form of local type inference used by C#, Java (var since Java 10), C++ (auto) and Go (:=). Third, it checks that every path through a function returns, by having statement checking report whether a statement always returns: a return does, an if does when both of its branches do, and a while loop is assumed not to, because its body might execute zero times.

# A type checker for Tern. Types: "int", "bool", "[int]" and function
# signatures. Expressions return their type (synthesized); statements are
# checked against the enclosing function's return type (inherited).
# AST as nested tuples (see lesson 5 for the parser that builds the real one).
ERR = "<error>"                                       # absorbs further errors
BUILTINS = {"print": (["any"], "int"), "len": (["[int]"], "int"), "array": (["int"], "[int]")}
ARITH, CMP, EQ, LOGIC = set("+-*/%"), {"<", "<=", ">", ">="}, {"==", "!="}, {"&&", "||"}
class Checker:
    def __init__(c, funcs):
        c.errors = []
        c.sigs = dict(BUILTINS)
        for _, line, name, params, ret, body in funcs: c.sigs[name] = ([t for _, t in params], ret)
    def err(c, line, msg): c.errors.append(f"line {line}: {msg}"); return ERR
    def expr(c, e, env):
        tag, line = e[0], e[1]
        if tag == "num": return "int"
        if tag == "bool": return "bool"
        if tag == "name":
            for scope in reversed(env):
                if e[2] in scope: return scope[e[2]]
            return c.err(line, f"undeclared name {e[2]!r}")
        if tag == "bin":
            op, l, r = e[2], c.expr(e[3], env), c.expr(e[4], env)
            if ERR in (l, r): return ERR
            if op in ARITH | CMP:
                if l == r == "int": return "int" if op in ARITH else "bool"
                return c.err(line, f"operator {op!r} needs int operands, got {l} and {r}")
            if op in EQ:
                if l == r and l in ("int", "bool"): return "bool"
                return c.err(line, f"cannot compare {l} with {r}")
            if l == r == "bool": return "bool"
            return c.err(line, f"operator {op!r} needs bool operands, got {l} and {r}")
        if tag == "not":
            t = c.expr(e[2], env)
            return "bool" if t == "bool" else (t if t == ERR else c.err(line, f"'!' needs bool, got {t}"))
        if tag == "index":
            a, i = c.expr(e[2], env), c.expr(e[3], env)
            if a not in ("[int]", ERR): c.err(line, f"cannot index a value of type {a}")
            if i not in ("int", ERR): c.err(line, f"array index must be int, got {i}")
            return "int"
        if tag == "call":
            if e[2] not in c.sigs: return c.err(line, f"call to undeclared function {e[2]!r}")
            params, ret = c.sigs[e[2]]; args = [c.expr(a, env) for a in e[3]]
            if len(args) != len(params):
                return c.err(line, f"{e[2]} expects {len(params)} argument(s), got {len(args)}")
            for k, (p, a) in enumerate(zip(params, args), 1):
                if p != "any" and a not in (p, ERR):
                    c.err(line, f"argument {k} of {e[2]} must be {p}, got {a}")
            return ret
    def block(c, stmts, env, ret):
        env = env + [{}]; returns = False
        for s in stmts:
            tag, line = s[0], s[1]
            if returns: c.err(line, "unreachable statement after return"); break
            if tag == "var":
                t = c.expr(s[4], env)
                if s[3] and t not in (s[3], ERR): c.err(line, f"{s[2]!r} declared {s[3]} but initialized with {t}")
                env[-1][s[2]] = s[3] or t                 # local inference: var i = 0
            elif tag == "assign":
                tt, vt = c.expr(s[2], env), c.expr(s[3], env)
                if ERR not in (tt, vt) and tt != vt: c.err(line, f"cannot assign {vt} to a target of type {tt}")
            elif tag in ("if", "while"):
                if c.expr(s[2], env) not in ("bool", ERR): c.err(line, f"{tag} condition must be bool")
                r1 = c.block(s[3], env, ret)
                r2 = c.block(s[4], env, ret) if tag == "if" and s[4] else False
                returns = tag == "if" and r1 and r2         # both branches return
            elif tag == "return":
                t = c.expr(s[2], env)
                if t not in (ret, ERR): c.err(line, f"return type is {ret}, but returns {t}")
                returns = True
            elif tag == "expr": c.expr(s[2], env)
        return returns
    def check(c, funcs):
        for _, line, name, params, ret, body in funcs:
            if not c.block(body, [dict(params)], ret):
                c.err(line, f"function {name!r} may finish without returning a {ret}")
        return c.errors
N = lambda l, x: ("name", l, x)
PROG = [
 ("fn", 1, "count", [("a", "[int]"), ("k", "int")], "int", [
    ("var", 2, "n", None, ("num", 2, 0)),
    ("var", 3, "i", "int", ("num", 3, 0)),
    ("while", 4, ("bin", 4, "<", N(4, "i"), ("call", 4, "len", [N(4, "a")])), [
        ("if", 5, ("bin", 5, "==", ("index", 5, N(5, "a"), N(5, "i")), N(5, "k")),
            [("assign", 5, N(5, "n"), ("bin", 5, "+", N(5, "n"), ("num", 5, 1)))], None),
        ("assign", 6, N(6, "i"), ("bin", 6, "+", N(6, "i"), ("num", 6, 1)))]),
    ("return", 7, N(7, "n"))]),
 ("fn", 9, "broken", [("x", "int")], "bool", [
    ("var", 10, "ok", "bool", ("num", 10, 1)),
    ("if", 11, N(11, "x"), [("return", 11, ("bool", 11, True))], None),
    ("assign", 12, ("index", 12, N(12, "x"), ("num", 12, 0)), ("num", 12, 5)),
    ("expr", 13, ("call", 13, "count", [N(13, "x")])),
    ("var", 14, "y", None, ("bin", 14, "+", N(14, "ok"), ("bool", 14, True)))]),
]
errors = Checker(PROG).check(PROG)
in_count = [e for e in errors if int(e.split()[1].rstrip(":")) < 9]
print("count:", "no errors" if not in_count else in_count)
for e in errors: print("error:", e)

count: no errors
error: line 10: 'ok' declared bool but initialized with int
error: line 11: if condition must be bool
error: line 12: cannot index a value of type int
error: line 13: count expects 2 argument(s), got 1
error: line 14: operator '+' needs int operands, got bool and bool
error: line 9: function 'broken' may finish without returning a bool

The first function checks cleanly: n is inferred to be int from its initializer, the comparison with len(a) is well typed, and the function ends with a return. The second contains six different mistakes, each with a precise message: a boolean variable initialized with an integer, an integer used as a condition, indexing an integer, a call with the wrong number of arguments, adding a boolean to a boolean, and a function that may end without returning. Note that the addition on line 14 produces only one error even though ok was the source of an earlier one: the checker is not confused by its own recovery.

Type equivalence and subtyping

Deciding whether two types are the same is easy for Tern's few built-in types but subtle in general. Under structural equivalence, two types are equal if they have the same structure: two record types with the same field names and types are interchangeable. Under name equivalence, each declared type is distinct even if its structure is identical, so a Celsius type and a Fahrenheit type, both wrapping a float, cannot be confused. C uses name equivalence for structs, Go and TypeScript use structural typing for interfaces, and most functional languages are structural. Subtyping adds a further relation: if S is a subtype of T, a value of type S can be used where a T is expected. In object-oriented languages a subclass is a subtype of its superclass; the checker must then compute subtype relations rather than test equality, and function types are contravariant in their parameters (CMPUT-325 lesson 8). Implicit conversions, such as C's integer promotions or Java's widening from int to long, are a related feature: the checker inserts explicit conversion nodes into the AST so that code generation sees exactly what to compute.

Overloading and resolution

Many languages let one name denote several functions or operators distinguished by type, a feature called ad hoc polymorphism or overloading. In Java and C++, the checker chooses among overloaded methods by comparing argument types with parameter types, preferring exact matches over conversions, and reporting ambiguity when no single best candidate exists; the C++ rules for this occupy dozens of pages of the standard. Operators are commonly overloaded: + means integer addition, floating-point addition and string concatenation in Java, and the type checker records which one each occurrence means, typically by annotating the AST node, so that code generation emits the correct instruction. Rust's traits and Haskell's type classes provide overloading in a more principled way, resolved by finding the trait implementation for the argument types.

Type inference

Annotating every variable is tedious, and in languages with rich types such as generic collections, closures and iterators, the annotations would dwarf the code. Type inference computes types the programmer omitted. Local inference, as in var x = e, needs only the forward synthesis already present in the checker. More powerful inference treats each unknown type as a variable, collects equations between types from the program's operations, and solves them by unification, the algorithm Robinson published in 1965 for automated theorem proving. Unifying two types makes them equal by binding type variables: unifying t0 with int binds t0, unifying two variables links them, and unifying int with bool fails with a type error. Each binding is recorded in a substitution, and lookups follow chains of bindings to the final type. Real implementations add an occurs check, refusing to bind t to a type containing t (which would mean an infinite type), and use a union-find structure to make binding nearly constant time.

# Type inference by unification for Tern functions whose parameter types
# are omitted. Each unknown type is a variable; every operation adds an
# equation; unification solves the equations or reports a clash.
import itertools
fresh = (f"t{i}" for i in itertools.count())
class TypeError_(Exception): pass
def resolve(t, s):
    while t in s: t = s[t]
    return t
def unify(a, b, s, why):
    a, b = resolve(a, s), resolve(b, s)
    if a == b: return
    if a.startswith("t"): s[a] = b; return            # bind a variable
    if b.startswith("t"): s[b] = a; return
    raise TypeError_(f"{why}: cannot unify {a} with {b}")
def infer(fn):
    name, params, body = fn
    env = {p: next(fresh) for p in params}; s = {}; ret = next(fresh); log = []
    def ex(e):
        tag = e[0]
        if tag == "num": return "int"
        if tag == "bool": return "bool"
        if tag == "name": return env[e[1]]
        if tag == "index":
            unify(ex(e[1]), "[int]", s, "indexed value"); unify(ex(e[2]), "int", s, "index"); return "int"
        if tag == "len": unify(ex(e[1]), "[int]", s, "argument of len"); return "int"
        op, l, r = e[0], ex(e[1]), ex(e[2])
        if op in "+-*/%": unify(l, "int", s, f"left of {op}"); unify(r, "int", s, f"right of {op}"); return "int"
        if op in ("<", ">"): unify(l, "int", s, f"left of {op}"); unify(r, "int", s, f"right of {op}"); return "bool"
        if op in ("&&", "||"): unify(l, "bool", s, f"left of {op}"); unify(r, "bool", s, f"right of {op}"); return "bool"
        if op == "==": unify(l, r, s, "operands of =="); return "bool"
    for stmt in body:
        if stmt[0] == "return": unify(ex(stmt[1]), ret, s, "return value")
        elif stmt[0] == "if": unify(ex(stmt[1]), "bool", s, "if condition")
    sig = ", ".join(f"{p}: {resolve(env[p], s)}" for p in params)
    return f"fn {name}({sig}) -> {resolve(ret, s)}"
FUNCS = [
    ("scale", ["a", "i", "k"], [("return", ("*", ("index", ("name", "a"), ("name", "i")), ("name", "k")))]),
    ("both",  ["p", "q", "x"], [("if", ("&&", ("name", "p"), ("==", ("name", "q"), ("name", "p")))),
                                ("return", ("<", ("name", "x"), ("num",)))]),
    ("same",  ["u", "v"],      [("return", ("==", ("name", "u"), ("name", "v")))]),
    ("bad",   ["m"],           [("if", ("name", "m")), ("return", ("+", ("name", "m"), ("num",)))]),
]
for f in FUNCS:
    try: print(infer(f))
    except TypeError_ as e: print(f"fn {f[0]}: type error ({e})")

fn scale(a: [int], i: int, k: int) -> int
fn both(p: bool, q: bool, x: int) -> bool
fn same(u: t9, v: t9) -> bool
fn bad: type error (left of +: cannot unify bool with int)

The inference works backwards from uses: in scale, indexing determines that a is an integer array and i an integer, and multiplication determines k. In both, the condition forces p to be bool, and the comparison q == p then forces q to have the same type. The function same is interesting: nothing determines what u and v are, only that they are equal, so their types remain the unbound variable t9 (the exact name depends on numbering). A Hindley–Milner system, as in OCaml, Haskell and the Algorithm W implemented in CMPUT-325, would generalize this into a polymorphic type, roughly for all t, (t, t) → bool, so that same could be used at several types. The last function is rejected because m is used both as a condition and as an operand of +, which requires it to be both bool and int.

Hindley–Milner inference infers the most general type of every expression in a pure functional language without any annotations, but it does not extend to every language feature: subtyping, overloading and higher-rank polymorphism make complete inference undecidable or impractical. Mainstream languages therefore use bidirectional type checking, which combines synthesis (computing an expression's type from its parts) with checking (pushing an expected type down into an expression). An expected type flows from a declaration into a closure's parameters, for example, so that in Rust, Swift, Kotlin, Scala and TypeScript, programmers annotate function signatures and the compiler infers the types of local variables, closure parameters and generic arguments. Rust's inference works within each function body using unification, which is why a variable's type can be determined by how it is used several lines later.

What types give the code generator

After type checking, every expression in the AST carries a type, and code generation depends on it. An int + int becomes a 64-bit integer add on RISC-V (add, or addw for 32-bit values, as CMPUT-229 lesson 5 shows), while a floating-point addition would be fadd.d with different registers. Types determine sizes and alignments for laying out stack frames and data structures (lesson 9), whether a comparison is signed or unsigned (blt versus bltu), and whether a value is a pointer that the garbage collector must trace. In languages with generics, the compiler either generates a specialized copy of a generic function for each type it is used with (monomorphization, used by C++ templates and Rust), or a single copy that handles all types uniformly by boxing values behind pointers (Java's erasure, OCaml), trading code size against speed.

Worked examples