A Type Checker

The previous chapter typed expressions built from literals, operators, and if. A program also names things, and its functions take parameters whose types it may not write down. This one prints total: 80. price and label are bound by let; double is a lambda whose parameter n carries no type annotation; to_string is the prelude’s conversion of a value to its text:

fn main() {
    let price = 40;
    let label = "total: ";
    let double = |n| n * 2;
    println(label ++ to_string(double(price)));
}

Two shorter programs are rejected before they run, each with the same message:

fn main() {
    let xs = [];
    println(len(xs));     // the type of this expression cannot be determined
}

fn main() {
    let id = |x| x;
    println(1);           // the type of this expression cannot be determined
}

The programs raise these questions:

• What type does price have where it is used? The rules so far type a literal and an operator. price is a name, and its type was settled two lines earlier.
• What type does n have? Nothing annotates it. The body n * 2 says something about it, and the call double(price) says what is passed to it, but the lambda is checked before the call is reached.
• When does a program not say enough? [] is a list of something, and |x| x returns whatever it is given. What would a checker need to know to give either one a type, and where would it look?

The rules of Appendix D answer the first question directly. The second and third are about how a program computes a type that no rule hands it, and the method came from automated theorem proving.

Solving for types

J. A. Robinson’s “A Machine-Oriented Logic Based on the Resolution Principle” (1965) is a method for proving theorems by machine, and at its centre is a procedure for making two logical expressions identical by substituting for their variables. §5.7 defines the idea: “θ is said to unify A, or to be a unifier of A, if Aθ is a singleton”, that is, if applying the substitution θ to every expression in the set A leaves only one expression. §5.8 gives “the Unification Algorithm”. It finds the first position at which the expressions disagree and, in its third step, substitutes for a variable there, with a condition: “If V_k is a variable, and does not occur in U_k, set σ_k+1 = σ_k{U_k/V_k}, add 1 to k, and return to step 2. Otherwise, terminate.” The clause “and does not occur in U_k” is what is now called the occurs check.

Robin Milner’s “A Theory of Type Polymorphism in Programming” (1978), whose guarantee the previous chapter quoted, brought the procedure to types. §4.1: “𝒲 is based on the unification algorithm of Robinson [14].” Milner’s algorithm 𝒲 gave each unknown type a variable and solved the equations that the program’s operations imposed on them. He credited the idea to the logician Roger Hindley, who had derived types for terms of combinatory logic: “Hindley appears to have been the first to notice that the Unification Algorithm of Robinson [14] is appropriate to this problem.”

Benjamin Pierce and David Turner’s “Local Type Inference” (2000) asked how much inference programmers need. Their answer was that “it is acceptable to require annotations on the bound variables of top-level function definitions (since these usually provide useful documentation)”, and they recovered the remaining types by passing them between neighbouring nodes of the syntax tree, in two modes, “synthesis mode, where typing information is propagated upward from subexpressions, and checking mode, where information is propagated downward from enclosing expressions.” Their inference was local by design, working “without long-distance constraints such as unification variables”. They did not claim the modes as their invention: “The basic idea of bidirectional checking is well known as folklore.”

Bridger’s checker draws on both. It has Pierce and Turner’s two modes and their annotated top-level signatures, and within a declaration it has Milner’s inference variables, solved by Robinson’s procedure.

Typing in a context

A variable’s type depends on where it appears, as its value did. The evaluator answered “what is x?” while the program ran, with the environment $\rho$, which maps each name in scope to a value. The checker answers it before the program runs, with a typing context $\Gamma$, which maps each name in scope to a type. The judgment is now the one Appendix D writes,

$$\Gamma ⊢e:\tau$$

read in context $\Gamma$, expression $e$ has type $\tau$. The rules of the previous chapter carry $\Gamma$ through unchanged; a literal’s type does not depend on it. A variable has the type its binding gave it, and a let extends the context for the rest of its block, as $\text{E-Let}$ extended the environment:

