Chapter 4: Simply Typed Lambda Calculus

New files

• src/types.rs

Changed files

• src/ast.rs
• src/eval.rs
• src/lexer.rs
• src/lib.rs
• src/main.rs
• src/names.rs
• src/normal.rs

Motivation

Our evaluator will happily try to run 1 True. It eventually discovers that an integer isn’t a function, but we didn’t need to run the program to spot that mistake. Could the compiler catch it for us?

A type checker does exactly this sort of reasoning. A function type tells us what a function accepts and what it returns. We check a call by comparing those types with the argument we’re about to pass. The rules are small enough to write down, and the Rust implementation will follow them closely.

For now we’ll ask the programmer to annotate lambda parameters. This gives us a clear starting point. In Chapter 6 we’ll teach the compiler to work out types for itself, including types that work for many different kinds of values.

The Language, Now

Types are Int, Bool, and arrows. Arrows associate right, so Int -> Bool -> Int means Int -> (Bool -> Int). An arrow on the left needs parentheses.

let choose = \(b : Bool) -> \(x : Int) -> \(y : Int) ->
  if b then x else y
in choose True 10 20

We annotate every lambda parameter, but calls, arithmetic, and scope work as before. Try calling an integer as a function again. This time E0201 comes from the checker, before the evaluator gets involved. We’ve moved the discovery of the mistake earlier in the process.

Theory

The Typed Grammar

The new ingredient is a type on each lambda parameter. First, here are the types we can write. A function’s input and output can themselves be functions.

$$\begin{array}{rlrl}\tau & =\text{Int}& & \text{integers}\\ & \mid \text{Bool}& & \text{booleans}\\ & \mid {\tau }_1\to {\tau }_2& & \text{function type}\end{array}$$

The expressions are familiar from the previous chapter. The annotation in $\lambda x:\tau .e$ tells the checker what it may assume about $x$.

$$\begin{array}{rlrl}e& =x& & \text{variable}\\ & \mid e_1{e}_2& & \text{application}\\ & \mid \lambda x:\tau .e& & \text{typed abstraction}\\ & \mid n& & \text{integer literal}\\ & \mid \text{True}\mid \text{False}& & \text{boolean literal}\\ & \mid \text{let}x=e_1\text{in}{e}_2& & \text{local binding}\\ & \mid \text{if}{e}_1\text{then}{e}_2\text{else}{e}_3& & \text{conditional}\\ & \mid -e& & \text{integer negation}\\ & \mid e_{1}op{e}_2& & \text{binary operation}\end{array}$$

As before, $n$ is an integer and $op$ is one of +, -, *, /, ==, <, or <=. We omit source spans and the parser’s recovery placeholder. This grammar describes what we can parse. The typing rules below decide which of those expressions we can safely run. For example, 1 True still has the shape of an application, but it won’t have a typing derivation.

Typing and Safety

A typing environment maps names to types. Reading a variable looks up its nearest binding. A lambda extends that environment while checking its body. Application checks its argument against the function’s domain (Pierce 2002).

$$\frac{\Gamma ,x:\tau ⊢e:\sigma }{\Gamma ⊢(\mathsf{lambda}x:\tau .e):\tau \to \sigma }\text{(Abs)}$$

$$\frac{\Gamma ⊢f:\tau \to \sigma \Gamma ⊢a:\tau }{\Gamma ⊢fa:\sigma }\text{(App)}$$

The condition of an if has type Bool. Both branches have the same type. Arithmetic takes integers, while comparisons return booleans. A let checks its right-hand side before extending the environment, so it remains non-recursive. There is no implicit quantification. An identity annotated Int -> Int cannot also accept Bool.

Two useful ideas explain what we’ve gained. Preservation says that taking an evaluation step doesn’t change an expression’s type. If we start with an Int expression, reducing it shouldn’t suddenly produce a function. The main proof step for a lambda call shows that substituting a correctly typed argument keeps the body’s type intact. This is the substitution lemma.

Progress says that a closed, well-typed expression is either a value or can take a step. We won’t reach a nonsensical instruction such as calling 42. Our division primitive needs a small qualification, since division by zero can still report a runtime error. Types catch this language’s shape mistakes. They don’t promise that every computation succeeds. Pierce develops the proofs behind these claims (Pierce 2002).

Implementation

types.rs represents arrows recursively and prints them with the required parentheses. There are no metavariables or substitution maps yet.

#![allow(unused)]
fn main() {
/// Simple types have no variables, schemes, or implicit quantification.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum Type {
    Int,
    Bool,
    Arrow(Box<Type>, Box<Type>),
}

impl Type {
    pub fn arrow(domain: Self, codomain: Self) -> Self {
        Self::Arrow(Box::new(domain), Box::new(codomain))
    }
}