$$\frac{x:\tau \in \Gamma }{\Gamma ⊢x:\tau }(\text{T-Var})\frac{\Gamma ⊢e_1:{\tau }_1\Gamma ,x:{\tau }_1⊢\{rest\}:\tau }{\Gamma ⊢\{\text{let}x=e_1;rest\}:\tau }(\text{T-Let})$$

$\Gamma ,x:{\tau }_1$ is $\Gamma$ with x bound to ${\tau }_1$, shadowing any earlier x, so a block that rebinds x as a String gives the inner x that type and leaves the outer one an Int outside the block. In the opening program $\text{T-Let}$ binds price : Int and label : String, and $\text{T-Var}$ reads them back at their uses.

The checker builds $\Gamma$ from the program text, before anything runs, and it can do so because Bridger’s scope is lexical: the binding a name refers to is fixed by where the name is written. As Static vs. Dynamic Scope observed, a dynamically scoped name would get its binding from whichever caller was running, and no context built from the text could say what type it had.

$\Gamma$ also carries the enclosing function’s return type, ${\tau }_{ret}$, so that a return can be checked against it. Because control leaves at a return, the expression itself produces no value where it stands, and the rule lets it have any type at all; that is what lets return 0 sit in one branch of an if whose other branch is a String:

$$\frac{\Gamma ⊢e:{\tau }_{ret}(\Gamma )}{\Gamma ⊢\text{return}e:\tau }(\text{T-Return})$$

The reference cells and loops of Part IV have rules of the same kind: ref e has type $\text{ref}⟨\tau ⟩$ when e has type $\tau$, deref undoes it, an assignment and a loop have type (), and a for binds its variable at the list’s element type for its body. The reference gives each.

Function types

A function value has a type that records what it takes and what it gives back. A lambda is typed by typing its body in a context extended with its parameters, and a call is typed by matching its arguments against the parameters of its callee’s type:

$$\frac{\Gamma ,x_1:{\tau }_1,\dots ,x_n:{\tau }_n⊢e:\tau }{\Gamma ⊢\lambda x_1\dots x_n.e:\text{fn}({\tau }_1,\dots ,{\tau }_n)\to \tau }(\text{T-Lam})$$

$$\frac{\Gamma ⊢e_0:\text{fn}({\tau }_1,\dots ,{\tau }_n)\to \tau \Gamma ⊢e_i:{\tau }_i(1\le i\le n)}{\Gamma ⊢e_0(e_1,\dots ,e_n):\tau }(\text{T-App})$$

(The rules write $\lambda x_1\dots x_n.e$ for Bridger’s |x1, …, xn| e, as the reference does, and the reference’s $\text{T-Lam}$ also sets ${\tau }_{ret}$ to $\tau$ for a return inside the lambda.) The opening program’s double gets $\text{fn}(\text{Int})\to \text{Int}$, and $\text{T-App}$ then accepts double(price) because price : Int.

The types in this chapter are monomorphic: each function type has particular types in it, and a lambda has one of them. The types a function written once can take at many types, and the top-level declarations whose signatures make them possible, are the subject of the next chapter.

From rules to an algorithm

$\text{T-Lam}$ does not say where ${\tau }_1$ comes from. Read as a rule, it says that if some ${\tau }_1$ makes the body well-typed, the lambda has a function type with ${\tau }_1$ in it, and it is silent about how to find one. For |n| n * 2 the right choice is Int, but the rule only confirms the choice once it has been made. A checker is a program and cannot guess. It has two ways to proceed without guessing: take the type from the surrounding context when the context has one, or give the unknown type a name and solve for it from what the rest of the declaration requires.

Checking and inferring

Some positions in a program already know what type they need. The body of fn f(c: Bool) -> Int needs an Int; the argument of a call to a function whose parameter is an Int needs an Int; the else branch of an if needs the type the then branch had. Other positions know nothing in advance: the right-hand side of an unannotated let, or a lambda whose type is about to be discovered.

A bidirectional checker splits the judgment into two modes, one for each kind of position. $\Gamma ⊢e\Rightarrow \tau$ reads $e$ synthesizes $\tau$: the checker works out a type from $e$ alone. $\Gamma ⊢e\Leftarrow \tau$ reads $e$ checks against $\tau$: the type is given, and the checker confirms that $e$ has it. A variable synthesizes the type $\Gamma$ gives it. A call synthesizes its type from its callee and checks each argument against the parameter type it is passed to. A lambda checks against a function type, taking its parameter types from it:

$$\frac{x:\tau \in \Gamma }{\Gamma ⊢x\Rightarrow \tau }(\text{Syn-Var})\frac{\Gamma ⊢e_0\Rightarrow \text{fn}({\tau }_1,\dots ,{\tau }_n)\to \tau \Gamma ⊢e_i\Leftarrow {\tau }_i}{\Gamma ⊢e_0(e_1,\dots ,e_n)\Rightarrow \tau }(\text{Syn-App})$$

$$\frac{\Gamma ,x_1:{\tau }_1,\dots ,x_n:{\tau }_n⊢e\Leftarrow \tau }{\Gamma ⊢\lambda x_1\dots x_n.e\Leftarrow \text{fn}({\tau }_1,\dots ,{\tau }_n)\to \tau }(\text{Chk-Lam})$$

In $\text{Chk-Lam}$ the parameter types are inputs, read off the function type the lambda is checked against, and nothing is guessed. One more rule connects the modes. An expression that synthesizes a type checks against any type equal to it:

$$\frac{\Gamma ⊢e\Rightarrow {\tau }^{\prime }{\tau }^{\prime }=\tau }{\Gamma ⊢e\Leftarrow \tau }(\text{Chk-Sub})$$

Bridger’s apply shows a lambda checked against a type its context supplies:

fn apply(f: fn(Int) -> Int, x: Int) -> Int = f(x);

fn main() {
    println(apply(|n| n + 1, 5));                       // 6
}

$\text{Syn-App}$ checks the argument |n| n + 1 against apply’s first parameter type, $\text{fn}(\text{Int})\to \text{Int}$, and $\text{Chk-Lam}$ gives n the type Int from it.

Inference variables

The modes do not cover every case. let double = |n| n * 2; has no type for its right-hand side to check against, so the lambda must synthesize, and synthesis needs a type for n before the body can be typed. A checker that cannot guess n’s type can name it. It gives n a fresh inference variable $\alpha$, a placeholder that stands for a type not yet known, and carries on. Typing the body then produces requirements on $\alpha$:

1. n * 2 is an arithmetic operation, so each operand is checked against Int.
2. n synthesizes $\alpha$, and $\text{Chk-Sub}$ requires $\alpha =\text{Int}$.
3. The requirement is met by solving $\alpha$ as Int. From then on, wherever $\alpha$ appears, it means Int.
4. The body synthesizes Int, so the lambda synthesizes $\text{fn}(\alpha )\to \text{Int}$, which is $\text{fn}(\text{Int})\to \text{Int}$.

double("a") is then rejected at "a", with expected Int, found String: by the time the call is checked, $\alpha$ has been solved, and $\text{Syn-App}$ checks the argument against Int.

The equation in the second step is what $\text{Chk-Sub}$’s premise ${\tau }^{\prime }=\tau$ becomes once types can contain variables. Satisfying it, by choosing types for the variables that make the two sides equal, is unification. It compares two types structurally:

• Two base types unify if they are the same type: Int with Int, Bool with Bool.
• Two types built by the same constructor unify if their parts do, pairwise: two lists if their element types unify; two function types if they take as many parameters, each parameter type unifies with the corresponding one, and the result types unify; tuples and reference types the same way.
• A variable already solved unifies as its solution would.
• An unsolved variable $\alpha$ unifies with a type $\tau$ by being solved as $\tau$.
• Anything else, such as Int with String or a list with a function type, is a mismatch.

The solution unification produces assigns only what the requirements force. Solving $\alpha$ as Int in double follows from n * 2; nothing else would make the body well-typed, and nothing more is assumed.