impl fmt::Display for Type {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Int => write!(f, "Int"),
            Self::Bool => write!(f, "Bool"),
            Self::Arrow(a, b) => {
                if matches!(**a, Self::Arrow(..)) {
                    write!(f, "({a})")?;
                } else {
                    write!(f, "{a}")?;
                }
                write!(f, " -> {b}")
            }
        }
    }
}
}

The grammar uses right recursion for the arrow’s codomain. The AST’s lambda variant now stores a Type beside the parameter name, so a successfully parsed lambda always has its annotation.

Type: Type = {
    <a:TypeAtom> "->" <b:Type> => Type::arrow(a, b),
    TypeAtom,
};
TypeAtom: Type = {
    "Int" => Type::Int, "Bool" => Type::Bool, "(" <Type> ")",
};

The checker mirrors the typing rules. Its environment is a stack, searched from the innermost binding outward. A scope is popped even if checking its body returns an error. Application first finds the function type, then checks the argument, giving a useful error at the argument rather than at the whole call.

#![allow(unused)]
fn main() {
fn infer(
    expr: &Expr,
    env: &mut Vec<(String, Type)>,
) -> Result<Type, Diagnostic> {
    match &expr.kind {
        Kind::Int(_) => Ok(Type::Int),
        Kind::Bool(_) => Ok(Type::Bool),
        Kind::Var(name) => env
            .iter()
            .rev()
            .find(|(n, _)| n == name)
            .map(|(_, ty)| ty.clone())
            .ok_or_else(|| {
                Diagnostic::new(
                    "E0101",
                    format!("unbound variable {name}"),
                    expr.span.clone(),
                )
            }),
        Kind::Lam(name, parameter, body) => {
            env.push((name.clone(), parameter.clone()));
            let result = infer(body, env);
            env.pop();
            Ok(Type::arrow(parameter.clone(), result?))
        }
        Kind::App(function, argument) => {
            let function_ty = infer(function, env)?;
            let Type::Arrow(domain, codomain) = function_ty else {
                return Err(mismatch(
                    function,
                    "a function type",
                    &function_ty,
                ));
            };
            expect(argument, infer(argument, env)?, &domain)?;
            Ok(*codomain)
        }
        Kind::Let(name, value, body) => {
            let ty = infer(value, env)?;
            env.push((name.clone(), ty));
            let result = infer(body, env);
            env.pop();
            result
        }
        Kind::If(condition, yes, no) => {
            expect(condition, infer(condition, env)?, &Type::Bool)?;
            let ty = infer(yes, env)?;
            expect(no, infer(no, env)?, &ty)?;
            Ok(ty)
        }
        Kind::Neg(value) => {
            expect(value, infer(value, env)?, &Type::Int)?;
            Ok(Type::Int)
        }
        Kind::Binary(op, left, right) => {
            expect(left, infer(left, env)?, &Type::Int)?;
            expect(right, infer(right, env)?, &Type::Int)?;
            Ok(match op {
                Op::Eq | Op::Lt | Op::Le => Type::Bool,
                _ => Type::Int,
            })
        }
        Kind::Error => Err(Diagnostic::new(
            "E0002",
            "unrecovered syntax error",
            expr.span.clone(),
        )),
    }
}
}

The small expect helper compares two simple types structurally. On a mismatch, it reports both the expected and found types at the expression’s byte span. Ariadne renders the source excerpt. This standalone checker stops at its first type error. The earlier lexical and scope passes still collect their errors.

The evaluator ignores annotations and retains the closure representation from Chapter 3. Substitution, normal-order reduction, and de Bruijn conversion carry types through their lambda cases. This lets the preservation tests check every intermediate term, and keeps annotated terms distinct in nameless dumps.

Running It

$ cd crates/ch04_stlc
$ cargo run -q -- run tests/programs/typed-return.fun
42
$ cargo run -q -- dump --pass=types tests/programs/church.fun
Int
$ cargo run -q -- repl
STLC: :quit, :type EXPR, :parse EXPR, :trace EXPR.
stlc> :type \(f : Int -> Bool) -> \(x : Int) -> f x
(Int -> Bool) -> Int -> Bool
stlc> :quit

check checks without evaluating. Both execution engines check types first. :trace also rejects ill-typed input before displaying reductions. A successful check of 1 / 0 is expected. Its type is Int, even though execution fails.

Exercises

1. Easy. Derive the type of the choose example using the abstraction rule.
2. Easy. Explain why (Int -> Bool) -> Int needs its parentheses.
3. Medium. Write an application with a well-typed function and an argument of the wrong type. Check the diagnostic’s span.
4. Hard. State the substitution lemma for this calculus, including the condition on the replacement term, and work through the lambda case.

Further Reading

Pierce gives the formal progress and preservation proofs (Pierce 2002). Damas and Milner motivate the next step beyond simple types: principal type schemes and polymorphic let (Damas and Milner 1982). Takenobu Tani’s Type Introduction Illustrated for Casual Haskellers (pdf / github) draws the same ideas as pictures, from simple types up to the extensions GHC adds.