let xs = []; gives the empty list the type $[\beta ]$ with a fresh $\beta$, since no element says what it holds. In len(xs ++ [1]) the concatenation unifies $[\beta ]$ with $[\text{Int}]$ and solves $\beta$ as Int. In len(xs) nothing does, and when the checker finishes the declaration $\beta$ is still unsolved. The type of [] is then not determined by the program, and Bridger rejects it, asking for an annotation such as let xs: [Int] = [];. let id = |x| x; with no use is the same case: its type is $\text{fn}(\gamma )\to \gamma$, and nothing fixes $\gamma$.

The occurs check

Recursion and higher-order functions promised that this checker would reject self-application with the error cannot construct the infinite type. The smallest case is

fn main() {
    let w = |x| x(x);
    println(1);
}

x gets a fresh variable $\alpha$, and the body’s result a fresh $\beta$. The body calls x, so $\alpha$ must be a function type. The call passes x itself as the argument, so that function type’s parameter is $\alpha$, and unification is asked to solve

$$\alpha =\text{fn}(\alpha )\to \beta$$

Solving $\alpha$ as $\text{fn}(\alpha )\to \beta$ would make every $\alpha$ inside that type stand for $\text{fn}(\alpha )\to \beta$ again, and spelling the solution out would substitute without end: no type written with finitely many fns satisfies the equation. Unification therefore adds one condition to its rule for an unsolved variable. Before solving $\alpha$ as $\tau$, it checks that $\alpha$ does not occur in $\tau$, looking through any variables already solved, and reports an infinite type if it does. This is the occurs check. The M4 evaluator runs the program, since w is never called; the checker rejects it, at x(x).

Bridger’s checker

Bridger’s checker is bidirectional, with inference variables for what neither mode supplies, and the inference it does stays inside one declaration. A function body is checked against the signature its declaration writes, a lambda’s parameter types come from an annotation, from the type it is checked against, or from a fresh variable, and every variable a declaration introduces must be solved by the time the declaration has been checked. No inference variable outlives its declaration, so a type left open in one declaration cannot be fixed by a use in another. The next chapter takes up what the signatures at those boundaries can say.

The checker leaves the program’s AST as the parser produced it. The type of each expression goes into a separate table, the TypeMap, keyed by the expression’s span; the determination rule reads it back, tests inspect it, and the evaluator never sees it.

Building it

The checker’s arms are the typing rules, one per form of Expr, as the evaluator’s arms were the evaluation rules. The provided method you fill in is

pub fn check_expr(
    &mut self,
    e: &Expr,
    ctx: &Ctx,
    expected: Option<&Ty>,
) -> Result<Ty, TyError>

and its expected argument is the two modes in one parameter. With Some(ty) the arm checks e against ty; with None it synthesizes. It returns e’s type either way, and records it at e’s span. An arm with no use for an expected type synthesizes one and then unifies it with the expected type, which is $\text{Chk-Sub}$. An arm that has a use for it passes it on: a lambda reads its parameter types from an expected function type, and an if checks its else branch against the type its then branch has.

Ctx is $\Gamma$, and it is built like the environment of Part III: immutable, with extend returning a new context and leaving the old one as it was.

impl Ctx {
    /// The type bound to `x`, searching outward through enclosing scopes.
    pub fn lookup(&self, x: &str) -> Option<Ty>;
    /// Bind `x : ty` in a fresh child scope and return it.
    pub fn extend(&self, x: Name, ty: Ty) -> Ctx;
    /// A lambda body: bindings stay visible, `return` targets `ret`
    /// (`self_ty` is for methods, Part IX).
    pub fn enter(&self, ret: Option<Ty>, self_ty: Option<Ty>) -> Ctx;
    /// The enclosing function's return type, if inside one.
    pub fn ret(&self) -> Option<Ty>;
}

The inference variables are provided too. fresh_meta makes one, solve records a solution, resolve replaces every solved variable in a type by its solution, and record puts a type in the TypeMap:

impl Checker {
    pub fn fresh_meta(&mut self) -> Ty;
    pub fn solve(&mut self, id: u32, ty: Ty);
    pub fn resolve(&self, ty: &Ty) -> Ty;
    pub fn record(&mut self, span: Span, ty: Ty);
}

The arms, and unify with its occurs check, are yours. In the starter each is a milestone hole naming the rules it implements:

// M5: one arm per typing rule, over the M1–M4 expressions
Expr::Var(..)    => todo_m5!("T-Var / T-Self"),
Expr::Block(..)  => todo_m5!("T-Block / T-Let / T-Seq"),
Expr::If(..)     => todo_m5!("T-If"),
// … and the rest, T-Lam and T-App among them

pub fn unify(&mut self, a: &Ty, b: &Ty, span: Span) -> Result<(), TyError> {
    todo_m5!(
        "unify (structural agreement; solves TyKind::Meta with an occurs check)"
    )
}

Where a rule needs two types to agree, the arm calls unify rather than comparing them with ==, since either may hold a variable that the comparison has to solve.

The provided driver walks the program’s declarations and calls check_expr on each body: a fn against its declared return type, in a context binding its parameters. After each declaration it asks that every type recorded for it be fully determined, which is where let xs = []; is rejected. Writing the arms and unify is Milestone M5.

Where errors are reported

The order in which a bidirectional checker visits a declaration decides where a mismatch is reported. In

fn f(c: Bool) -> Int = if c { 1 } else { "one" };

the body is checked against Int, the if passes the type on to its branches, and the error points at "one": expected Int, found String. With apply from above,

println(apply(|n| n ++ "!", 5));

is rejected at n, with expected String, found Int. $\text{Chk-Lam}$ gave n the type Int from apply’s parameter, and ++ then needed a String. A checker that synthesized the lambda’s type first would have found $\text{fn}(\text{String})\to \text{String}$ and reported the mismatch at the whole lambda, against apply’s parameter type.

The design space

Where the types go

Bridger’s checker answers yes or no and leaves its types in a side table. A checker can keep less: one that only validates computes each type, uses it to check the parent, and discards it, which is enough to accept or reject but gives later passes nothing to read. It can also keep more. It can write each type into the AST node it belongs to, so that a later pass reads a node’s type from the node, at the cost of an AST whose shape changes between the parser and the checker. Or it can elaborate the program into a separate typed representation, a new tree in which every node carries its type and constructs the types have resolved are made explicit. Compilers take the last route, and generate code from the typed representation; the types are discarded when the machine code is produced, which is why a compiled program carries no types at run time. Bridger’s evaluator needs nothing from the checker in this part, and the side table keeps the AST the evaluator walks the same before and after the checker arrives. Part IX is where the checker first hands the evaluator something it decided, a method chosen by type.

How much is inferred

Languages place the line between written and inferred types differently. Pascal and the C of the 1970s inferred nothing beyond the type of an operator’s result: every variable carried a declared type. ML infers the types of whole programs, top-level functions included. Bridger, like Rust and Pierce and Turner’s proposal, asks for types on top-level signatures and infers the types within a body. The written signatures are documentation a reader can rely on, and they keep each declaration’s inference small and its errors close to their cause; the cost is annotations that a whole-program inference would not need. The next chapter describes what Bridger’s choice leaves out.

Unification elsewhere

Unification is not specific to types. It solves equations between any terms built from constructors and variables, and Part VII uses it again, on the facts and rules of Bridger’s relations, where the variables stand for values instead of types.

Further reading

Bidirectional checking: David Christiansen’s “Bidirectional Typing Rules: A Tutorial” (2013) splits the typing rules of a small typed λ-calculus into checking and synthesis judgments and turns each rule into a case of a recursive function, which is the shape of check_expr. Jana Dunfield and Neel Krishnaswami’s survey “Bidirectional Typing” (2021) covers the design choices bidirectional systems make, for many type systems, and ends with historical notes on where the idea came from. Pierce and Turner’s “Local Type Inference” (2000) develops the two modes for a language with polymorphism and subtyping.

Unification: Robinson’s paper (1965) states the algorithm and proves that it finds a most general unifier, in the vocabulary of first-order logic. Pierce’s Types and Programming Languages (MIT Press, 2002) treats type inference by unification in chapter 22, where a program’s typing constraints are first collected and then solved.

Concept checks