Chapter 1: Introduction

Motivation

I started writing this text in 2014 because the introduction I needed did not exist. The material I found on functional compilers was often dense and hard to approach, or written for an academic audience rather than people building software in industry. I wanted someone to walk me through a working compiler and explain the ideas as we needed them.

I slowly filled in the gaps in my own knowledge, but there was no reason others should have to take the same slow route. In the spirit of “be the change you want to see,” I decided to write the introduction I had been looking for. This book is my way of lowering the ladder for the next person.

We’ll build Fun, a strict functional language with inferred types, algebraic data, nominal records, and type classes. And building Fun is going to be fun! We’ll write it in Rust and take it all the way to native code through LLVM. Along the way we’ll build interpreters that let us run programs before we have a code generator, and check our translations as we go. The Haskell Report gives us a starting point for syntax and typing (Simon Marlow 2010).

A compiler becomes easier to understand when each transformation has a small input language and a small output language. The early chapters study parsing, evaluation, and inference separately. From Chapter 7 onward each crate is a complete snapshot of the same compiler. Read a chapter together with its diff. Run an earlier snapshot whenever you want to revisit a simpler implementation.

Tool Setup

Use Apple Silicon macOS, or Linux on x86-64 or AArch64. We need Rust and Cargo to build the chapters, just to run the repository recipes, a C compiler and Boehm GC for the runtime, and LLVM 22 for native compilation and the JIT. The book has a separate toolchain, installed by just bootstrap.

macOS

Install Apple’s command-line development tools and follow the Homebrew installation instructions if brew is not already available. Then install the system dependencies:

xcode-select --install
brew install git python just llvm@22 bdw-gc pkg-config
export LLVM_SYS_221_PREFIX="$(brew --prefix llvm@22)"
export GC_LIB_DIR="$(brew --prefix bdw-gc)/lib"

Wait for the command-line tools installer to finish before running the build. Keep the two exports in your shell configuration if you want them in later terminal sessions. llvm@22 is intentional. An unversioned LLVM package can select a different ABI from the one used by our Rust bindings.

Ubuntu

These commands target Ubuntu 26.04 LTS, the current LTS when this edition was written. They also work with the supported Ubuntu 24.04 CI environment. Install the common tools, then use the official LLVM package installer to select version 22 explicitly:

sudo apt update
sudo apt install -y build-essential git curl wget ca-certificates \
  gnupg lsb-release software-properties-common python3 pkg-config \
  libgc-dev libssl-dev just
curl -fsSLo /tmp/wyah-llvm.sh https://apt.llvm.org/llvm.sh
sudo bash /tmp/wyah-llvm.sh 22
sudo apt install -y llvm-22-dev libpolly-22-dev
export LLVM_SYS_221_PREFIX=/usr/lib/llvm-22

The versioned LLVM prefix belongs in your shell configuration for later builds. The distribution’s default Rust package need not match the book’s pinned compiler, so install Rust through rustup next.

Rust and the Repository

Follow the canonical Rust installation guide. On either platform, its rustup installer is:

curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
. "$HOME/.cargo/env"
git clone https://github.com/sdiehl/write-you-a-haskell.git
cd write-you-a-haskell
rustup show
rustc --version
cargo --version

Inside this checkout, rust-toolchain.toml selects Rust 1.99.0 with Clippy and rustfmt. Rustup installs the selected toolchain when needed. The rustup book explains how directory toolchains work. just is a command runner, not another build system. Its installation guide lists alternatives to the system packages above.

Now build a small chapter and the complete workspace:

cargo run -p ch02_calc -- repl
just build
cargo fmt --all -- --check
cargo clippy --workspace --all-targets -- -D warnings

For HTML and PDF, install the pinned book tools locally:

just bootstrap
just book
just pdf

Bootstrap installs mdBook, its preprocessors, Pandoc, and Typst under .tools. The just recipes put .tools/bin on PATH. Fonts are already vendored in the repository. Open book/build/html/index.html or build/write-you-a-haskell.pdf. The published copies are the HTML at https://sdiehl.github.io/write-you-a-haskell/ and the PDF beside it at https://sdiehl.github.io/write-you-a-haskell/write-you-a-haskell.pdf, which is also the asset on the repository’s latest GitHub release. The full compiler tests run with cargo test --workspace and include long recursion and allocation regressions.

Nix Alternative

With Nix installed, the flake supplies the pinned Rust toolchain, LLVM 22, Boehm, a C compiler, and development tools for Apple Silicon macOS and both Linux architectures:

nix --extra-experimental-features 'nix-command flakes' develop
just build
just bootstrap
just pdf

The lock file fixes the package inputs. The shell sets the LLVM and GC paths, so it replaces the platform package-installation steps above. Bootstrap still installs the book’s exact tool versions into .tools.

Why Rust

When I first wrote this book in the mid-2010s, Haskell was an appealing way to explain a compiler. Algebraic data types, pattern matching, and a compact syntax made the transformations almost read like their mathematical definitions. But getting from those definitions to a complete native compiler already meant relying on libraries whose support was thin. In my experience, that maintenance problem has grown worse with time.

I still love Haskell’s surface language. I no longer consider it a good practical choice for building the compiler in this book. A compiler needs maintained bindings, diagnostics, testing tools, packaging, and a predictable runtime as well as elegant tree transformations. Implicit laziness also puts extra distance between the program I write and its allocation and evaluation behavior. Those costs matter when a compiler must process large inputs reliably.

Rust is my choice for this edition because of its much broader ecosystem and sustained investment in production tooling. It offers enums and pattern matching for our intermediate languages, explicit ownership for their storage, and direct access to LLVM and the native runtime. Cargo makes the chapter snapshots easy to build and test together. I want readers to spend their time learning compilation, with a toolchain they can continue using after the last chapter.

For this project, Rust is the best balance of expressive implementation code and practical engineering. Perhaps there will be an OCaml edition one day. For now, Haskell remains a language worth studying, while Rust is the language I want to build in. The original Haskell edition is preserved in the repository under the haskell-edition tag.

Why not laziness?

Haskell’s strongest lessons survive without making every ordinary computation potentially lazy. Algebraic data, pattern matching, principal types, purity, and type classes are all worth keeping. Fun brings them together with call-by-value. Arguments are computed before a call, constructor fields before construction, and ordinary bindings before their bodies. This gives the reader a direct account of when work happens and where storage is needed.

I do not see implicit laziness as a productive default for a new language. A suspended expression may retain its environment long after its source binding looks finished. Forcing it can move both work and failure far from their cause. Sharing can avoid repeated work, but it introduces its own allocation and update protocol. Strictness analysis can recover efficient execution in many cases, yet that is substantial machinery to reconstruct a cost model we could have made explicit from the start. Chapter 5 studies the tradeoff in executable form.

Delayed computation is still useful. My preferred foundation for making it opt-in is call-by-push-value (CBPV). It separates values from computations. A computation can produce a value, and a value can hold a suspended computation. Explicit thunk and force operations mark the boundary. Both call-by-value and call-by-name can be expressed through these smaller operations (Levy 2001). The programmer or compiler can therefore specify where delay belongs instead of inheriting it everywhere.

CBPV does not by itself memoize a suspension. Call-by-need additionally requires sharing and an update that remembers the result. Forcing an ordinary thunk twice can run its computation twice. That distinction is precisely why I prefer this foundation for exploring laziness. Fun itself remains a strict call-by-value language. It implements neither CBPV nor lazy values. An explicit account of delay is a direction for a later language, beyond this book’s compiler.

Chapter roadmap

The tables below describe the complete book. Linked titles open each chapter. Chapters 2–6 are standalone languages. Chapters 7–24 are successive snapshots of Fun. Each row names the piece you will build, rather than a list of prerequisites.

Part I: Foundations

Part II: Frontend

Part III: Backend

Appendices collect the grammar, typing rules, intermediate representations, runtime ABI, and diagnostic index. A bibliography closes the book.

How We Will Build It

We begin with a calculator. It is small enough that we can follow an expression from the text we type to the answer it produces. We then build a few small languages to explore functions, evaluation, and types separately. Each has a complete Rust implementation you can run and change. You do not need to understand a whole compiler before you can experiment with one part of it.

In Chapter 7, those ideas come together in Fun. From there, each chapter starts with the previous chapter’s compiler and adds one piece. Records extend the language, type classes introduce a way to share operations across types, and later chapters teach the compiler to produce native code. Every chapter has its own crate, so you can keep an earlier version open beside the one you are studying.

Read the changes as well as the finished code. Each chapter lists its new and changed source files, with the important ones first. Comparing two snapshots lets you see what a feature actually asks of the compiler. You might need a new syntax node, a typing rule, and a translation into simpler operations. The book includes code from those source files, so the implementation you read is the one you run. Tests carry forward too, helping us check that adding a feature has not broken what already worked.

The theory arrives alongside the problems it helps us solve. We will try a small example, find the question it raises, and introduce enough notation to make the answer precise. You can work through the code and examples first, then return to a rule once you have seen it in action. No prior course in type theory is assumed. Familiarity with Rust enums, pattern matching, borrowing, and Cargo will help you follow the implementations.

Theory

A compiler rewrites a program several times before the computer can run it. The challenge is to change how the program is written while keeping what it does. If your program prints 42, the machine code we produce should also print 42. If it asks for your name before greeting you, compilation must keep those actions in that order.

We will build up those steps one at a time. First we work out how the source text fits together. In 1 + 2 * 3, multiplication belongs inside the addition. Then we check that the operations make sense, so adding a number to a function is caught before the program runs. Later chapters translate the program into simpler forms that are easier to turn into machine code.

How do we know we got a translation right? One useful trick is to write a small interpreter for each form and run the same examples through them. If they give different answers, we have found a compiler bug. Matching answers do not establish that every possible program works, but they give us a practical way to check our work as we go. Along the way, we will also learn how types and rules about evaluation help us reason about programs beyond the examples we can test (Pierce 2002).

Implementation

The repository is part of the book. Each chapter has a crate you can run, take apart, and change. If you’re wondering what a transformation really did, ask the compiler to dump its output and compare it with the input. That habit will tell you more than staring at the implementation and hoping for enlightenment.

We also want to keep the examples working as the compiler grows. testkit runs small programs and checks their output, errors, and exit status. Later it runs the same program through several execution engines. If two engines disagree, we have something concrete to investigate.

#![allow(unused)]
fn main() {
/// The chapter supplies its binary and available engines; the runner owns policy.
pub struct Config<'a> {
    pub binary: &'a Path,
    pub programs: &'a Path,
    pub engines: &'a [Engine],
    pub timeout: Duration,
}
}

xtask handles the repetitive work of copying a chapter and checking its inherited examples. The book itself includes Rust directly from the chapter sources. You can follow an included function into the crate and experiment with the code you’re reading. The HTML and PDF are built from the same chapters.

Running It

Install the pinned book tools with just bootstrap, then run:

$ cargo test --workspace
$ just book
$ just pdf

The HTML is in book/build/html/. The PDF is build/write-you-a-haskell.pdf. Compiler --dump commands start in Chapter 2. There is no compiler pass to dump in Chapter 1.

Further Reading

The Haskell Report is the language reference (Simon Marlow 2010). Pierce introduces the operational and typing judgments we will use (Pierce 2002). Kiselyov connects type generalization with dependency tracking, preparing for Chapter 6 (Kiselyov 2013). When you want to compare our choices with the real thing, Takenobu Tani’s GHC Reading Guide (pdf / github) is a map of the GHC source tree and its pipeline.

Chapter 2: Parsing

New files

• src/lexer.rs
• src/pratt.rs
• src/ast.rs
• src/eval.rs
• build.rs
• src/diagnostic.rs
• src/lib.rs
• src/main.rs

Changed files

None.

Motivation

We read 1 + 2 * 3 and know that the multiplication comes first. The computer gets a string of characters. Before it can calculate anything, we have to teach it how those characters fit together. That’s the parser’s job.

We’ll start with a calculator, small enough to follow all the way from source text to an answer. We’ll build its parser twice. LALRPOP lets us write down a grammar and generates the parsing machinery for us. A Pratt parser puts the operator-handling logic in a short Rust function. Seeing both is a useful way to discover what a parser generator is doing on our behalf.

The Language, Now

A program is one expression. It has decimal integer literals, names, +, -, *, /, unary minus, parentheses, and a non-recursive let.

let x = 7 in (let y = x + 1 in y * y) - x

The binding is visible in its body, not its right-hand side. A nested binding shadows an outer name. Multiplication and division bind above addition and subtraction. All four operators associate left. Unary minus binds above them. The / operator truncates integer division toward zero in this mini-language. Full Fun will reserve / for fractional arithmetic and spell this operation quot.

Theory

There are two plausible trees for 1 + 2 * 3. One adds first and returns 9. The other multiplies first and returns 7. We want the second, so our grammar needs to express that choice. We’ll separate sums, products, and atoms into different rules. A sum can contain a whole product as an operand. Parentheses let us start again from the full expression grammar when we want another grouping.

Choosing a parsing strategy

There isn’t one parsing technique that wins at everything. Some approaches make the whole grammar easy to inspect. Others make it easy to write a little parser directly in the host language. Before choosing, it helps to separate three things we often bundle together. The grammar says what syntax we accept, the algorithm recognizes it, and the API determines how we write the parser.

LR(1) scans left to right and constructs a rightmost derivation in reverse. Its state summarizes the prefix already read. One lookahead token helps decide whether to shift another token or reduce a completed production. The “1” does not limit expressions to one token. The parser’s stack retains arbitrarily deep syntactic context. Left recursion, such as a sum containing a smaller sum, fits this bottom-up process naturally.

LALR(1) merges LR(1) states with the same underlying LR(0) items, combining their lookahead sets. This reduces table size but can introduce conflicts absent from the unmerged grammar. Despite its name, our generator uses LR(1) by default. LALR(1) is an option. See the LALRPOP documentation. A conflict is useful feedback. The grammar needs attention before we can trust its generated parser.

Pratt parsing makes the operator decision local. After reading 1 + 2, the parser compares the following * with the binding power of +. Multiplication belongs inside the right operand, so 1 + 2 * 3 becomes 1 + (2 * 3). For 8 - 3 - 1, the right-operand threshold excludes an equal-strength subtraction, giving (8 - 3) - 1. Prefix and infix uses of - can have different handlers. This is an excellent fit for expressions, but does not by itself specify the structure of a class declaration or a layout block.

Packrat parsing avoids repeated work during backtracking by remembering a rule’s success or failure at each position. It is commonly associated with parsing expression grammars (PEGs), whose alternatives use ordered choice. The first successful alternative wins. Reordering alternatives can therefore change the language. For a fixed grammar with bounded work per memoized entry, this gives linear recognition time and generally linear memo storage. Ordinary left-recursive rules need rewriting or a specialized extension. Ford’s packrat and PEG overview develops these choices.

Parser combinators are a way to write parsers, not one recognition algorithm. A sequencing combinator runs one parser after another. A choice combinator tries alternatives according to its library’s rules. A combinator library may commit, backtrack, or memoize. Its pleasant surface does not automatically give linear time, good recovery, or support for left recursion. Those remain design choices.

Why LALRPOP and a comparison Pratt parser?

LALRPOP gives us one inspectable grammar for the language as a whole, typed Rust actions for constructing the AST, and explicit recovery productions. Pratt gives us a compact second account of the calculator’s precedence rules. Implementing both here makes the grouping decisions concrete and gives us an independent comparison. The later compiler keeps LALRPOP. It does not run both parsers.

Haskell-style syntax also needs work around the grammar. In Chapter 8, logos recognizes tokens, marginalia retains comments and whitespace for formatting, and offsides translates indentation into block delimiters. The latter two libraries supply the trivia and Haskell-style layout support this frontend needs. LALRPOP then consumes that prepared token stream. Layout remains visible as a separate, testable transformation instead of being scattered through parser actions. This calculator has neither layout nor comment preservation yet.

User-declared fixities introduce a separate issue. A generated parser cannot have a different precedence table for each source file. Chapter 8 parses flat operator chains and resolves their grouping afterward. Neither a Pratt loop nor a parser generator removes the need to decide when those declarations become known.

Syntax and typing

A typing judgment already describes this small language. If two operands have type Int, their sum has type Int:

$$\frac{\Gamma ⊢e_1:\mathsf{Int}\Gamma ⊢e_2:\mathsf{Int}}{\Gamma ⊢e_1+e_2:\mathsf{Int}}\text{(Add)}$$

We don’t need an inferencer yet, since integers are our only values. It does check lexical scope before evaluating. Pierce develops the distinction between syntax, typing, and evaluation (Pierce 2002). The Haskell Report is useful for comparison, although Fun’s later fixity rules are deliberately absent here (Simon Marlow 2010).

Implementation

lexer.rs uses logos to recognize tokens and retain byte spans. Keywords win over identifiers of the same length. An invalid character or an out-of-range literal produces E0001. ast.rs stores a span on each expression, making both parsers comparable without losing source information.

#![allow(unused)]
fn main() {
/// Byte offsets into the single source file, including parentheses when present.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Expr {
    pub kind: Kind,
    pub span: Range<usize>,
}

/// An error node exists only during recovery; the driver never evaluates it.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum Kind {
    Int(i64),
    Var(String),
    Neg(Box<Expr>),
    Binary(Op, Box<Expr>, Box<Expr>),
    Let(String, Box<Expr>, Box<Expr>),
    Error,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Op {
    Add,
    Sub,
    Mul,
    Div,
}
}

The generated parser implements precedence with nonterminals. The complete grammar also handles bindings, parentheses, unary minus, and a recovery production.

Sum: Expr = {
    <a:Sum> "+" <b:Product> => Expr::binary(Op::Add, a, b),
    <a:Sum> "-" <b:Product> => Expr::binary(Op::Sub, a, b),
    Product,
};
Product: Expr = {
    <a:Product> "*" <b:Unary> => Expr::binary(Op::Mul, a, b),
    <a:Product> "/" <b:Unary> => Expr::binary(Op::Div, a, b),
    Unary,
};

An ! production inserts an error node and stores the recovery diagnostic. The driver returns errors even when recovery produces a tree. The evaluator never receives recovery nodes. diagnostic.rs prints a stable error-code line and location, then lets ariadne render the source excerpt with byte indexing.

#![allow(unused)]
fn main() {
/// Parse and recover enough to report several syntax errors, then stop the pass.
pub fn parse(source: &str) -> Result<Expr, Vec<Diagnostic>> {
    let tokens = lexer::lex(source)?;
    let mut recovered = Vec::new();
    let parsed = parser::ExprParser::new()
        .parse(&mut recovered, tokens.into_iter().map(Ok));
    let mut errors: Vec<_> = recovered
        .into_iter()
        .map(|r| parse_error(r.error))
        .collect();
    match parsed {
        Ok(expr) if errors.is_empty() => Ok(expr),
        Ok(_) => Err(errors),
        Err(error) => {
            errors.push(parse_error(error));
            Err(errors)
        }
    }
}
}

The Pratt parser’s loop consumes operators whose binding power is high enough. Parsing the right operand at power + 1 makes the operator left-associative. Prefix parsing handles names, literals, parentheses, and negation. A separate entry handles let.

#![allow(unused)]
fn main() {
fn infix(&mut self, min_power: u8) -> Result<Expr, Diagnostic> {
    let mut left = self.prefix()?;
    loop {
        let (op, power) = match self.peek() {
            Some(Token::Plus) => (Op::Add, 1),
            Some(Token::Minus) => (Op::Sub, 1),
            Some(Token::Star) => (Op::Mul, 3),
            Some(Token::Slash) => (Op::Div, 3),
            _ => break,
        };
        if power < min_power {
            break;
        }
        self.at += 1;
        let right = self.infix(power + 1)?;
        left = Expr::binary(op, left, right);
    }
    Ok(left)
}
}

eval.rs uses a stack of bindings, searched from the end, to model lexical scope. It evaluates a binary operator’s left operand before its right operand and restores the environment even if a binding body fails. Arithmetic uses wrapping 63-bit values from the start, avoiding dependence on Rust’s debug overflow checks. The normalization function is included as a Rust item:

#![allow(unused)]
fn main() {
use crate::{
    ast::{Expr, Kind, Op},
    diagnostic::Diagnostic,
};
/// Check every variable occurrence without executing arithmetic.
pub fn check(expr: &Expr) -> Result<(), Vec<Diagnostic>> {
    fn visit(
        expr: &Expr,
        names: &mut Vec<String>,
        errors: &mut Vec<Diagnostic>,
    ) {
        match &expr.kind {
            Kind::Var(name) if !names.contains(name) => {
                errors.push(Diagnostic::new(
                    "E0101",
                    format!("unbound variable `{name}`"),
                    expr.span.clone(),
                ))
            }
            Kind::Neg(a) => visit(a, names, errors),
            Kind::Binary(_, a, b) => {
                visit(a, names, errors);
                visit(b, names, errors);
            }
            Kind::Let(name, a, b) => {
                visit(a, names, errors);
                names.push(name.clone());
                visit(b, names, errors);
                names.pop();
            }
            _ => {}
        }
    }
    let mut errors = Vec::new();
    visit(expr, &mut Vec::new(), &mut errors);
    if errors.is_empty() {
        Ok(())
    } else {
        Err(errors)
    }
}
/// The environment is a stack: the most recent binding shadows earlier names.
pub fn evaluate(
    expr: &Expr,
    env: &mut Vec<(String, i64)>,
) -> Result<i64, String> {
    match &expr.kind {
        Kind::Int(n) => Ok(normalize(*n)),
        Kind::Var(name) => env
            .iter()
            .rev()
            .find(|(key, _)| key == name)
            .map(|(_, value)| *value)
            .ok_or_else(|| format!("unbound variable `{name}`")),
        Kind::Neg(value) => {
            Ok(normalize(evaluate(value, env)?.wrapping_neg()))
        }
        Kind::Binary(op, left, right) => {
            let a = evaluate(left, env)?;
            let b = evaluate(right, env)?;
            Ok(normalize(match op {
                Op::Add => a.wrapping_add(b),
                Op::Sub => a.wrapping_sub(b),
                Op::Mul => a.wrapping_mul(b),
                Op::Div if b == 0 => return Err("divide by zero".into()),
                Op::Div => a / b,
            }))
        }
        Kind::Let(name, value, body) => {
            let value = evaluate(value, env)?;
            env.push((name.clone(), value));
            let result = evaluate(body, env);
            env.pop();
            result
        }
        Kind::Error => {
            Err("internal error: attempted to evaluate a recovery node"
                .into())
        }
    }
}
pub fn normalize(n: i64) -> i64 {
    (n << 1) >> 1
}
}

#![allow(unused)]
fn main() {
/// The environment is a stack: the most recent binding shadows earlier names.
pub fn evaluate(
    expr: &Expr,
    env: &mut Vec<(String, i64)>,
) -> Result<i64, String> {
    match &expr.kind {
        Kind::Int(n) => Ok(normalize(*n)),
        Kind::Var(name) => env
            .iter()
            .rev()
            .find(|(key, _)| key == name)
            .map(|(_, value)| *value)
            .ok_or_else(|| format!("unbound variable `{name}`")),
        Kind::Neg(value) => {
            Ok(normalize(evaluate(value, env)?.wrapping_neg()))
        }
        Kind::Binary(op, left, right) => {
            let a = evaluate(left, env)?;
            let b = evaluate(right, env)?;
            Ok(normalize(match op {
                Op::Add => a.wrapping_add(b),
                Op::Sub => a.wrapping_sub(b),
                Op::Mul => a.wrapping_mul(b),
                Op::Div if b == 0 => return Err("divide by zero".into()),
                Op::Div => a / b,
            }))
        }
        Kind::Let(name, value, body) => {
            let value = evaluate(value, env)?;
            env.push((name.clone(), value));
            let result = evaluate(body, env);
            env.pop();
            result
        }
        Kind::Error => {
            Err("internal error: attempted to evaluate a recovery node"
                .into())
        }
    }
}
}

main.rs connects these pieces to commands and a REPL. Try both parsers on the same expression and inspect their trees. The tests do this too, including generated expressions with different groupings. Comparing the trees catches mistakes that a coincidentally correct numerical answer could hide.

Running It

$ cd crates/ch02_calc
$ cargo run -q -- run tests/programs/precedence.fun
7
$ cargo run -q -- dump --pass=parse tests/programs/precedence.fun
(+ 1 (* 2 3))
$ cargo run -q -- run tests/programs/precedence.fun --parser=pratt
7
$ cargo run -q -- repl
Calc: :quit to exit, :parse EXPR to inspect the AST.
calc> let x = 6 in x * 7
42
calc> :quit

check verifies syntax and names without executing arithmetic. Thus 1 / 0 passes check but run reports fun: divide by zero and exits with status 1. Use dump --pass=tokens to inspect lexer spans.

Exercises

1. Easy. Predict both the value and the parse dump of 20 - 3 * 4 - 1, then run it.
2. Easy. Compare the spans of 1 and (1). Explain why their values agree.
3. Medium. Change the Pratt parser’s right binding power to power. Find the smallest subtraction expression that exposes the associativity change.
4. Medium. Write a malformed expression that reports two independent syntax errors. Explain where recovery can resume.
5. Hard. Extend the generator to insert redundant parentheses and verify that evaluation remains unchanged.

Further Reading

Pierce separates syntax and semantics carefully (Pierce 2002). The Haskell Report specifies a much larger concrete syntax and fixity-resolution procedure (Simon Marlow 2010).

Chapter 3: Lambda Calculus

New files

• src/names.rs
• src/normal.rs

Changed files

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

Motivation

Our calculator can name a number. What if we could name a computation and use it with different inputs? That’s a function, and adding functions takes us a surprisingly long way. With just lambdas and application we can express the pure untyped lambda calculus. Even data can be represented by functions, as we’ll see with Church encodings (Pierce 2002). That’s a remarkable amount of expressive power for two pieces of syntax!

There are a couple of details we need to get right. If two variables are both called x, how do we know which one a function means? And when we call a function, should we evaluate its argument first? We’ll build substitution and closures ourselves so we can see the answers, rather than quietly borrowing Rust’s answers.

The Language, Now

Programs remain single expressions. Lambdas have one parameter, application associates left, and booleans control an if expression. Comparisons are integer operations. There are no type annotations yet.

let twice = \f -> \x -> f (f x) in twice (\x -> x + 1) 0

A closure remembers the bindings present where its lambda was evaluated. In let x = 1 in let f = \y -> x + y in let x = 100 in f 2, the result is 3. Using the caller’s binding of x instead would give dynamic scope.

Theory

The Untyped Grammar

The pure untyped lambda calculus has just three forms. An expression is a variable, an application, or an abstraction. Read each vertical bar as “or”.

$$\begin{array}{rlrl}e& =x& & \text{variable}\\ & \mid e_1{e}_2& & \text{application}\\ & \mid \lambda x.e& & \text{abstraction}\end{array}$$

That’s the whole calculus! Our little language adds a few conveniences so we can experiment without encoding every number and boolean as a function.

$$\begin{array}{rlrl}e& =\cdots & & \text{the three forms above}\\ & \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}$$

Here $n$ is an integer and $op$ is one of +, -, *, /, ==, <, or <=. Parentheses group expressions without adding a tree node. The parser also has an Error placeholder for recovery, which isn’t a form of an accepted program. “Untyped” means we have no static type checker yet, not that every combination of these forms makes sense at runtime.

Reduction and Evaluation

Calling a lambda means replacing its parameter with the supplied argument. This step is called beta reduction. For \x -> x + 1 applied to 41, we replace x and get 41 + 1. So far, so good. The subtlety begins when names repeat. We replace only free occurrences of the parameter in the body, and rename an inner binder if it would capture a free name from the argument. We’ll work through exactly that mistake below (Pierce 2002).

Evaluation order decides which reduction we do next. Normal order takes the leftmost outermost reducible expression, and our full reducer also continues under lambdas. Call-by-value first evaluates the function and its argument, then enters the body. A lambda itself is already a value.

The difference becomes visible when a function ignores an argument that would run forever. Normal order can skip that argument. Call-by-value gets stuck trying to compute it. The Y combinator gives us a particularly striking example. It computes factorial under normal order but exhausts our strict evaluator’s fuel. Running out of fuel means we’ve reached our experiment’s limit, not that we’ve proved the computation will never finish.

Why De Bruijn Indices?

Names help us read programs, but their spelling is incidental to binding. \x -> x and \answer -> answer describe the same function. We call them alpha-equivalent. Renaming a bound variable consistently changes nothing. Comparing their syntax trees directly, however, finds different strings. A compiler that rewrites named terms must keep distinguishing harmless renaming from a change in which binder an occurrence refers to.

Consider this reduction of an open term, where y is free:

(\x -> \y -> x) y

Replacing x with y mechanically gives \y -> y. That is wrong. The function should return the free y supplied as its argument, regardless of its own parameter. Rename the inner parameter first:

(\x -> \z -> x) y
→ \z -> y

This is the capture problem our substitution function must solve. De Bruijn indices give binding a representation that does not depend on fresh spellings. Replace each bound occurrence with its distance to its binder, counting from zero. Count enclosing binders, not application nodes or source lines.

We write λ. body for an unnamed lambda in the examples below. Its numbers are variable indices, not integer literals. This is explanatory notation, not input syntax for the chapter’s parser.

For a longer example, walk into \f -> \x -> f (f x). Entering the first lambda pushes f onto a scope stack. Entering the second pushes x:

scope, nearest first:  [x, f]
index:                  0  1

f (f x)                 1 (1 0)
\f -> \x -> f (f x)     λ. λ. 1 (1 0)

Both occurrences of f have index 1. Application adds no binder, so entering (f x) does not change either index. Renaming the parameters to g and seed produces exactly the same indexed tree. Alpha-equivalence has become ordinary structural equality (Pierce 2002). This is useful in our printer tests. A parse–print–parse round trip should preserve binding even if names change.

An open term still needs a way to represent free variables. Our Term type keeps them as Free(name), separate from Bound(index). Thus \x -> x y becomes Lam(App(Bound(0), Free("y"))). A non-recursive let introduces a binder only in its body. In let x = x in x, the right-hand x is free and the final x is bound:

Let(Free("x"), Bound(0))

Indices make renaming simple, but moving terms across binders still requires care. Inside \a -> (\x -> \b -> x) a, the argument a has index 0 at its original location. After reduction the result is \a -> \b -> a, where the same occurrence needs index 1. Copying the old zero would accidentally select b. An evaluator that substitutes directly into indexed terms needs shifting: adjust references to surrounding binders when a term moves into or out of a scope, while leaving its internally bound references alone.

Here we use indices for conversion and comparison. The normal-order reducer still substitutes in the named tree, and the strict evaluator uses closures. That keeps each example focused. Later Fun passes use unique names so their dumps remain readable. Nameless terms are a useful tool for understanding binding, not a requirement for every compiler IR.

S, K, and I: Functions Without Binders

A combinator is a lambda term with no free variables. It needs no bindings from its surroundings. Three small combinators are enough to express the functions of the pure untyped lambda calculus:

I = \x -> x
K = \x -> \y -> x
S = \f -> \g -> \x -> f x (g x)

These capital letters are mathematical names. The executable tests use lowercase s, k, and i as ordinary local bindings. Applications associate left, so S f g a means ((S f) g) a. Each reduction rule needs all its displayed arguments before it can fire.

I and K are easy to picture. S explains how an application can depend on a shared input. Given f, g, and a, compute f a and g a, then apply the first result to the second. The parentheses in f a (g a) matter.

Try choosing K for both functions:

S K K a
→ K a (K a)        apply the S rule
→ a                apply the K rule

So S K K behaves as I. That’s a beautiful little result. We can build identity out of two operations that, at first glance, don’t look much like identity at all. S and K suffice, though keeping I around makes expressions easier to read. Try the chapter’s s k k (i 42) example and follow the reductions.

Why should these particular operations eliminate lambdas? For a body t, write [x]t for a combinator expression that accepts x and produces t. Once inner lambdas have been translated, there are three cases:

[x]x       = I
[x]t       = K t                  when x is not free in t
[x](p q)   = S ([x]p) ([x]q)       otherwise

If the body is the parameter itself, return it. If the body ignores the parameter, use K to discard it. Otherwise the body is an application, and S passes the parameter to both translated children. This procedure is called bracket abstraction. Work from the innermost lambda outward. Translating a closed pure lambda term eventually leaves only combinators and applications.

For example, remove the binder from \x -> f x, treating f as a free name:

[x](f x)
= S ([x]f) ([x]x)
= S (K f) I

Check the result by giving it an argument:

S (K f) I a
→ (K f a) (I a)
→ f (I a)
→ f a

The occurrence of x has disappeared. The free f remains, as it should. De Bruijn indices retain binders and encode their references as distances. Bracket abstraction removes the binders and expresses their work as application. This gives us a small example of compilation between two representations of the same computation.

There is a catch, and it is the same evaluation-order question we started with. Normal order reduces K 42 omega to 42 even if omega runs forever. Our strict evaluator tries to compute omega before entering K’s body, so it never gets that far. These combinator equations describe rewriting in the pure calculus. They don’t let a strict compiler discard arbitrary computations. We’ll use SKI to understand binding and reduction, while Fun’s back end will use closures. Closures also spare us the large application trees that a simple combinator translation can produce.

Implementation

ast.rs adds lambdas, application, booleans, and conditionals. Its printer uses precedence contexts and adds parentheses only where required to retain the tree. The parser gives application higher precedence than arithmetic:

Application: Expr = {
    <a:Application> <b:Atom> => {
        let (start, end) = (a.span.start, b.span.end);
        Expr::new(Kind::App(Box::new(a), Box::new(b)), start, end)
    },
    Atom,
};

names.rs computes free variables and performs capture-avoiding substitution. The helper below handles a binder. The recursive substitution handles each term form. Fresh names avoid both free and bound names in the original body and the replacement, preventing a new name from colliding with an inner lambda.

#![allow(unused)]
fn main() {
fn binder(
    name: &str,
    body: &Expr,
    target: &str,
    value: &Expr,
) -> (String, Expr) {
    if name == target {
        return (name.to_owned(), body.clone());
    }
    let mut name = name.to_owned();
    let mut body = body.clone();
    if free(value).contains(&name) && free(&body).contains(target) {
        let mut used = BTreeSet::from([target.to_owned()]);
        all_names(&body, &mut used);
        all_names(value, &mut used);
        let mut fresh = format!("{name}'");
        while used.contains(&fresh) {
            fresh.push('\'');
        }
        let variable = Expr::new(Kind::Var(fresh.clone()), 0, 0);
        body = substitute(&body, &name, &variable);
        name = fresh;
    }
    (name, substitute(&body, target, value))
}
}

The same module converts a named term to indices. A stack holds names from the outermost to the innermost scope. A let right-hand side is converted before its binder is pushed. That binder belongs only to the body.

#![allow(unused)]
fn main() {
/// Bound names are distances to binders; free names remain explicit.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum Term {
    Bound(usize),
    Free(String),
    Int(i64),
    Bool(bool),
    Lam(Box<Term>),
    App(Box<Term>, Box<Term>),
    Let(Box<Term>, Box<Term>),
    If(Box<Term>, Box<Term>, Box<Term>),
    Neg(Box<Term>),
    Binary(Op, Box<Term>, Box<Term>),
    Error,
}

/// Convert without substitution; alpha-equivalent expressions have equal terms.
pub fn debruijn(expr: &Expr, bound: &mut Vec<String>) -> Term {
    let mut go = |e: &Expr| Box::new(debruijn(e, bound));
    match &expr.kind {
        Kind::Var(n) => bound
            .iter()
            .rev()
            .position(|x| x == n)
            .map_or_else(|| Term::Free(n.clone()), Term::Bound),
        Kind::Lam(n, a) => {
            bound.push(n.clone());
            let body = debruijn(a, bound);
            bound.pop();
            Term::Lam(Box::new(body))
        }
        Kind::Let(n, a, b) => {
            let value = go(a);
            bound.push(n.clone());
            let body = debruijn(b, bound);
            bound.pop();
            Term::Let(value, Box::new(body))
        }
        Kind::App(a, b) => Term::App(go(a), go(b)),
        Kind::Binary(op, a, b) => Term::Binary(*op, go(a), go(b)),
        Kind::If(c, a, b) => Term::If(go(c), go(a), go(b)),
        Kind::Neg(a) => Term::Neg(go(a)),
        Kind::Int(n) => Term::Int(*n),
        Kind::Bool(b) => Term::Bool(*b),
        Kind::Error => Term::Error,
    }
}
}

normal.rs implements one small step. In the application case it substitutes without first evaluating the argument. If the function is not a lambda, it steps that function first, then the argument when no earlier redex exists.

#![allow(unused)]
fn main() {
Kind::App(function, argument) => {
    if let Kind::Lam(name, body) = &function.kind {
        return Ok(Some(substitute(body, name, argument)));
    }
    if let Some(next) = step(function)? {
        Kind::App(Box::new(next), argument.clone())
    } else if let Some(next) = step(argument)? {
        Kind::App(function.clone(), Box::new(next))
    } else {
        return Ok(None);
    }
}
}

reduce repeatedly calls step with a limit and a callback that displays each term. This reducer can inspect open terms, including irreducible applications. It is a term-rewriting demonstration rather than Fun’s eventual execution engine.

eval.rs instead stores a lambda’s environment in a closure:

#![allow(unused)]
fn main() {
/// Lexical bindings retained by a closure.
pub type Env = Vec<(String, Value)>;

#[derive(Clone, Debug)]
/// Runtime integers, booleans, and code paired with its lexical environment.
pub enum Value {
    Int(i64),
    Bool(bool),
    Closure(String, Rc<Expr>, Rc<Env>),
}
}

The call-by-value application case makes its order explicit:

#![allow(unused)]
fn main() {
Kind::App(function, argument) => {
    let function = evaluate(function, env, fuel)?;
    let argument = evaluate(argument, env, fuel)?;
    if let Value::Closure(name, body, captured) = function {
        let mut local = (*captured).clone();
        local.push((name, argument));
        evaluate(&body, &local, fuel)
    } else {
        Err("expected a function".into())
    }
}
}

The body runs in the captured environment extended with the argument. Each recursive visit consumes fuel. The CLI uses a larger host stack for these tree walkers. Chapter 5 replaces host recursion with an explicit machine. Neither fuel nor a larger stack is a substitute for that transformation.

Running It

$ cd crates/ch03_lambda
$ cargo run -q -- run tests/programs/church.fun
2
$ cargo run -q -- dump --pass=debruijn tests/programs/identity.fun
App(Lam(Bound(0)), Int(42))
$ cargo run -q -- repl
Lambda: :quit, :parse EXPR, :trace EXPR.
lambda> :trace (\x -> x) 42
(\x -> x) 42
42
lambda> :quit

Select normal order with run --engine=normal. Use --fuel=N when experimenting with terms that might not finish. The two engines count different operations, so the same fuel limit needn’t stop them at the same point. Try a function that ignores a failing argument to see why their answers can differ.

Exercises

1. Easy. Convert \x -> \y -> y x to de Bruijn indices by hand.
2. Medium. Substitute the free name y for x in \y -> \y' -> x y. Check the result’s free variables.
3. Medium. Translate \x -> x x by bracket abstraction, then apply the result to I. Compare its reduction with the lambda term.
4. Medium. Trace K I a b and explain which argument is discarded.
5. Hard. Construct a fixed-point combinator suitable for call-by-value and compare its trace with Y.

Further Reading

Pierce treats substitution, reduction, and nameless terms (Pierce 2002). Felleisen and Friedman introduce the abstract-machine setting that we return to in Chapter 5 (Felleisen and Friedman 1986).

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.

Chapter 5: Evaluation

New files

• src/cek.rs
• src/cbn.rs

Changed files

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

Motivation

A recursive evaluator is a lovely way to explain evaluation. Each Rust call follows one more piece of the program. Unfortunately, each call can also use another piece of Rust’s stack. Our little language has inherited a limit we never intended to give it. A bigger stack buys us time, but the problem is still there.

We’ll fix this by writing down what the evaluator needs to do next. Instead of leaving that information in Rust call frames, we’ll store it in a data structure and drive the whole evaluator with a loop. This is the idea behind an abstract machine.

The machine we’ll use is called CEK. The C tells us what we’re evaluating, the E records the current variable bindings, and the K records what comes next (Felleisen and Friedman 1986). The name is more intimidating than the idea. We’re turning the evaluator’s implicit bookkeeping into something we can inspect.

The Language, Now

A recursive binding gives its type before its right-hand side. That right-hand side must be syntactically a lambda. A value such as let rec x : Int = x in x is rejected with E0120.

let rec sum : Int -> Int -> Int =
  \(acc : Int) -> \(n : Int) ->
    if n == 0 then acc else sum (acc + n) (n - 1)
in sum 0 100

The self name is available inside the function and its enclosing let body. Its annotation is checked against the inferred right-hand-side type. fix is also an explicit term form, binding tighter than application:

fix (\(self : Int -> Int) -> \(n : Int) ->
  if n == 0 then 1 else n * self (n - 1)) 6

Both examples are well typed, but only the sum is tail recursive. Multiplication must wait for each recursive factorial call to return.

Theory

A fixed point of a function satisfies an unfolding equation. fix f behaves as f (fix f). Its type rule requires the argument to return the same type that it accepts (Pierce 2002).

$$\frac{\Gamma ⊢f:\tau \to \tau }{\Gamma ⊢\mathsf{fix}f:\tau }\text{(Fix)}$$

With fix, a well-typed program can run forever. Try fix (\(x : Int) -> x) and watch it use up any fuel budget you give it. The type checker hasn’t failed us. It never promised this recursive program would terminate. Recursive let uses the same fixed-point idea, but requires a function on the right-hand side so we know how to initialize it. Fun will keep that restriction.

Call-by-value evaluates a function and its argument before entering its body. Call-by-name substitutes an unevaluated argument each time it is used and stops at a lambda. Call-by-need additionally shares the argument’s result, requiring a suspended computation and a memoized result. Our small comparison interpreter implements call-by-name without memoization. Its substitution code makes the absence of sharing explicit. Chapter 3’s full normal-order reducer also enters lambda bodies, unlike this weak call-by-name evaluator.

Fun chooses call-by-value to make order and allocation easier to follow through its intermediate languages. Constructors will also be strict. A lambda remains a value, so the language can represent an action without performing it yet. Chapter 15 uses this property for IO. Laziness would require another runtime representation and another account of effects and space usage, beyond this book’s chosen compiler.

Implementation

The parser checks the recursive-binding restriction and lowers an accepted binding through this constructor:

#![allow(unused)]
fn main() {
/// Lower function-only recursive bindings to a fixed point with an annotated self parameter.
pub fn recursive(
    name: String,
    ty: Type,
    rhs: Expr,
    body: Expr,
    start: usize,
    end: usize,
) -> Result<Expr, Diagnostic> {
    if !matches!(rhs.kind, Kind::Lam(..)) {
        return Err(Diagnostic::new(
            "E0120",
            "recursive binding must be a function",
            rhs.span,
        ));
    }
    let self_function =
        Expr::new(Kind::Lam(name.clone(), ty, Box::new(rhs)), start, end);
    let fixed = Expr::new(Kind::Fix(Box::new(self_function)), start, end);
    Ok(Expr::new(
        Kind::Let(name, Box::new(fixed), Box::new(body)),
        start,
        end,
    ))
}
}

Value::Recursive stores the function used to construct a fixed point. Reading that recursive variable applies the stored function to its recursive reference. For a recursive function this rebuilds the closure in its original environment. It does not form a Rust ownership cycle. Entering fix evaluates its defining function immediately, so errors in that initialization are still strict. This is a teaching implementation of explicit recursion, not a general lazy binding mechanism.

cek.rs separates control from continuation frames. The frame variants are the places where the tree evaluator would otherwise wait for a recursive call.

#![allow(unused)]
fn main() {
/// The remaining work after the current expression returns a value.
enum Frame {
    Argument(Rc<Expr>, Rc<Env>),
    Apply(Value),
    Let(String, Rc<Expr>, Rc<Env>),
    If(Rc<Expr>, Rc<Expr>, Rc<Env>),
    Neg,
    Left(Op, Rc<Expr>, Rc<Env>),
    Right(Op, i64),
    Fix,
}

/// Control alternates between evaluating an expression and returning a value.
enum Control {
    Expr(Rc<Expr>, Rc<Env>),
    Value(Value),
    Apply(Value, Value),
}

/// Statistics make tail-space behavior testable without relying on timing.
pub struct ResultValue {
    pub value: Value,
    pub steps: usize,
    pub max_continuations: usize,
}
}

An application first pushes an Argument frame while evaluating its function. That frame then becomes an Apply frame while evaluating the argument. Once both values are available, the machine enters the body in the closure’s captured environment extended with the parameter. The application frames have already been popped:

#![allow(unused)]
fn main() {
Control::Apply(
    Value::Closure(name, body, captured),
    argument,
) => {
    let mut env = (*captured).clone();
    env.push((name, argument));
    Control::Expr(body, Rc::new(env))
}
Control::Apply(_, _) => {
    return Err("expected a function".into());
}
}

Look at the sum again. Its recursive call already produces the answer, so there’s nothing to remember for the caller. Factorial still has a multiplication to finish. That pending work needs a frame.

Both versions now avoid growing Rust’s call stack. Only the tail-recursive version avoids growing our explicit continuation stack as well. We check this by comparing the maximum continuation depth of a short run with a million-call run. Finishing on one generously sized machine wouldn’t tell us nearly as much.

The complete transition loop follows the expression forms and pops one frame when a value returns. max_continuations is measured before every transition, and a fuel counter makes divergent examples safe to inspect. Fuel counts machine transitions, so its numerical value differs from the tree evaluator’s count of expression visits.

The tiny call-by-name evaluator uses substitution instead of an environment for its application and let cases:

#![allow(unused)]
fn main() {
Kind::App(f, a) => {
    let function = evaluate(f, fuel)?;
    if let Kind::Lam(name, _, body) = function.kind {
        evaluate(&substitute(&body, &name, a), fuel)
    } else {
        Err("expected a function".into())
    }
}
Kind::Let(n, a, b) => evaluate(&substitute(b, n, a), fuel),
}

A call-by-need variant would replace this substitution with a shared cell whose first demand computes and saves the argument. We leave that implementation for future work. The production path here remains the strict machine, and the comparison interpreter is selected explicitly.

Running It

$ cd crates/ch05_eval
$ cargo run -q -- run tests/programs/sum-tail.fun
5050
$ cargo run -q -- run --engine=core tests/programs/factorial.fun
720
$ cargo run -q -- dump --pass=types tests/programs/fix-factorial.fun
Int
$ cargo run -q -- run --engine=cbn tests/programs/strict-argument.fun
1
$ cargo test -q a_million_tail_calls_use_bounded_continuations

The default engine is cek. core selects the recursive closure evaluator, cbn selects the comparison interpreter, and normal retains the earlier full reducer. --fuel=N bounds execution. Use a modest fuel budget for the tree interpreters. CEK is the one that removes their dependence on the host stack. The two strict engines should agree on both answers and failures. The call-by-name comparison deliberately differs when an unused argument would fail. Try it before reading the implementation and predict which error, if any, you’ll see.

Exercises

1. Easy. Draw the continuation frames for 1 + 2 * 3 as each operand returns.
2. Medium. Change the tail sum into a non-tail sum and measure both maximum continuation depths.
3. Medium. Explain why a closure must capture its definition environment rather than its caller’s environment.
4. Hard. Give an expression for which call-by-name repeats substantial work that call-by-value computes once. Explain what sharing would change.

Further Reading

Felleisen and Friedman develop the abstract-machine account (Felleisen and Friedman 1986). Pierce relates evaluation strategies, typing, and fixed points (Pierce 2002). Appel develops the related technique of making continuations explicit during compilation (Appel 1992). Our ANF compiler returns to that connection later.

Chapter 6: Hindley–Milner Inference

New files

• src/algorithm_w.rs
• src/union_find.rs

Changed files

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

Motivation

Look at \x -> x. We haven’t said what type x has, but we already know something useful. Whatever goes in is exactly what comes back out. Its type must have the shape a -> a.

That’s pretty cool! We learned something about every possible call without running the function once. An integer, a boolean, or another function would all work. A type scheme lets each use choose its own a. Hindley–Milner inference finds the most general scheme that the program permits (Damas and Milner 1982).

We’ll implement it in two ways. Algorithm W keeps an explicit record of the type substitutions it discovers (Damas and Milner 1982). Our second implementation updates mutable cells and uses levels to track which variables can be generalized. They solve the same equations, but make different implementation choices. Working through both will help us understand the algorithm before we choose the version we’ll carry into Fun.

The Language, Now

Poly has unannotated lambdas, application, polymorphic let, function-only let rec, integers, booleans, conditionals, and arithmetic. The explicit fix form remains available from the evaluation chapter for comparison exercises.

let id = \x -> x in
let first = id 1 in
id True

The two occurrences of id instantiate its scheme independently. Lambda parameters behave differently. \f -> let first = f 1 in f True is rejected, because f has one type throughout that lambda body.

We can drop the parameter annotations from the previous chapter. In particular, identity no longer has to choose between accepting integers and booleans. We’ll keep the evaluation machinery we already understand and concentrate on how the compiler discovers that freedom.

Theory

How to read a typing rule

A page of typing rules can look forbidding the first time you see one. The notation is mostly there to save us from repeating the same sentences. Each rule explains one piece of syntax. Start below the bar to see what we’re trying to establish, then look above it to see what we need to know about the parts. Pierce uses this style throughout his treatment of type systems (Pierce 2002).

$$\Gamma ⊢e:\tau$$

Read this as “under the assumptions in gamma, expression e has type tau.” The symbols keep repeated sentences short:

The colon asserts a type. It does not evaluate the expression. Gamma contains static assumptions, not runtime values. In this chapter it maps let-bound names to schemes and lambda parameters to monotypes, represented as schemes with no quantifiers. Greek variables in the rules are mathematical placeholders. The inferencer’s mutable metavariables are an implementation technique for finding which types satisfy the rules.

The horizontal bar means “if everything above holds, then the statement below holds.” It is not division. A rule with an empty top has no premises. Integer literals have type Int without consulting a subexpression.

$$\frac{}{\Gamma ⊢42:\mathsf{Int}}\text{(Int)}$$

For application, two facts must agree on the same input type:

$$\frac{\Gamma ⊢e_1:\alpha \to \beta \Gamma ⊢e_2:\alpha }{\Gamma ⊢e_1{e}_2:\beta }\text{(App)}$$

If e1 accepts an integer and returns a boolean, e2 must be an integer and the call returns a boolean. The repeated $\alpha$ expresses that agreement. During inference we discover it by unification. The rule describes a valid relationship. It does not prescribe an order in which to solve the premises.

Build a small derivation

Consider \x -> x + 1. Give x a provisional type. The addition rule requires both operands to be integers, which fixes that provisional type to Int. Writing $\Delta =\Gamma ,x:\mathsf{Int}$ keeps the resulting tree compact:

$$\frac{\frac{x:\mathsf{Int}\in \Delta }{\Delta ⊢x:\mathsf{Int}}\text{(Var)}\frac{}{\Delta ⊢1:\mathsf{Int}}\text{(Int)}}{\Delta ⊢x+1:\mathsf{Int}}\text{(Add)}$$

The two leaves justify Add by lookup and the literal rule. The lambda rule then moves the assumption about the parameter into a function type:

$$\frac{\Gamma ,x:\alpha ⊢e:\beta }{\Gamma ⊢\lambda x.e:\alpha \to \beta }\text{(Lam)}$$

Here $\lambda x.e$ means \x -> e. Lam gives our function type Int -> Int and removes the body’s local assumption about x. Replacing 1 with True breaks an Add premise, so we can’t complete the derivation.

From monotypes to schemes

The interesting part of let id = \x -> x in ... is that each use of id gets to choose its own argument type. We record that permission in a scheme. A monotype describes one type, perhaps with variables we haven’t solved yet. A scheme marks which variables a caller may choose afresh. Making those fresh copies is instantiation. Deciding which variables can safely be offered to callers is generalization (Damas and Milner 1982).

We can’t generalize a variable that the surrounding scope still depends on. Otherwise a local function could pretend to accept any type while quietly using an outer value whose type was already fixed. A lambda parameter therefore starts with one monotype shared by all its uses.

$$\frac{\Gamma ⊢e_1:\tau \sigma =\mathsf{gen}(\Gamma ,\tau )\Gamma ,x:\sigma ⊢e_2:\beta }{\Gamma ⊢\mathsf{let}x=e_1\mathsf{in}{e}_2:\beta }\text{(Let)}$$

Read Let in three steps. First infer the binding’s right-hand side, then generalize its type. Finally check the body with that scheme in scope. The equation for $\sigma$ is a side condition defining that scheme, rather than another program to evaluate. A variable is free in a type or environment when it is not bound by a scheme’s quantifier. Only variables absent from the environment’s free variables may be generalized.

For let id = \x -> x in ..., the right-hand side has type $\alpha \to \alpha$. If $\alpha$ is independent of the surrounding environment, we bind id to $\forall \alpha .\alpha \to \alpha$. Each lookup instantiates this scheme afresh. id 1 chooses Int. id True chooses Bool. By contrast, the parameter f in \f -> ... receives one monotype from Lam. All its uses must satisfy that same type. Quantification belongs to the let rule, not to every name that happens to denote a function.

Unification solves equality constraints between types. Two arrows unify by unifying their domains, applying what that learned, and unifying their codomains. A variable can be solved by a type only if it does not occur inside that type. Without this occurs check, self-application would require an infinite type. It is reported as E0202. Incompatible base types produce E0201.

A recursive function has one provisional monotype while its body is checked. Only after that check may the surrounding let generalize it. Our lowering to fix expresses this rule through the ordinary monomorphic self parameter. There is no polymorphic recursion here. The environment-based generalization rule and its efficient level-based form are developed in the cited accounts [Kiselyov (2013); Rémy (1992)].

Poly has no mutable state, so a let right-hand side need not be a syntactic value to generalize. For example, applying an identity to another identity still produces a polymorphic binding. This unrestricted rule will also apply to Fun.

A Small Payoff

Composition is a lovely example of how much a short definition can say.

let compose = \f -> \g -> \x -> f (g x) in
compose (\x -> x + 1) (\x -> x * 2) 20

The result is 41. More interestingly, compose itself knows nothing about integers. Its principal type is (b -> c) -> (a -> b) -> a -> c. The output of g is the input of f, so those two positions share b. Nothing requires a, b, and c to be the same type. Two applications in the definition give us that whole story. This is the kind of thing that makes inference worth building.

Implementation

The algorithms share immutable output types and schemes, but no unifier or inference traversal. Variable identities are canonicalized by first occurrence only after inference. That makes their principal types comparable up to renaming.

#![allow(unused)]
fn main() {
/// Variables are fresh identities; algorithms choose their own representation of solutions.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum Type {
    Int,
    Bool,
    Var(u32),
    Arrow(Box<Type>, Box<Type>),
}

/// Quantified variables are freshened independently at every occurrence.
#[derive(Clone, Debug)]
pub struct Scheme {
    pub variables: Vec<u32>,
    pub ty: Type,
}

impl Scheme {
    pub fn mono(ty: Type) -> Self {
        Self {
            variables: vec![],
            ty,
        }
    }
}

impl Type {
    pub fn arrow(a: Self, b: Self) -> Self {
        Self::Arrow(Box::new(a), Box::new(b))
    }
    /// Rename by first occurrence, making principal types comparable up to alpha-renaming.
    pub fn canonical(&self) -> Self {
        fn go(ty: &Type, names: &mut BTreeMap<u32, u32>) -> Type {
            match ty {
                Type::Var(n) => {
                    let next = names.len() as u32;
                    Type::Var(*names.entry(*n).or_insert(next))
                }
                Type::Arrow(a, b) => {
                    Type::arrow(go(a, names), go(b, names))
                }
                other => other.clone(),
            }
        }
        go(self, &mut BTreeMap::new())
    }
}
}

Algorithm W

algorithm_w.rs separates substitution, instantiation, generalization, and inference. The core rules extend to Poly’s arithmetic, conditional, and fixed-point forms, with source spans retained for diagnostics.

A substitution maps variables to types. Composition means applying the earlier substitution first, then rewriting its result with the newer one. Applying a substitution to a scheme must protect the scheme’s quantified variables.

#![allow(unused)]
fn main() {
impl Subst {
    fn apply(&self, ty: &Type) -> Type {
        match ty {
            Type::Var(n) => {
                self.0.get(n).map_or_else(|| ty.clone(), |t| self.apply(t))
            }
            Type::Arrow(a, b) => Type::arrow(self.apply(a), self.apply(b)),
            other => other.clone(),
        }
    }
    /// self after earlier: every earlier range is rewritten by the newer substitution.
    fn compose(&self, earlier: &Self) -> Self {
        let mut result: BTreeMap<_, _> =
            earlier.0.iter().map(|(n, t)| (*n, self.apply(t))).collect();
        for (n, t) in &self.0 {
            result.entry(*n).or_insert_with(|| t.clone());
        }
        Self(result)
    }
    fn environment(&self, env: &Env) -> Env {
        env.iter()
            .map(|(name, scheme)| {
                let mut filtered = self.clone();
                for n in &scheme.variables {
                    filtered.0.remove(n);
                }
                (
                    name.clone(),
                    Scheme {
                        variables: scheme.variables.clone(),
                        ty: filtered.apply(&scheme.ty),
                    },
                )
            })
            .collect()
    }
}
}

Application threads information learned from the function into the environment used to infer its argument. It then unifies the function’s type with an arrow from the argument’s type to a fresh result.

#![allow(unused)]
fn main() {
Kind::App(f, a) => {
    let (s1, tf) = self.infer(env, f)?;
    let (s2, ta) = self.infer(&s1.environment(env), a)?;
    let result = self.fresh();
    let s3 = unify(
        &s2.apply(&tf),
        &Type::arrow(ta, result.clone()),
        expr,
    )?;
    Ok((s3.compose(&s2.compose(&s1)), s3.apply(&result)))
}
}

The let case applies the right-hand side’s substitution to the environment before generalizing. Generalizing against the old environment would allow an already constrained variable to escape.

#![allow(unused)]
fn main() {
Kind::Let(n, value, body) => {
    let (s1, t) = self.infer(env, value)?;
    let mut local = s1.environment(env);
    local.insert(n.clone(), generalize(&local, s1.apply(&t)));
    let (s2, result) = self.infer(&local, body)?;
    Ok((s2.compose(&s1), result))
}
}

Mutable solutions and levels

union_find.rs replaces the explicit substitution map with metavariable cells. A cell records its creation level and an optional solution. Following a solved variable compresses its path, so later visits can reach the resolved type sooner.

#![allow(unused)]
fn main() {
#[derive(Clone)]
struct Meta {
    level: u32,
    solution: Option<Type>,
}

#[derive(Default)]
struct Infer {
    level: u32,
    metas: Vec<Meta>,
}

impl Infer {
    fn fresh(&mut self) -> Type {
        let n = self.metas.len() as u32;
        self.metas.push(Meta {
            level: self.level,
            solution: None,
        });
        Type::Var(n)
    }
    fn zonk(&mut self, ty: &Type) -> Type {
        match ty {
            Type::Var(n) => {
                match self.metas[*n as usize].solution.clone() {
                    None => ty.clone(),
                    Some(t) => {
                        let t = self.zonk(&t);
                        self.metas[*n as usize].solution = Some(t.clone());
                        t
                    }
                }
            }
            Type::Arrow(a, b) => Type::arrow(self.zonk(a), self.zonk(b)),
            other => other.clone(),
        }
    }
}

Inferring a let right-hand side enters a deeper level. Before installing a solution for an older metavariable, the occurs-check traversal lowers every metavariable reachable from that solution to the older level. These variables now belong to the outer scope, even if they were allocated inside the let.

#![allow(unused)]
fn main() {
/// One traversal rejects cycles and prevents younger variables escaping their scope.
fn occurs_and_lower(
    &mut self,
    n: u32,
    level: u32,
    ty: &Type,
    expr: &Expr,
) -> Result<(), Diagnostic> {
    match self.zonk(ty) {
        Type::Var(m) if m == n => Err(types::occurs(expr)),
        Type::Var(m) => {
            self.metas[m as usize].level =
                self.metas[m as usize].level.min(level);
            Ok(())
        }
        Type::Arrow(a, b) => {
            self.occurs_and_lower(n, level, &a, expr)?;
            self.occurs_and_lower(n, level, &b, expr)
        }
        _ => Ok(()),
    }
}
fn unify(
    &mut self,
    a: &Type,
    b: &Type,
    expr: &Expr,
) -> Result<(), Diagnostic> {
    let (a, b) = (self.zonk(a), self.zonk(b));
    match (&a, &b) {
        _ if a == b => Ok(()),
        (Type::Var(n), t) | (t, Type::Var(n)) => {
            self.occurs_and_lower(
                *n,
                self.metas[*n as usize].level,
                t,
                expr,
            )?;
            self.metas[*n as usize].solution = Some(t.clone());
            Ok(())
        }
        (Type::Arrow(a, b), Type::Arrow(c, d)) => {
            self.unify(a, c, expr)?;
            self.unify(b, d, expr)
        }
        _ => Err(types::mismatch(expr, &a, &b)),
    }
}
}

After returning to the enclosing level, generalization selects only unsolved variables whose levels are still deeper. It does not scan the environment. Every occurrence of a scheme replaces its quantified variables with fresh cells. Unquantified variables retain their identities and therefore their constraints.

#![allow(unused)]
fn main() {
Kind::Let(n, value, body) => {
    self.level += 1;
    let result = self.infer(env, value);
    self.level -= 1;
    let scheme = self.generalize(result?);
    env.push((n.clone(), scheme));
    let result = self.infer(env, body);
    env.pop();
    result
}
}

Try \x -> let y = \z -> x z in .... The type of y depends on x, so we mustn’t let two calls choose unrelated types for it. Calling y with both an integer and a boolean should fail. This is a useful example to keep beside the level-lowering code. It shows exactly what goes wrong if we generalize too much. We compare both inferencers on examples like this, including programs that should be rejected.

Running It

$ cd crates/ch06_poly
$ cargo run -q -- run tests/programs/poly-id.fun
True
$ cargo run -q -- dump --pass=types tests/programs/missing-annotation.fun
a -> a
$ cargo run -q -- dump --pass=types-w tests/programs/missing-annotation.fun
a -> a
$ cargo run -q -- repl
Poly: :quit, :type EXPR, :parse EXPR, :trace EXPR.
poly> :type \f -> \x -> f x
(a -> b) -> a -> b
poly> :quit

types and the normal checking path use the level-based inferencer. types-w selects Algorithm W’s independent result. Free variables in the displayed principal type are implicitly quantified. Evaluation still uses the strict CEK machine by default. Changing inference does not change its runtime values.

Exercises

1. Easy. Infer the type of \x -> \y -> x by writing down fresh variables first.
2. Medium. Trace the substitutions for let id = \x -> x in id id.
3. Medium. Explain why \f -> let a = f 1 in f True fails while the opening id example succeeds.
4. Hard. Draw the metavariable cells and levels for an inner function that captures an outer lambda parameter. Identify the unification that lowers a level.

Further Reading

Damas and Milner establish principal type schemes (Damas and Milner 1982). Kiselyov explains levels through the OCaml implementation (Kiselyov 2013), building on Rémy’s work (Rémy 1992). Pierce provides a broader introduction to typing judgments and derivations (Pierce 2002).

See my alternative writeup about just type systems for another route through these ideas.

Chapter 7: Design of Fun

New files

• src/session.rs
• src/core.rs
• src/typecheck.rs
• src/elaborate.rs
• src/diagnostics/codes.rs
• src/diagnostics/mod.rs
• src/parse.rs
• src/source.rs

Changed files

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

Motivation

We’ve built a parser, explored how functions run, and taught a compiler to infer types. Now we can bring those pieces together. From this chapter onward we’ll be building Fun, the language we’ll eventually compile to native code. Each chapter keeps a runnable snapshot, so you can always return to a simpler version when you want to see where an idea began.

Some of the work here is the ordinary engineering that makes the interesting parts pleasant to build. When the type checker finds a mistake, it needs to point back to the source. When one pass fails, the next shouldn’t try to make sense of its unfinished output. We’ll give names, source locations, and errors a shared home, then connect our passes into a compiler we can keep extending.

The Language, Now

A program is an explicit brace block containing declarations. Semicolons separate declarations. A trailing semicolon is optional. Each declaration may refer to itself and to earlier declarations. Forward references and mutual recursion wait until Chapter 9.

{
  twice f x = f (f x);
  sum n = if n == 0 then 0 else n + sum (n - 1);
  main = twice (\x -> x + 1) (sum 10);
}

Local let uses braces too, with one binding in this snapshot. Recursive bindings need no rec keyword. A self-reference identifies recursion, and the right-hand side must be a lambda. let { x = x; } in x is rejected with E0120.

Char contains a Unicode scalar value, and String is a primitive UTF-8 string. Strings concatenate with the monomorphic ++ operator. Integers accept hexadecimal notation and underscores. Both line comments and nested block comments are supported.

{ {- outer {- nested -} -} main = "Hello, " ++ "λ\n"; }

run still prints the value of main, including quotes and escapes for strings. It does not yet execute IO. Integer div and mod are curried built-in functions with floor semantics: div 7 (-3) is -3, and mod 7 (-3) is -2. The old calculator’s truncating division fixture changes accordingly.

Theory

A source program and an executable intermediate language serve different purposes. The source tree keeps spelling, syntax, and source spans. Core keeps only the operations needed for evaluation. Elaborating one into the other makes language conveniences explicit. Later we add types to Core so that a separate checker can validate each transformation (Pierce 2002).

Strictness remains a semantic requirement. The function is evaluated before its argument, operator operands are evaluated left to right, and a conditional selects only one branch. Top-level values are initialized once, in declaration order in this snapshot, before the final value of main is selected. Even an unused failing initializer stops the program. Top-level function bodies wait until application.

The current type system remains Hindley–Milner, using the level-based checker from Chapter 6 [Damas & Milner (1982); Kiselyov (2013)]. The recursive-binding restriction avoids constructing a value before its own initialization has completed. Recursive functions instead refer to their own closure when entered. Ordinary name scopes still use spelling-based maps here. Unique binding identities become operational in Chapter 9.

Implementation

Source and session state

source.rs gives a file its own identity and stores a line-start table. Spans are half-open byte ranges, matching the lexer, while displayed columns count Unicode scalar values. The file identity prevents equal offsets in different files from being confused.

#![allow(unused)]
fn main() {
/// Index of a source file in a session's source map.
#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
pub struct FileId(pub u32);

/// Half-open byte offsets within one source file.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct Span {
    pub file: FileId,
    pub start: u32,
    pub end: u32,
}

impl Span {
    pub fn new(file: FileId, start: usize, end: usize) -> Self {
        Self {
            file,
            start: start.try_into().expect("source exceeds 4 GiB"),
            end: end.try_into().expect("source exceeds 4 GiB"),
        }
    }
    pub fn range(self) -> Range<usize> {
        self.start as usize..self.end as usize
    }
    pub fn through(self, other: Self) -> Self {
        assert_eq!(self.file, other.file);
        Self {
            end: other.end,
            ..self
        }
    }
}

/// Original text and line starts; columns count Unicode scalar values.
pub struct SourceFile {
    pub name: String,
    pub text: String,
    lines: Vec<usize>,
}

#[derive(Default)]
/// Owns every source used by this compilation, including future Prelude input.
pub struct SourceMap {
    pub files: Vec<SourceFile>,
}

impl SourceMap {
    pub fn add(&mut self, name: impl Into<String>, text: String) -> FileId {
        assert!(u32::try_from(text.len()).is_ok(), "source exceeds 4 GiB");
        let mut lines = vec![0];
        lines.extend(text.match_indices('\n').map(|(i, _)| i + 1));
        let id = FileId(
            self.files.len().try_into().expect("too many source files"),
        );
        self.files.push(SourceFile {
            name: name.into(),
            text,
            lines,
        });
        id
    }
    pub fn get(&self, file: FileId) -> &SourceFile {
        &self.files[file.0 as usize]
    }
    pub fn line_col(&self, span: Span) -> (usize, usize) {
        let file = self.get(span.file);
        let offset = span.start as usize;
        let line = file.lines.partition_point(|start| *start <= offset) - 1;
        (
            line + 1,
            file.text[file.lines[line]..offset].chars().count() + 1,
        )
    }
}
}

names.rs supplies a handwritten interner and fresh-name supply. Repeated spellings share a Symbol. Repeated calls to the supply produce distinct Name identities. These definitions establish the interface for the later renamer without changing lexical scoping prematurely.

A session owns these facilities along with options and a diagnostic sink:

#![allow(unused)]
fn main() {
#[derive(Default)]
/// No pass needs a global interner, source map, or diagnostic sink.
pub struct Session {
    pub sources: SourceMap,
    pub interner: Interner,
    pub supply: Supply,
    pub options: Options,
    pub diagnostics: Vec<Diagnostic>,
}

impl Session {
    pub fn emit(&mut self, diagnostic: Diagnostic) {
        self.diagnostics.push(diagnostic);
    }
    pub fn finish<T>(&self, value: T) -> Result<T, Stop> {
        if self
            .diagnostics
            .iter()
            .any(|d| d.severity == Severity::Error)
        {
            Err(Stop)
        } else {
            Ok(value)
        }
    }
}
}

Each pass takes &mut Session and returns Result<Output, Stop>. A Stop carries no second copy of the diagnostics. The driver renders the accumulated structured errors and exits before calling the next pass. Lexing and duplicate-definition checks collect errors. Inference stops where a type error prevents a meaningful result.

diagnostics/codes.rs is the stable registry for errors and warnings, including codes reserved for upcoming features. A diagnostic has a severity, message, source labels, and notes. Ariadne renders it. The first two stderr lines remain the stable code and primary source location used by the corpus runner.

Surface checking and Core

lexer.rs uses logos, including callbacks for nested comments and literal escapes. Its reserved-word and operator tables also generate the HTML and PDF syntax definitions through cargo xtask syntax. The book build checks these outputs for drift.

parser.lalrpop builds spanned expressions and top-level bindings. Equation parameters become nested lambdas, and duplicate parameters are rejected. The checker processes declarations in source order. For a self-dependent binding, it introduces a provisional monotype while checking the lambda, unifies the result, then generalizes as in the previous chapter.

elaborate.rs lowers the checked tree into a separate Core representation:

#![allow(unused)]
fn main() {
#[derive(Clone, Debug, PartialEq, Eq)]
/// Immediate source values; strings are primitive UTF-8 values, not character lists.
pub enum Lit {
    Int(i64),
    Bool(bool),
    Char(char),
    String(String),
}

#[derive(Clone, Debug)]
/// The initial lambda Core; types, data constructors, and compiled cases arrive later.
pub enum Expr {
    Var(String),
    Lit(Lit),
    Lam(String, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Let(Bind, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Prim(Op, Vec<Expr>, Span),
}

#[derive(Clone, Debug)]
/// A recursive binding is guaranteed to have a lambda right-hand side.
pub struct Bind {
    pub name: String,
    pub rhs: Box<Expr>,
    pub recursive: bool,
}

#[derive(Clone, Debug)]
/// Globals retain source order in this chapter; SCC ordering arrives in Chapter 9.
pub struct Program {
    pub bindings: Vec<Bind>,
    pub main: String,
}
}

Operators become saturated primitive calls. Negation becomes subtraction from zero. The initial built-in environment provides curried wrappers for div and mod. --no-prelude removes those wrappers for isolated tests. The source Prelude arrives with datatypes. Source names beginning with prim_ are rejected with E0111 outside that future Prelude path.

--lint currently checks Core scope, primitive saturation, and the recursive lambda invariant. It is structural lint, not a type checker. Chapter 10 will replace it with the full System F check. The golden harness enables it on every run.

Reference evaluation

eval.rs interprets Core directly. A recursive closure stores its self name without creating a cyclic Rust environment. Application inserts that closure into its captured environment before the parameter:

#![allow(unused)]
fn main() {
Expr::App(function, argument) => {
    let function = evaluate(function, env, fuel)?;
    let argument = evaluate(argument, env, fuel)?;
    if let Value::Closure {
        parameter,
        body,
        env,
        recursive,
    } = &function
    {
        let mut local = (**env).clone();
        if let Some(name) = recursive {
            local.push((name.clone(), function.clone()));
        }
        local.push((parameter.clone(), argument));
        evaluate(body, &local, fuel)
    } else {
        Err("internal error: non-function application".into())
    }
}
}

The program runner initializes every top-level binding in order and retains those values in its environment. Integers normalize to 63 bits after arithmetic, and division checks zero before computing its floor quotient and matching remainder. Character and string printing share the source literal escape rules.

This reference evaluator is a recursive tree walker on a 512 MiB thread stack. It has a fuel limit for experiments, but no constant-stack guarantee. The explicit machine from Chapter 5 returns as an ANF oracle in Chapter 18. Keeping Core’s reference interpreter direct makes the forthcoming elaboration passes easier to inspect.

Running It

$ cd crates/ch07_fun
$ cargo run -q -- run tests/programs/fun-top.fun
42
$ cargo run -q -- dump --pass=types tests/programs/fun-string.fun
main : String
$ cargo run -q -- dump --pass=core --no-prelude tests/programs/fun-char.fun
val main = 'λ'
$ cargo run -q -- repl
Fun: expressions, :type EXPR, :core EXPR, :quit.
fun> :type \x -> x
main : a -> a
fun> :quit

Try the tokens, parse, types, and core dumps on the same small program. Each shows a different stage of the journey. You can use dump --pass=... or the common --dump=... option. The REPL evaluates individual expressions for now. Persistent definitions will arrive with the JIT.

Exercises

1. Easy. Use --dump=tokens to compare a nested comment with the operator -->.
2. Medium. Add an unused top-level initializer that divides by zero. Explain why main never produces a value.
3. Medium. Inspect Core for a local recursive function and explain where the self reference becomes bound.
4. Hard. Construct an invalid Core program that passes source parsing but could only be produced by a faulty compiler transformation. Extend a lint test to reject it.

Further Reading

The Haskell Report provides the lexical and scoping reference that Fun gradually adopts (Simon Marlow 2010). Pierce develops the typed intermediate-language perspective (Pierce 2002).

Chapter 8: Layout and the Extended Parser

New files

• src/layout.rs
• src/fixity.rs
• src/format.rs

Changed files

• src/parse.rs
• src/typecheck.rs
• src/ast.rs
• src/elaborate.rs
• src/lexer.rs
• src/lib.rs
• src/main.rs
• src/types.rs

Motivation

The braces were useful while we were getting started. By now they’re mostly making us type punctuation for structure we can already see in the indentation. Let’s make Fun a little nicer to write.

We’ll add layout, local helpers with where, type signatures, and user-defined operators. Much of this can happen before evaluation. Indentation becomes punctuation, sections become lambdas, and operator chains acquire their grouping once we know the declared fixities. It’s a satisfying compiler trick. We can make the source language more expressive while keeping its evaluator small.

The Language, Now

Braces and semicolons become optional when indentation supplies their boundaries. A where block belongs to its equation. The equation’s parameters remain visible inside it. Several local declarations may share a let block.

addTwo x = x + y
  where
    y = 2

main = let result = addTwo 40 in result

Signatures can appear before or after their binding within the same block. Type variables are implicitly quantified. A signature may specialize an inferred type, but it cannot make the implementation more polymorphic than it is.

id :: a -> a
id x = x

main = let { n :: Int; n = id 42; } in n

Operators may be defined in prefix or infix form. Their fixities apply throughout the file, even before the fixity declaration. An undeclared operator associates to the left at precedence 9. Named functions become operators inside backticks.

infixr 5 %%

a %% b = a * 10 + b

main = 1 %% 2 %% 3

This program prints 33 because it means 1 %% (2 %% 3). Sections supply one argument: (40 +) and (+ 2) are functions. (- 2) instead means negation. Unary minus has precedence 6, so -2 * 3 + 4 means (-(2 * 3)) + 4. Write parentheses around negation used after an operator of precedence 6 or greater.

Theory

Layout is easier to understand once we stop treating whitespace as mysterious. We’re going to translate indentation into the braces and semicolons our parser already knows. The Haskell Report describes this translation (Simon Marlow 2010). Let’s do it by hand before looking at the adapter.

See the Invisible Delimiters

Think of indentation as a shorthand for punctuation. The first declaration in a block sets its left margin. Another declaration at that margin begins a new item. Moving back to an enclosing margin finishes the block.

scale x = result
  where
    doubled = x + x
    result = doubled * 3

main = let n = 7 in scale n

Before parsing, layout makes the omitted punctuation explicit. Here every brace and semicolon was inserted by the layout pass:

{ scale x = result
    where { doubled = x + x
          ; result = doubled * 3
          }
; main = let { n = 7 } in scale n
}

The file gets an outer pair of braces. doubled establishes the where block’s indentation, and result at the same column gets a separator before it. main is farther left, so layout closes the where block and separates the next top-level declaration. The same-line in closes the let block even though there was no dedent. The final brace closes the file at end of input. Writing the braces yourself produces the same grouping.

The later pattern and IO chapters use the same mechanism after of and do:

main = do
  case flag of
    True -> putStrLn "yes"
    False -> putStrLn "no"
  putStrLn "done"

Its explicit form is:

{ main = do
    { case flag of
        { True -> putStrLn "yes"
        ; False -> putStrLn "no"
        }
    ; putStrLn "done"
    }
}

The dedent before the last action closes only the of block. That action is still inside do. These constructs arrive later, but the rule for translating their indentation is already the same. Use --dump=layout to see the actual tokens, including the spans that distinguish inserted punctuation from source characters.

Fixity resolution compares adjacent operators before constructing applications. A greater precedence binds first. Equal precedences require compatible associativities. Two left-associative operators reduce from the left, and two right-associative operators from the right. Non-associative operators and mixed associativities at the same precedence require parentheses (Simon Marlow 2010).

A signature makes a promise. If we write a -> a, we mean the function works for any a its caller chooses. The checker mustn’t make that promise true by quietly choosing a = Int.

We enforce this by replacing the signature’s quantified variables with rigid identities, called skolems. Inference variables can be solved, but a skolem stands for an arbitrary type and must stay arbitrary. We instantiate the inferred scheme with fresh flexible variables and try to unify it with the rigid signature. We also check that no skolem escapes into the surrounding scope. Together these checks tell us whether the inferred type supports the promise [Damas & Milner (1982); Pierce (2002)].

Implementation

Layout and trivia

The logos lexer emits comment tokens with their original text. TriviaLexer records them in a side table and exposes only semantic tokens. LayoutLexer then performs indentation insertion. The adapter groups explicit braces and parentheses, recursively handling layout inside them, so a parenthesized let still gets its own block.

#![allow(unused)]
fn main() {
pub fn layout(
    sess: &mut Session,
    file: FileId,
) -> Result<Vec<Spanned>, Stop> {
    let tokens = lexer::lex(sess, file)?;
    let source = &sess.sources.get(file).text;
    let eager = !matches!(tokens.first(), Some((_, Token::Open, _)));
    // offsides measures byte columns with fixed-width tabs. Give it a shadow
    // source whose byte positions are visual columns, then restore original spans.
    let (shadow, forward, backward) = visual_source(source);
    let tokens = tokens
        .into_iter()
        .map(|(lo, t, hi)| (forward[lo], t, forward[hi]))
        .collect::<Vec<_>>();
    match region(&shadow, &tokens, eager)
        .map(|tokens| {
            tokens
                .into_iter()
                .map(|(lo, t, hi)| (backward[lo], t, backward[hi]))
                .collect()
        })
        .map_err(|(lo, hi, message)| (backward[lo], backward[hi], message))
    {
        Ok(tokens) => Ok(tokens),
        Err((lo, hi, message)) => {
            sess.emit(Diagnostic::error(
                ErrorCode::Parse,
                message,
                Span::new(file, lo, hi),
            ));
            Err(Stop)
        }
    }
}
}

The library does not expose a let/in closure operation. The adapter tracks which virtual frames have already closed at in, suppressing their later separators and closing braces. It also handles empty blocks and redundant virtual separators beside explicit semicolons. Tokens keep their original byte offsets. Inserted punctuation has zero-width spans.

of and do participate in lexical layout tests now. Their language constructs still wait for Chapters 11 and 15, respectively. The compiler does not accept those expressions prematurely.

Operator chains

The grammar retains a first operand followed by operator/operand pairs. Parentheses remain explicit until the resolver has established their boundary. A stack resolves these chains. A distinguished unary entry gives negation its precedence.

#![allow(unused)]
fn main() {
fn chain(
    &mut self,
    first: Expr,
    pairs: Vec<(String, Expr)>,
) -> Result<Expr, Diagnostic> {
    let mut values = Vec::new();
    let mut operators: Vec<Option<String>> = Vec::new();
    self.operand(first, &mut values, &mut operators)?;
    for (op, value) in pairs {
        let next = self.fix(&op);
        while let Some(previous) = operators.last() {
            let prior =
                previous.as_ref().map(|p| self.fix(p)).unwrap_or(Fix {
                    precedence: 6,
                    assoc: Assoc::Left,
                });
            if prior.precedence < next.precedence {
                break;
            }
            if prior.precedence == next.precedence && previous.is_some()
            {
                if prior.assoc != next.assoc
                    || prior.assoc == Assoc::None
                {
                    return Err(self.error(value.span,"operators with conflicting fixities need parentheses"));
                }
                if prior.assoc == Assoc::Right {
                    break;
                }
            }
            let prior = operators.pop().unwrap();
            self.reduce(&mut values, prior);
        }
        operators.push(Some(op));
        self.operand(value, &mut values, &mut operators)?;
    }
    while let Some(op) = operators.pop() {
        self.reduce(&mut values, op);
    }
    Ok(values.pop().unwrap())
}
}

Sections become lambdas with generated names that source identifiers cannot spell. The current primitive operators remain direct arithmetic nodes when unshadowed. User operators become ordinary curried applications. Core therefore needs no new expression forms.

Checking signatures

Declarations are collected before signatures are attached to bindings. The checker first infers and generalizes a binding, then tests its signature in a trial store. A successful check specializes the live scheme used by subsequent occurrences. Recursive calls remain monomorphic during inference. Signature-guided polymorphic recursion arrives with the later signature checker.

#![allow(unused)]
fn main() {
fn check_signature(
    &mut self,
    inferred: &Scheme,
    declared: &Scheme,
    expr: &Expr,
) -> Result<Scheme, Diagnostic> {
    fn rigid(ty: &Type) -> Type {
        match ty {
            Type::Var(n) => Type::Skolem(*n),
            Type::Arrow(a, b) => Type::arrow(rigid(a), rigid(b)),
            t => t.clone(),
        }
    }
    fn has_skolem(ty: &Type) -> bool {
        match ty {
            Type::Skolem(_) => true,
            Type::Arrow(a, b) => has_skolem(a) || has_skolem(b),
            _ => false,
        }
    }
    let mut trial = self.clone();
    let actual = trial.instantiate(inferred);
    let expected = rigid(&declared.ty);
    let invalid = trial.unify(&actual, &expected, expr).is_err()
        || (0..self.metas.len()).any(|n| {
            self.metas[n].level <= self.level
                && has_skolem(&trial.zonk(&Type::Var(n as u32)))
        });
    if invalid {
        return Err(Diagnostic::error(
            ErrorCode::Signature,
            format!(
                "signature {} is not an instance of inferred type {}",
                declared.ty,
                inferred.ty.canonical()
            ),
            expr.span,
        ));
    }
    // Specialization can constrain variables captured from an outer scope.
    self.level += 1;
    let actual = self.instantiate(inferred);
    let expected = self.instantiate(declared);
    let result = self.unify(&actual, &expected, expr);
    self.level -= 1;
    result?;
    Ok(self.generalize(expected))
}
}

Formatting

The formatter uses marginalia’s document algebra and attached comment map. Its canonical output uses explicit blocks and keeps source parentheses. Comments move to separate leading lines at token boundaries, preserving their text and order. This avoids inserting punctuation inside a line comment.

#![allow(unused)]
fn main() {
pub fn format(sess: &mut Session, file: FileId) -> Result<String, Stop> {
    let parsed = parse::parse(sess, file)?;
    crate::fixity::resolve(sess, parsed)?;
    let (semantic, trivia) = lexer::trivia(sess, file)?;
    let tokens = layout::layout(sess, file)?;
    let source = &sess.sources.get(file).text;
    let mut comments = attach(
        source,
        &trivia,
        semantic.iter().map(|(lo, _, hi)| span(*lo, *hi)),
        AttachOptions::default(),
    );
    // Tokens are smaller anchors than statements. Put their comments on
    // separate leading lines so a trailing line comment cannot swallow a
    // newly inserted separator or a following `where`.
    for (lo, _, hi) in &semantic {
        let entry = comments.entry(span(*lo, *hi));
        entry.leading.append(&mut entry.trailing);
    }
    let mut cursor = 0;
    let doc = document(source, &tokens, &mut cursor, false);
    let rendered = pretty::render(&doc, &comments, RenderOpts::default());
    Ok(format!("{}\n", rendered.trim_end()))
}
}

The tests compare parsed trees after removing spans, rather than merely comparing results of evaluation. Every syntactically valid corpus program must round-trip, and formatting the output again must produce exactly the same bytes. Dedicated cases retain nested block comments and comments beside where.

Running It

$ cd crates/ch08_layout
$ cargo run -q -- run tests/programs/layout/right-fixity.fun
33
$ cargo run -q -- dump --pass=fixity tests/programs/layout/negation.fun
{
  main = -(2 * 3) + 4;
}
$ cargo run -q -- fmt example.fun
$ cargo run -q -- fmt example.fun --check

The three dumps make a useful little tour. --dump=layout reveals the inserted punctuation, --dump=parse shows operator chains before grouping, and --dump=fixity shows the chosen grouping. Try changing only the indentation or a fixity declaration and watch which stage first changes.

Exercises

1. Introductory. predict the grouping of three operators with distinct fixities, then compare the fixity dump with your answer.
2. Intermediate. Explain why (1 + 2 *) is rejected and repair it with parentheses.
3. Intermediate. Add a formatter test with nested comments between an operator and its operand. Check both tree equality and comment retention.
4. Advanced. Construct a local signature whose skolem would escape through a captured lambda parameter. Trace the trial-store check that rejects it.
5. Advanced. Compare the restricted in rule with the Report’s general parse-error(t) rule. Identify syntax for which the latter would do more work.

Further Reading

The Report specifies layout and fixity resolution precisely (Simon Marlow 2010). Damas and Milner establish the principal-type property used by signature checks (Damas and Milner 1982). Pierce develops the distinction between polymorphic types and their instances in a broader type-theoretic setting (Pierce 2002).

Chapter 9: The Renamer

New files

• src/rename.rs
• src/scc.rs
• src/renamed.rs

Changed files

• src/names.rs
• src/typecheck.rs
• src/ast.rs
• src/core.rs
• src/elaborate.rs
• src/eval.rs
• src/fixity.rs
• src/lib.rs
• src/main.rs
• src/parse.rs
• src/types.rs

Motivation

Two variables can both be called x and mean entirely different things. That’s easy enough to follow in a small expression. It gets less comfortable when the compiler starts moving expressions around. We’d like to settle which binding each occurrence means once, then carry that answer through the rest of the compiler.

That’s the renamer’s first job. Its second is to free us from writing helpers before the functions that use them. Some functions even call each other, so there is no possible ordering that puts every helper first. We’ll find those groups in a dependency graph and give the type checker the whole group at once.

The Language, Now

Top-level and local declarations may refer forward within their block. These two functions belong to the same recursive component:

even n = if n == 0 then True else odd (n - 1)

odd n = if n == 0 then False else even (n - 1)

main = even 100

Each binding block is one lexical scope. A local definition shadows a global with the same spelling. Two definitions in the same block are an E0102 error. Every member of a recursive component must have a function right-hand side. Thus a = b; b = a is rejected with E0120, even if neither value is used.

Fixities also receive a scope check. A top-level fixity declaration must have a matching definition in the file (E0130). An unbound variable reports E0101 and suggests an in-scope spelling when its edit distance is at most two.

Theory

A binding identity consists of an interned spelling and a fresh integer. The spelling serves diagnostics. The unique integer separates shadowed binders. Inference and Core use these identities, so neither has to repeat lexical lookup. This is the compiler counterpart of the binding distinctions explored in Chapter 3 (Pierce 2002).

Draw an arrow from a function to each binding in its block that it uses. If even calls odd and odd calls even, we can follow arrows from either one back to the other. They belong together. A strongly connected component is a maximal group with this mutual-reachability property.

Now treat each group as one node. The resulting graph has no cycles, so we can process its dependencies first. That’s the order our type checker needs. A helper outside a recursive group can have its type generalized before its callers use it (Simon Marlow 2010).

Inside a recursive component, allocate one provisional monotype per binder and infer all bodies against them. Unify those provisional types with the results. Only then generalize the component. Outside the component, each occurrence can instantiate the resulting schemes independently. Signatures still check inferred types here. Signature-directed polymorphic recursion remains Chapter 14’s work.

Implementation

Name resolution

The surface tree retains a whole local declaration block until renaming. The renamer allocates all of that block’s identities before visiting any right-hand side. Each lambda introduces a smaller scope containing its parameter. Lookup searches scopes from the innermost outward.

#![allow(unused)]
fn main() {
pub fn rename(
    sess: &mut Session,
    program: ast::Program,
) -> Result<Program, Stop> {
    let program = crate::fixity::resolve(sess, program)?;
    for fixity in &program.fixities {
        for op in &fixity.operators {
            if !program.bindings.iter().any(|b| b.name == *op) {
                sess.emit(Diagnostic::error(
                    ErrorCode::OrphanFixity,
                    format!("fixity without a definition: {op}"),
                    fixity.span,
                ));
            }
        }
    }
    let mut primitives = Vec::new();
    let mut prelude = BTreeMap::new();
    if !sess.options.no_prelude {
        for op in [
            Op::Div,
            Op::Mod,
            Op::Add,
            Op::Sub,
            Op::Mul,
            Op::Append,
            Op::Eq,
            Op::Lt,
            Op::Le,
        ] {
            let id = sess.fresh_id(op.text());
            prelude.insert(op.text().into(), id.clone());
            primitives.push((op, id));
        }
    }
    let mut renamer = Renamer {
        sess,
        scopes: vec![prelude],
    };
    let groups = renamer.bindings(program.bindings);
    let main = renamer.lookup("main", program.span);
    renamer.sess.finish(Program {
        groups,
        primitives,
        main,
        span: program.span,
    })
}
}

The renamed tree is a separate IR. Its occurrences contain an Id, which keeps a Name and its diagnostic spelling together. Dumps display names as x#12. This small amount of repeated text keeps dumps readable after the source session has gone away. Comparisons still include the allocated identity.

Errors accumulate during the walk. An unresolved occurrence receives a fresh placeholder so other bodies can still be checked for scope errors. The driver stops after the renaming pass, before any placeholder can reach evaluation.

Dependency components

Tarjan’s search assigns each vertex an index and records the lowest reachable index still active on the search stack. When the two indices agree, the vertex is the root of a complete component, which can be popped together.

#![allow(unused)]
fn main() {
fn visit(&mut self, v: usize) {
    self.index[v] = Some(self.next);
    self.low[v] = self.next;
    self.next += 1;
    self.stack.push(v);
    self.active[v] = true;
    for &w in &self.edges[v] {
        if self.index[w].is_none() {
            self.visit(w);
            self.low[v] = self.low[v].min(self.low[w]);
        } else if self.active[w] {
            self.low[v] = self.low[v].min(self.index[w].unwrap());
        }
    }
    if self.low[v] == self.index[v].unwrap() {
        let mut group = Vec::new();
        loop {
            let w = self.stack.pop().unwrap();
            self.active[w] = false;
            group.push(w);
            if w == v {
                break;
            }
        }
        group.sort_unstable();
        self.result.push(group);
    }
}
}

Our edges point toward dependencies, so completed components arrive in the order inference needs. We visit source indices in a fixed order to keep dumps reproducible. A group containing just one binding is recursive only if that binding refers to itself. As a check on Tarjan’s bookkeeping, the tests also find components by the much slower but direct method of testing mutual reachability.

Inference by group

The environment contains all provisional types while a recursive component is being inferred. Generalization waits until every body has contributed constraints. Signatures are checked against the inferred schemes, and specialization propagates through the shared component before the exported schemes are finalized.

#![allow(unused)]
fn main() {
fn group(
    &mut self,
    env: &mut Vec<(Id, Scheme)>,
    group: &BindGroup,
) -> Result<(), Diagnostic> {
    self.level += 1;
    let size = env.len();
    let provisional: Vec<_> = group
        .binds
        .iter()
        .map(|b| (b.id.clone(), self.fresh()))
        .collect();
    if group.recursive {
        env.extend(
            provisional
                .iter()
                .map(|(id, ty)| (id.clone(), Scheme::mono(ty.clone()))),
        );
    }
    let inferred = group
        .binds
        .iter()
        .zip(&provisional)
        .map(|(b, (_, expected))| {
            let ty = self.infer(env, &b.rhs)?;
            if group.recursive {
                self.unify(expected, &ty, &b.rhs)?;
            }
            Ok(ty)
        })
        .collect::<Result<Vec<_>, Diagnostic>>();
    env.truncate(size);
    self.level -= 1;
    let inferred = inferred?;
    for (binding, ty) in group.binds.iter().zip(&inferred) {
        if let Some(annotation) = &binding.annotation {
            let scheme = self.generalize(ty.clone());
            self.check_signature(&scheme, annotation, &binding.rhs)?;
        }
    }
    self.level += 1;
    for (binding, ty) in group.binds.iter().zip(&inferred) {
        if let Some(annotation) = &binding.annotation {
            let declared = self.instantiate(annotation);
            self.unify(ty, &declared, &binding.rhs)?;
        }
    }
    self.level -= 1;
    for (binding, ty) in group.binds.iter().zip(inferred) {
        env.push((binding.id.clone(), self.generalize(ty)));
    }
    Ok(())
}
}

That last step matters. If f and g call one another and f has an Int -> Int signature, a shared argument type must also constrain g. Exporting an unconstrained polymorphic scheme for g would be unsound. A regression test rejects a subsequent g True call.

Recursive closures

The interpreter stores an immutable recipe for every recursive group: its lambda bodies and the outer environment. Entering one of these closures reconstructs the group’s bindings before adding the function argument. No closure needs a mutable pointer to itself, and there is no reference-counting cycle.

#![allow(unused)]
fn main() {
fn recursive_values(bindings: Rc<Vec<Bind>>, env: Rc<Env>) -> Env {
    let mut values = Vec::new();
    for binding in bindings.iter() {
        let Expr::Lam(parameter, body) = &*binding.rhs else {
            unreachable!("recursive lambda invariant")
        };
        let value = Value::Closure {
            parameter: parameter.clone(),
            body: Rc::new(*body.clone()),
            env: env.clone(),
            recursive: Some(bindings.clone()),
        };
        values.push((binding.name.clone(), value));
    }
    values
}
}

Top-level value initializers run once in dependency order. Functions are closures. Creating one does not run its body. Core lint now checks unique binder identities as well as scope, primitive saturation, and the recursive-lambda restriction.

Running It

$ cd crates/ch09_rename
$ cargo run -q -- run tests/programs/rename/mutual.fun
True
$ cargo run -q -- dump --pass=rename tests/programs/fun-forward.fun
nonrec { later#10 = 1; }
nonrec { main#9 = later#10; }
$ cargo xtask check-inherit 09
chapter 09: 101 inherited programs verified and chapter tests passed

Try moving the helper in a small program below its caller. It now works. Then make the two functions call each other and inspect the rename dump. You should see one recursive group, which tells the checker to infer them together.

Exercises

1. Introductory. annotate each occurrence of x in a nested-shadowing example with the binder it references. Compare with the rename dump.
2. Intermediate. Draw the dependency graph of a three-function recursive group with one non-recursive helper, then predict the emitted component order.
3. Intermediate. Add a diagnostic test with two independent misspelled names and verify that the pass reports both.
4. Advanced. Explain why the immutable closure recipe has no reference-counting cycle even when one of its functions returns another closure.
5. Advanced. Identify where signature-directed polymorphic recursion will require the current component construction and checking strategy to change.

Further Reading

The Haskell Report describes binding groups and dependency analysis (Simon Marlow 2010). Pierce supplies the underlying treatment of variables, scope, and binding (Pierce 2002).

Chapter 10: Typed Core and Core Lint

New files

• src/core_lint.rs
• src/core_type.rs

Changed files

• src/core.rs
• src/elaborate.rs
• src/typecheck.rs
• src/eval.rs
• src/lib.rs
• src/main.rs
• src/rename.rs
• src/renamed.rs

Motivation

The type checker has accepted our program. Excellent. Now the compiler gets to rewrite it, which gives us plenty of opportunities to introduce mistakes of our own. We might pass the wrong argument, forget a type instantiation, or reuse a variable identity. The source program being correct doesn’t help if we translate it incorrectly.

We’ll give Core explicit types and write a second checker for it. This checker has an easier job than inference. All the answers are already in the tree, so it only needs to verify that they fit together. When a transformation goes wrong, we can catch it close to where it happened. A compiler that checks its own homework is a rather useful thing to have.

The Language, Now

We can still write polymorphic functions without spelling out their type arguments.

id x = x

number = id 42

main = id True

In Core, the definition of id abstracts over a type variable. Its two uses apply it first to Int and then to Bool. Those applications are real IR nodes rather than comments on an untyped expression. The evaluator ignores their types, so this program still prints True.

Theory

The source expression id 42 hides a small decision. We’re using identity at Int. System F gives us a way to write that decision into the program. A type abstraction introduces a type parameter, and a type application chooses a type for it. Girard and Reynolds developed this explicit treatment of polymorphism [Girard (1972); Reynolds (1974)].

Think of the two new forms alongside ordinary lambdas and calls. An ordinary lambda waits for a value. A type abstraction abstracts over a type. This analogy helps us read the rules, although the type arguments will disappear before runtime.

$$\frac{\Gamma ,\alpha ⊢e:\tau \alpha \notin \mathsf{ftv}(\Gamma )}{\Gamma ⊢\Lambda \alpha .e:\forall \alpha .\tau }\text{(Type abstraction)}$$

$$\frac{\Gamma ⊢e:\forall \alpha .\tau \Gamma ⊢\sigma :\ast }{\Gamma ⊢e[\sigma ]:\tau [\sigma /\alpha ]}\text{(Type application)}$$

Every type binder has kind * in this chapter. Higher-kinded constructors will extend the kind judgment later. Ordinary application still requires an arrow type. A universally quantified function must first receive its type arguments.

Core supports full System F. Fun still exposes only HM polymorphism. Hand-built Core terms test that distinction without extending source syntax (Pierce 2002).

Implementation

The Core Datatypes

We can write the same language as a small grammar before looking at the Rust. Read each vertical bar as “or”. An expression $e$ is one of the forms below, and the right-hand column tells us what that form does.

$$\begin{array}{rlrl}e& =x& & \text{local variable}\\ & \mid g& & \text{global reference}\\ & \mid \ell & & \text{literal}\\ & \mid e_1{e}_2& & \text{application}\\ & \mid \lambda x:\tau .e& & \text{term abstraction}\\ & \mid \Lambda \alpha .e& & \text{type abstraction}\\ & \mid e[\tau ]& & \text{type application}\\ & \mid \text{let}b\text{in}e& & \text{binding group}\\ & \mid \text{if}{e}_1\text{then}{e}_2\text{else}{e}_3& & \text{conditional}\\ & \mid p[\overline{\tau }](\overline{e})& & \text{primitive operation}\end{array}$$

Here $x$ and $g$ name local and global values, $\ell$ is a literal, and $p$ is a primitive. An overbar means a sequence, so $\overline{e}$ stands for the primitive’s operands in evaluation order. We leave source spans out of the notation, though the Rust representation keeps them for diagnostics.

The types and binding groups have their own grammar.

$$\begin{array}{rlrl}\tau & =\text{Int}\mid \text{Bool}\mid \text{Char}\mid \text{String}& & \text{base types}\\ & \mid \alpha & & \text{type variable}\\ & \mid {\tau }_1\to {\tau }_2& & \text{function type}\\ & \mid \forall \alpha .\tau & & \text{universal type}\\ b& =x:\tau =e& & \text{nonrecursive binding}\\ & \mid \text{rec}\{\overline{x:\tau =e}\}& & \text{recursive group}\end{array}$$

A recursive group’s names are in scope throughout its right-hand sides. Lint also checks that those right-hand sides describe functions, possibly wrapped in type abstractions. In a nonrecursive binding, the new name is available only in the body of the let.

Notice the two different lambdas. In $\Lambda \alpha .\lambda x:\alpha .x$, the capital $\Lambda$ chooses no value at all. It introduces the type parameter used by the ordinary $\lambda$. Applying this identity to a type and then a value gives $(\Lambda \alpha .\lambda x:\alpha .x)[\mathsf{Int}]42$. That’s the explicit version of the source-level id 42 we started with.

A Core expression is a Rust enum. Each variable and term binder carries an Id with its type, so lint can check the tree without rerunning inference.

#![allow(unused)]
fn main() {
pub use crate::core_type::Type;
use crate::{ast::Op, source::Span};
impl std::fmt::Display for Id {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} : {}", self.name, self.ty)
    }
}
#[derive(Clone, Debug, PartialEq, Eq)]
/// Immediate source values; strings are primitive UTF-8 values, not character lists.
pub enum Lit {
    Int(i64),
    Bool(bool),
    Char(char),
    String(String),
}
#[derive(Clone, Debug)]
/// System F Core makes type abstraction and instantiation explicit.
pub enum Expr {
    Var(Id),
    Global(Id),
    TyLam(u32, Box<Expr>),
    TyApp(Box<Expr>, Type),
    Lit(Lit),
    Lam(Id, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Let(BindGroup, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Prim(Op, Vec<Type>, Vec<Expr>, Span),
}
#[derive(Clone, Debug)]
/// A recursive binding is guaranteed to have a lambda right-hand side.
pub struct Bind {
    pub name: Id,
    pub rhs: Box<Expr>,
}
#[derive(Clone, Debug)]
/// An ordered component; recursive members are in scope in every right-hand side.
pub struct BindGroup {
    pub recursive: bool,
    pub binds: Vec<Bind>,
}
#[derive(Clone, Debug)]
/// Globals are initialized in dependency order, with explicit recursive components.
pub struct Program {
    pub groups: Vec<BindGroup>,
    pub main: Id,
}
impl std::fmt::Display for Expr {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Var(n) => write!(f, "{}", n.name),
            Self::Global(n) => write!(f, "@{}", n.name),
            Self::TyLam(v, b) => write!(f, "(type-lambda t{v} {b})"),
            Self::TyApp(a, t) => write!(f, "(type-app {a} {t})"),
            Self::Lit(l) => write!(f, "{l}"),
            Self::Lam(n, b) => write!(f, "(lambda {n} {b})"),
            Self::App(a, b) => write!(f, "(app {a} {b})"),
            Self::Let(group, body) => write!(f, "(let {group} in {body})"),
            Self::If(c, a, b) => write!(f, "(if {c} {a} {b})"),
            Self::Prim(op, _, args, _) => {
                write!(f, "(prim {}", op.text())?;
                for a in args {
                    write!(f, " {a}")?;
                }
                write!(f, ")")
            }
        }
    }
}
impl std::fmt::Display for Lit {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Int(n) => write!(f, "{n}"),
            Self::Bool(b) => {
                write!(f, "{}", if *b { "True" } else { "False" })
            }
            Self::Char(c) => {
                write!(f, "{}", crate::ast::quote(&c.to_string(), '\''))
            }
            Self::String(s) => write!(f, "{}", crate::ast::quote(s, '"')),
        }
    }
}
impl std::fmt::Display for BindGroup {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} {{", if self.recursive { "rec" } else { "nonrec" })?;
        for b in &self.binds {
            write!(f, " {} = {};", b.name, b.rhs)?;
        }
        write!(f, " }}")
    }
}
/// Independently typecheck System F Core after each Core-producing pass.
pub fn lint(program: &Program) -> Result<(), String> {
    crate::core_lint::lint(program)
}
impl Id {
    pub fn unique(&self) -> u32 {
        self.name.name.unique
    }
}
/// A Core identifier carries its independently checkable type.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Id {
    pub name: crate::names::Id,
    pub ty: Type,
}
}

The expression constructors distinguish term-level functions (Lam, App) from type-level abstraction and instantiation (TyLam, TyApp). Let keeps the recursive components produced by the renamer. Prim carries explicit type arguments, evaluated operands, and a source span for failures.

#![allow(unused)]
fn main() {
pub use crate::core_type::Type;
use crate::{ast::Op, source::Span};
/// A Core identifier carries its independently checkable type.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Id {
    pub name: crate::names::Id,
    pub ty: Type,
}
impl std::fmt::Display for Id {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} : {}", self.name, self.ty)
    }
}
#[derive(Clone, Debug, PartialEq, Eq)]
/// Immediate source values; strings are primitive UTF-8 values, not character lists.
pub enum Lit {
    Int(i64),
    Bool(bool),
    Char(char),
    String(String),
}
#[derive(Clone, Debug)]
/// A recursive binding is guaranteed to have a lambda right-hand side.
pub struct Bind {
    pub name: Id,
    pub rhs: Box<Expr>,
}
#[derive(Clone, Debug)]
/// An ordered component; recursive members are in scope in every right-hand side.
pub struct BindGroup {
    pub recursive: bool,
    pub binds: Vec<Bind>,
}
#[derive(Clone, Debug)]
/// Globals are initialized in dependency order, with explicit recursive components.
pub struct Program {
    pub groups: Vec<BindGroup>,
    pub main: Id,
}
impl std::fmt::Display for Expr {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Var(n) => write!(f, "{}", n.name),
            Self::Global(n) => write!(f, "@{}", n.name),
            Self::TyLam(v, b) => write!(f, "(type-lambda t{v} {b})"),
            Self::TyApp(a, t) => write!(f, "(type-app {a} {t})"),
            Self::Lit(l) => write!(f, "{l}"),
            Self::Lam(n, b) => write!(f, "(lambda {n} {b})"),
            Self::App(a, b) => write!(f, "(app {a} {b})"),
            Self::Let(group, body) => write!(f, "(let {group} in {body})"),
            Self::If(c, a, b) => write!(f, "(if {c} {a} {b})"),
            Self::Prim(op, _, args, _) => {
                write!(f, "(prim {}", op.text())?;
                for a in args {
                    write!(f, " {a}")?;
                }
                write!(f, ")")
            }
        }
    }
}
impl std::fmt::Display for Lit {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Int(n) => write!(f, "{n}"),
            Self::Bool(b) => {
                write!(f, "{}", if *b { "True" } else { "False" })
            }
            Self::Char(c) => {
                write!(f, "{}", crate::ast::quote(&c.to_string(), '\''))
            }
            Self::String(s) => write!(f, "{}", crate::ast::quote(s, '"')),
        }
    }
}
impl std::fmt::Display for BindGroup {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} {{", if self.recursive { "rec" } else { "nonrec" })?;
        for b in &self.binds {
            write!(f, " {} = {};", b.name, b.rhs)?;
        }
        write!(f, " }}")
    }
}
/// Independently typecheck System F Core after each Core-producing pass.
pub fn lint(program: &Program) -> Result<(), String> {
    crate::core_lint::lint(program)
}
impl Id {
    pub fn unique(&self) -> u32 {
        self.name.name.unique
    }
}
#[derive(Clone, Debug)]
/// System F Core makes type abstraction and instantiation explicit.
pub enum Expr {
    Var(Id),
    Global(Id),
    TyLam(u32, Box<Expr>),
    TyApp(Box<Expr>, Type),
    Lit(Lit),
    Lam(Id, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Let(BindGroup, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Prim(Op, Vec<Type>, Vec<Expr>, Span),
}
}

Binding groups hold typed names and right-hand sides. A program is an ordered list of these groups together with the entry point:

#![allow(unused)]
fn main() {
pub use crate::core_type::Type;
use crate::{ast::Op, source::Span};
/// A Core identifier carries its independently checkable type.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Id {
    pub name: crate::names::Id,
    pub ty: Type,
}
impl std::fmt::Display for Id {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} : {}", self.name, self.ty)
    }
}
#[derive(Clone, Debug, PartialEq, Eq)]
/// Immediate source values; strings are primitive UTF-8 values, not character lists.
pub enum Lit {
    Int(i64),
    Bool(bool),
    Char(char),
    String(String),
}
#[derive(Clone, Debug)]
/// System F Core makes type abstraction and instantiation explicit.
pub enum Expr {
    Var(Id),
    Global(Id),
    TyLam(u32, Box<Expr>),
    TyApp(Box<Expr>, Type),
    Lit(Lit),
    Lam(Id, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Let(BindGroup, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Prim(Op, Vec<Type>, Vec<Expr>, Span),
}
#[derive(Clone, Debug)]
/// An ordered component; recursive members are in scope in every right-hand side.
pub struct BindGroup {
    pub recursive: bool,
    pub binds: Vec<Bind>,
}
#[derive(Clone, Debug)]
/// Globals are initialized in dependency order, with explicit recursive components.
pub struct Program {
    pub groups: Vec<BindGroup>,
    pub main: Id,
}
impl std::fmt::Display for Expr {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Var(n) => write!(f, "{}", n.name),
            Self::Global(n) => write!(f, "@{}", n.name),
            Self::TyLam(v, b) => write!(f, "(type-lambda t{v} {b})"),
            Self::TyApp(a, t) => write!(f, "(type-app {a} {t})"),
            Self::Lit(l) => write!(f, "{l}"),
            Self::Lam(n, b) => write!(f, "(lambda {n} {b})"),
            Self::App(a, b) => write!(f, "(app {a} {b})"),
            Self::Let(group, body) => write!(f, "(let {group} in {body})"),
            Self::If(c, a, b) => write!(f, "(if {c} {a} {b})"),
            Self::Prim(op, _, args, _) => {
                write!(f, "(prim {}", op.text())?;
                for a in args {
                    write!(f, " {a}")?;
                }
                write!(f, ")")
            }
        }
    }
}
impl std::fmt::Display for Lit {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Int(n) => write!(f, "{n}"),
            Self::Bool(b) => {
                write!(f, "{}", if *b { "True" } else { "False" })
            }
            Self::Char(c) => {
                write!(f, "{}", crate::ast::quote(&c.to_string(), '\''))
            }
            Self::String(s) => write!(f, "{}", crate::ast::quote(s, '"')),
        }
    }
}
impl std::fmt::Display for BindGroup {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} {{", if self.recursive { "rec" } else { "nonrec" })?;
        for b in &self.binds {
            write!(f, " {} = {};", b.name, b.rhs)?;
        }
        write!(f, " }}")
    }
}
/// Independently typecheck System F Core after each Core-producing pass.
pub fn lint(program: &Program) -> Result<(), String> {
    crate::core_lint::lint(program)
}
impl Id {
    pub fn unique(&self) -> u32 {
        self.name.name.unique
    }
}
#[derive(Clone, Debug)]
/// A recursive binding is guaranteed to have a lambda right-hand side.
pub struct Bind {
    pub name: Id,
    pub rhs: Box<Expr>,
}
pub use crate::core_type::Type;
use crate::{ast::Op, source::Span};
/// A Core identifier carries its independently checkable type.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Id {
    pub name: crate::names::Id,
    pub ty: Type,
}
impl std::fmt::Display for Id {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} : {}", self.name, self.ty)
    }
}
#[derive(Clone, Debug, PartialEq, Eq)]
/// Immediate source values; strings are primitive UTF-8 values, not character lists.
pub enum Lit {
    Int(i64),
    Bool(bool),
    Char(char),
    String(String),
}
#[derive(Clone, Debug)]
/// System F Core makes type abstraction and instantiation explicit.
pub enum Expr {
    Var(Id),
    Global(Id),
    TyLam(u32, Box<Expr>),
    TyApp(Box<Expr>, Type),
    Lit(Lit),
    Lam(Id, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Let(BindGroup, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Prim(Op, Vec<Type>, Vec<Expr>, Span),
}
#[derive(Clone, Debug)]
/// A recursive binding is guaranteed to have a lambda right-hand side.
pub struct Bind {
    pub name: Id,
    pub rhs: Box<Expr>,
}
#[derive(Clone, Debug)]
/// Globals are initialized in dependency order, with explicit recursive components.
pub struct Program {
    pub groups: Vec<BindGroup>,
    pub main: Id,
}
impl std::fmt::Display for Expr {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Var(n) => write!(f, "{}", n.name),
            Self::Global(n) => write!(f, "@{}", n.name),
            Self::TyLam(v, b) => write!(f, "(type-lambda t{v} {b})"),
            Self::TyApp(a, t) => write!(f, "(type-app {a} {t})"),
            Self::Lit(l) => write!(f, "{l}"),
            Self::Lam(n, b) => write!(f, "(lambda {n} {b})"),
            Self::App(a, b) => write!(f, "(app {a} {b})"),
            Self::Let(group, body) => write!(f, "(let {group} in {body})"),
            Self::If(c, a, b) => write!(f, "(if {c} {a} {b})"),
            Self::Prim(op, _, args, _) => {
                write!(f, "(prim {}", op.text())?;
                for a in args {
                    write!(f, " {a}")?;
                }
                write!(f, ")")
            }
        }
    }
}
impl std::fmt::Display for Lit {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Int(n) => write!(f, "{n}"),
            Self::Bool(b) => {
                write!(f, "{}", if *b { "True" } else { "False" })
            }
            Self::Char(c) => {
                write!(f, "{}", crate::ast::quote(&c.to_string(), '\''))
            }
            Self::String(s) => write!(f, "{}", crate::ast::quote(s, '"')),
        }
    }
}
impl std::fmt::Display for BindGroup {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} {{", if self.recursive { "rec" } else { "nonrec" })?;
        for b in &self.binds {
            write!(f, " {} = {};", b.name, b.rhs)?;
        }
        write!(f, " }}")
    }
}
/// Independently typecheck System F Core after each Core-producing pass.
pub fn lint(program: &Program) -> Result<(), String> {
    crate::core_lint::lint(program)
}
impl Id {
    pub fn unique(&self) -> u32 {
        self.name.name.unique
    }
}
#[derive(Clone, Debug)]
/// An ordered component; recursive members are in scope in every right-hand side.
pub struct BindGroup {
    pub recursive: bool,
    pub binds: Vec<Bind>,
}
pub use crate::core_type::Type;
use crate::{ast::Op, source::Span};
/// A Core identifier carries its independently checkable type.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Id {
    pub name: crate::names::Id,
    pub ty: Type,
}
impl std::fmt::Display for Id {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} : {}", self.name, self.ty)
    }
}
#[derive(Clone, Debug, PartialEq, Eq)]
/// Immediate source values; strings are primitive UTF-8 values, not character lists.
pub enum Lit {
    Int(i64),
    Bool(bool),
    Char(char),
    String(String),
}
#[derive(Clone, Debug)]
/// System F Core makes type abstraction and instantiation explicit.
pub enum Expr {
    Var(Id),
    Global(Id),
    TyLam(u32, Box<Expr>),
    TyApp(Box<Expr>, Type),
    Lit(Lit),
    Lam(Id, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Let(BindGroup, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Prim(Op, Vec<Type>, Vec<Expr>, Span),
}
#[derive(Clone, Debug)]
/// A recursive binding is guaranteed to have a lambda right-hand side.
pub struct Bind {
    pub name: Id,
    pub rhs: Box<Expr>,
}
#[derive(Clone, Debug)]
/// An ordered component; recursive members are in scope in every right-hand side.
pub struct BindGroup {
    pub recursive: bool,
    pub binds: Vec<Bind>,
}
impl std::fmt::Display for Expr {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Var(n) => write!(f, "{}", n.name),
            Self::Global(n) => write!(f, "@{}", n.name),
            Self::TyLam(v, b) => write!(f, "(type-lambda t{v} {b})"),
            Self::TyApp(a, t) => write!(f, "(type-app {a} {t})"),
            Self::Lit(l) => write!(f, "{l}"),
            Self::Lam(n, b) => write!(f, "(lambda {n} {b})"),
            Self::App(a, b) => write!(f, "(app {a} {b})"),
            Self::Let(group, body) => write!(f, "(let {group} in {body})"),
            Self::If(c, a, b) => write!(f, "(if {c} {a} {b})"),
            Self::Prim(op, _, args, _) => {
                write!(f, "(prim {}", op.text())?;
                for a in args {
                    write!(f, " {a}")?;
                }
                write!(f, ")")
            }
        }
    }
}
impl std::fmt::Display for Lit {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Int(n) => write!(f, "{n}"),
            Self::Bool(b) => {
                write!(f, "{}", if *b { "True" } else { "False" })
            }
            Self::Char(c) => {
                write!(f, "{}", crate::ast::quote(&c.to_string(), '\''))
            }
            Self::String(s) => write!(f, "{}", crate::ast::quote(s, '"')),
        }
    }
}
impl std::fmt::Display for BindGroup {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} {{", if self.recursive { "rec" } else { "nonrec" })?;
        for b in &self.binds {
            write!(f, " {} = {};", b.name, b.rhs)?;
        }
        write!(f, " }}")
    }
}
/// Independently typecheck System F Core after each Core-producing pass.
pub fn lint(program: &Program) -> Result<(), String> {
    crate::core_lint::lint(program)
}
impl Id {
    pub fn unique(&self) -> u32 {
        self.name.name.unique
    }
}
#[derive(Clone, Debug)]
/// Globals are initialized in dependency order, with explicit recursive components.
pub struct Program {
    pub groups: Vec<BindGroup>,
    pub main: Id,
}
}

This chapter still has If. Datatype constructors and pattern matches arrive in Chapter 11, and flat cases and join points arrive in Chapter 16. The smaller enum here lets us establish typed elaboration and lint before adding those forms.

Recording inference results

Renamed expressions now have stable node numbers. The checker records the fresh type arguments used at each variable occurrence, the scheme of each binding, and the monotype of each lambda parameter. Before returning, it zonks all these types, so elaboration never needs access to the mutable metavariable store.

A variable occurrence inferred inside a recursive group initially sees a provisional monotype. Once the component is generalized, elaboration instantiates its recursive Core references at the corresponding generalized variables. Ordinary occurrences use the fresh arguments recorded during inference.

Elaborating polymorphism

Each generalized metavariable receives a fresh Core type identity. Binder types wrap the converted monotype in Forall. Right-hand sides wrap their terms in the matching TyLams. Local schemes can still mention type variables bound by an outer function’s abstraction.

#![allow(unused)]
fn main() {
fn group(
    &mut self,
    group: &renamed::BindGroup,
    outer: &BTreeMap<u32, u32>,
    global: bool,
) -> BindGroup {
    for binding in &group.binds {
        self.binder(
            binding.id.clone(),
            &self.typed.schemes[&binding.id],
            outer,
            global,
        );
    }
    let binds = group
        .binds
        .iter()
        .map(|binding| {
            let binder = self.binders[&binding.id].clone();
            let mut variables = outer.clone();
            variables.extend(binder.quantifiers.iter().copied());
            let mut rhs = self.expression(&binding.rhs, &variables);
            for (_, variable) in binder.quantifiers.iter().rev() {
                rhs = Expr::TyLam(*variable, Box::new(rhs));
            }
            Bind {
                name: binder.id,
                rhs: Box::new(rhs),
            }
        })
        .collect();
    BindGroup {
        recursive: group.recursive,
        binds,
    }
}
}

Occurrences gain TyApps, and lambda parameters carry their converted types. Core distinguishes global references from local variables. Its binder annotations are checked against the declared environment, so attaching a plausible-looking type to an otherwise wrong occurrence cannot evade lint.

An internal variable absent from every enclosing scheme needs a closed witness: (\f -> 42) (\x -> x) is an example. We use Int for these erased annotations. This does not default source expressions or resolve ambiguous class constraints.

Independent lint

The checker maintains term and type scopes, plus sets of binder identities already used. It checks arrow applications, primitive saturation, conditional branches, recursive function groups, and binder annotations. These are the explicit type abstraction and application rules:

#![allow(unused)]
fn main() {
Expr::TyLam(variable, body) => {
    if !self.seen_types.insert(*variable) {
        return Err(format!(
            "duplicate Core type binder t{variable}"
        ));
    }
    self.types.insert(*variable);
    let body = self.expression(body)?;
    self.types.remove(variable);
    Ok(Type::Forall(*variable, Box::new(body)))
}
Expr::TyApp(fun, argument) => {
    self.well_formed(argument)?;
    let function = self.expression(fun)?;
    let Type::Forall(variable, body) = function else {
        return Err(format!(
            "Core type application of non-polymorphic type {function}"
        ));
    };
    Ok(body.substitute(variable, argument))
}
}

Type application substitutes into the quantified body. Substitution must avoid capturing a free type variable in the argument, even for Core terms constructed outside our elaborator. The implementation freshens a conflicting binder:

#![allow(unused)]
fn main() {
pub fn substitute(&self, variable: u32, replacement: &Type) -> Type {
    match self {
        Self::Var(v) if *v == variable => replacement.clone(),
        Self::Arrow(a, b) => Self::arrow(
            a.substitute(variable, replacement),
            b.substitute(variable, replacement),
        ),
        Self::Forall(v, _) if *v == variable => self.clone(),
        Self::Forall(v, body) => {
            let (v, body) = if replacement.free().contains(v) {
                let fresh = self
                    .largest()
                    .max(replacement.largest())
                    .max(variable)
                    .checked_add(1)
                    .expect("type variable supply exhausted");
                (fresh, body.substitute(*v, &Self::Var(fresh)))
            } else {
                (*v, *body.clone())
            };
            Self::Forall(
                v,
                Box::new(body.substitute(variable, replacement)),
            )
        }
        _ => self.clone(),
    }
}
}

Type equality is alpha equivalence, so two forall types may use different fresh identities and still denote the same type. In contrast, a free type variable must refer to the same enclosing binder.

#![allow(unused)]
fn main() {
pub fn lint(program: &Program) -> Result<(), String> {
    let mut checker = Checker::default();
    for group in &program.groups {
        checker.group(group, true)?;
    }
    checker.expression(&Expr::Global(program.main.clone()))?;
    Ok(())
}
}

Aside. A compiler bug that drops TyApp from an application of polymorphic identity produces Core application of non-function type forall t0. t0 -> t0. The source program may be valid. The generated Core is not. The malformed-Core tests check this failure directly, without rerunning source inference.

Erasure and strict execution

TyLam and TyApp do not allocate runtime objects. The interpreter steps through them without substituting runtime values. This is erasure, rather than a separate runtime evaluation strategy for System F.

In particular, a type abstraction does not delay a strict initializer. The unused polymorphic binding below still fails before main is selected:

unused = (\x -> \y -> y) (div 1 0)

main = 42

Chapter 18 introduces an explicit erased IR. Corpus runs already enable --lint.

Running It

$ cd crates/ch10_core
$ cargo run -q -- run tests/programs/core/self-instantiation.fun --lint
42
$ cargo run -q -- dump --pass=core --no-prelude tests/programs/layout/signature.fun
nonrec { id#0 : forall t0. t0 -> t0 = (type-lambda t0 (lambda x#2 : t0 x#2)); }
nonrec { main#1 : Int = (app (type-app @id#0 Int) 42); }
$ cargo test -p ch10_core --test system_f

For a useful experiment, remove a type application from a small Core term and run lint. The source checker has no role in this test. We’re deliberately feeding the second checker a mistake that only the compiler could have made. It should reject the term before evaluation.

Exercises

1. Introductory. identify every type abstraction and type application in the Core dump for id id 42.
2. Intermediate. Explain why a captured outer type variable remains free in a local binding’s scheme but is bound in the complete Core program.
3. Intermediate. Construct a malformed Core primitive call with the right number of arguments but the wrong operand type.
4. Advanced. Demonstrate a capture bug in type substitution if freshening is removed, then explain why alpha equivalence alone does not repair it.

Further Reading

Girard’s thesis and Reynolds’s paper are the original sources for explicit polymorphism [Girard (1972); Reynolds (1974)]. Pierce develops System F’s typing and substitution rules (Pierce 2002).

Chapter 11: Datatypes and Pattern Matching

New files

• src/data.rs
• src/syn.rs
• src/desugar.rs

Changed files

• src/typecheck.rs
• src/core.rs
• src/elaborate.rs
• src/ast.rs
• src/core_lint.rs
• src/core_type.rs
• src/eval.rs
• src/fixity.rs
• src/layout.rs
• src/lexer.rs
• src/lib.rs
• src/main.rs
• src/parse.rs
• src/rename.rs
• src/renamed.rs
• src/session.rs
• src/types.rs

Motivation

Integers and functions have taken us a long way, but it’s time to build some proper data structures. A binary tree can be empty or contain a value and two subtrees. A lookup can fail or return a result. Algebraic datatypes let us say these things directly, without inventing special values to mean “nothing here”.

Pattern matching gives us an equally direct way to take the values apart. The shape of the data becomes the shape of the program. This is one of the beautiful parts of functional programming, and we’ll use it constantly from here on.

We’ll first implement matching by trying patterns in source order. That gives us a clear account of what a match means. In Chapter 16 we’ll turn the same matches into decision trees suitable for native code.

The Language, Now

Declarations introduce nominal types and their constructors. Constructor arguments are strict, and constructors can be passed around as curried functions.

data Tree a = Empty | Node (Tree a) a (Tree a)

size Empty = 0
size (Node left _ right) = 1 + size left + size right

main = size (Node Empty 42 Empty)

Read size beside the datatype. Empty contributes zero. A Node contributes one, plus the sizes of its two children. The definition follows the data almost word for word. That’s beautiful, and it scales to much more interesting trees.

We can mirror a tree just as directly.

data Tree a = Empty | Node (Tree a) a (Tree a)

mirror Empty = Empty
mirror (Node left x right) = Node (mirror right) x (mirror left)

main = mirror (Node Empty 1 (Node Empty 2 Empty))

Notice that mirror never examines x. Its type is Tree a -> Tree a, so it works for trees of any element type. The recursion changes the shape while leaving the values alone.

Equations may have nested constructor patterns, literals, wildcards, and as-patterns. Lists, pairs, triples, and unit have dedicated syntax. Guards must have type Bool. If all guards fail, matching continues with the next equation.

select all@(x : xs) | x < 0 = xs
select all = all

main = select [-1,2,3]

A where block belongs to its entire equation, including every guard. A case alternative may also have guards and a where block. Pattern lambdas and strict, non-recursive pattern bindings work as well: let (x,y) = (20,22) in x + y. Types remain first-order here. A datatype parameter has kind *, so Tree Int is valid but applying a parameter as in f Int waits for Chapter 13.

The initial Prelude is embedded from this actual Fun source:

data Bool = False | True

data Ordering = LT | EQ | GT

data Maybe a = Nothing | Just a

data Either a b = Left a | Right b

data [] a = [] | (:) a [a]

data () = ()

data (,) a b = (,) a b

data (,,) a b c = (,,) a b c

Theory

A datatype declaration supplies a polymorphic scheme for each constructor. For example, Node has type Tree a -> a -> Tree a -> Tree a, quantified over a. Each occurrence instantiates that scheme with fresh metavariables, just as a polymorphic function occurrence does [Marlow (2010); Pierce (2002)].

For a constructor with instantiated field types, a pattern judgment returns the bindings introduced by its subpatterns:

$$\frac{K:{\tau }_1\to {\tau }_2\to T\Gamma ⊢p_1:{\tau }_1\Rightarrow {\Delta }_1\Gamma ⊢p_2:{\tau }_2\Rightarrow {\Delta }_2}{\Gamma ⊢K{p}_1{p}_2:T\Rightarrow {\Delta }_1,{\Delta }_2}\text{(Constructor pattern)}$$

The combined pattern environment must not bind a name twice. Each row is checked against the same scrutinee types, and every successful right-hand side must have the same result type. Guards additionally unify with Bool.

Fun evaluates fields before constructing a value. A failed match raises a runtime error. There are no lazy patterns or suspended constructor fields. Exhaustiveness and redundancy warnings require a separate analysis. They arrive with match compilation (Maranget 2007).

Implementation

Declaring names before checking fields

data.rs first allocates every type head, then converts constructor fields. This permits mutually recursive datatypes. The immutable table stores each type’s arity, each constructor’s scheme, and declaration-order tags. Duplicate names, unbound field variables, and incorrect type arities are diagnosed before expression inference begins.

The renamer resolves constructor names in expressions and patterns separately from ordinary variables. Pattern variables receive fresh identities for each row. Its scope then contains those variables and the row’s local declarations while visiting both guards and right-hand sides.

Lowering syntax into Syn

desugar.rs introduces an explicit pass between renaming and inference. Lists and tuples become constructor applications. if becomes a two-row match on True and False. Infix && and || first become conditionals. As first-class values those operators are ordinary eta-expanded functions, whose arguments are evaluated by call-by-value application.

A single equation containing only variable patterns can use ordinary lambdas and lets. Other equations become a lambda for each argument followed by a match:

#![allow(unused)]
fn main() {
let params: Vec<_> = (0..rows[0].patterns.len())
    .map(|_| self.sess.fresh_id("$match"))
    .collect();
let scruts = params
    .iter()
    .map(|id| self.node(Kind::Var(id.clone()), span))
    .collect();
let mut body = self.node(Kind::Match(scruts, rows), span);
for id in params.into_iter().rev() {
    body = self.node(Kind::Lam(id, Box::new(body)), span);
}
body
}

Strict pattern bindings use one checked bundle of their bound values, represented by nested pairs, followed by projections. The right-hand side is evaluated once. Its newly bound names are hidden while renaming that right-hand side, so an outer binding of the same spelling remains accessible. An unused top-level pattern binding still executes and can fail.

Inferring constructor patterns

The checker instantiates a constructor scheme, separates its field arrows from its result type, and unifies the result with the scrutinee. It then checks each subpattern against the corresponding instantiated field:

#![allow(unused)]
fn main() {
PatKind::Con(id, patterns) => {
    let info = self.data.con(id).clone();
    if patterns.len() != info.fields.len() {
        return Err(Diagnostic::error(
            ErrorCode::Mismatch,
            format!(
                "{} expects {} pattern fields",
                id.name,
                info.fields.len()
            ),
            pattern.span,
        ));
    }
    let mut ty = self.instantiate(&info.scheme);
    let mut fields = Vec::new();
    for _ in patterns {
        let Type::Arrow(a, b) = ty else {
            unreachable!("constructor arity")
        };
        fields.push(*a);
        ty = *b;
    }
    self.unify(expected, &ty, &site)?;
    for (pattern, ty) in patterns.iter().zip(fields) {
        self.pattern(env, pattern, &ty)?;
    }
}
}

Pattern variables enter the row environment monomorphically. Local bindings retain ordinary let-polymorphism. The checker records expression and pattern-binder types alongside the instantiation metadata already needed by System F elaboration.

Extending Core and lint

Elaboration eta-expands constructor values into lambdas whose bodies are saturated Con nodes. Strict lets evaluate match scrutinees once and in source order. Core keeps nested patterns until the decision-tree compiler is introduced:

#![allow(unused)]
fn main() {
/// Nested patterns remain until the decision-tree compiler in Chapter 16.
#[derive(Clone, Debug)]
pub enum Pat {
    Var(Id),
    Wild,
    As(Id, Box<Pat>),
    Con(crate::data::ConId, Vec<Pat>),
    Lit(Lit),
}

/// A guarded row falls through when all its Boolean tests fail.
#[derive(Clone, Debug)]
pub enum RowBody {
    Plain(Box<Expr>),
    Guarded(Vec<(Expr, Expr)>),
}

/// Row-local declarations run after patterns match and are shared by the guards.
#[derive(Clone, Debug)]
pub struct Row {
    pub pats: Vec<Pat>,
    pub locals: Vec<BindGroup>,
    pub body: RowBody,
    pub span: Span,
}

/// Scrutinees name strict preceding lets; the match records its result type and failure site.
#[derive(Clone, Debug)]
pub struct Match {
    pub scruts: Vec<Id>,
    pub rows: Vec<Row>,
    pub result: Type,
    pub span: Span,
}
}

Lint independently checks constructor type arguments, field counts and field types. For a constructor pattern it instantiates the declaration under the scrutinee’s type arguments, then checks each binder. Guards must be Boolean, and every row must produce the declared match result. Malformed-Core tests exercise these checks without asking the surface inferencer to validate their inputs.

Executing rows

The interpreter evaluates constructor fields left to right. Matching already evaluated values recursively tests constructors and literals, extending a private row environment with variables and as-patterns:

#![allow(unused)]
fn main() {
fn matches_pattern(p: &core::Pat, v: &Value, env: &mut Env) -> bool {
    match p {
        core::Pat::Wild => true,
        core::Pat::Var(id) => {
            env.push((id.clone(), v.clone()));
            true
        }
        core::Pat::As(id, p) => {
            env.push((id.clone(), v.clone()));
            matches_pattern(p, v, env)
        }
        core::Pat::Lit(l) => matches!(v,Value::Lit(actual) if l==actual),
        core::Pat::Con(id, ps) => match v {
            Value::Con(actual, vs)
                if id == actual && ps.len() == vs.len() =>
            {
                ps.iter().zip(vs).all(|(p, v)| matches_pattern(p, v, env))
            }
            _ => false,
        },
    }
}
}

A failed pattern discards that environment and tries the next row. A successful pattern evaluates its where groups once, then tests guards in order. If all fail, execution continues with the next row. Exhausting the rows reports fun: pattern match failure at FILE:LINE:COL and exits with status 1.

The value printer uses constructor precedence, so a nested application prints as Just (Left 3). Lists and tuples use their surface notation. A character list prints as ['a','b'], while primitive strings keep double quotes.

Running It

$ cd crates/ch11_data
$ cargo run -q -- run tests/programs/data/tree.fun --lint
(True,False)
$ cargo run -q -- dump --pass=syn tests/programs/data/bool-data.fun
nonrec { not#9 = (lambda $match#11 (match $match#11 [ (True) -> False ] [ (False) -> True ])); }
nonrec { main#10 = (app (app (,) (app not#9 True)) (app not#9 False)); }
$ cargo test --test data

Guard fallthrough is worth experimenting with. Make the first pattern match but its guard fail, then check that the next equation runs. Also try an unused top-level pattern binding that fails. Strict evaluation means “unused” doesn’t make the match disappear. These examples exercise the parts that an ordinary successful tree traversal might miss.

Exercises

1. Introductory. define a binary tree mirror function and test it on an asymmetric tree.
2. Intermediate. Explain the type errors from a constructor pattern with too few fields and from two equations returning different types.
3. Intermediate. Write two guards that fall through to a later equation. Move their shared computation into where and inspect the Syn dump.
4. Advanced. Compare strict pattern binding with Haskell’s ordinary pattern binding. Construct a program whose termination or error behavior differs.
5. Advanced. Design a lint test that swaps two differently typed constructor fields while preserving the field count.

Further Reading

The Haskell Report specifies datatype declarations, patterns, guards, and local scopes (Simon Marlow 2010). Pierce develops the connection between data introductions and eliminations (Pierce 2002). Maranget’s papers explain the later steps: warning analysis and decision-tree compilation [Maranget (2007); Maranget (2008)].

Chapter 12: Records

New files

None.

Changed files

• src/typecheck.rs
• src/data.rs
• src/lexer.rs
• src/elaborate.rs
• src/ast.rs
• src/core.rs
• src/desugar.rs
• src/eval.rs
• src/fixity.rs
• src/format.rs
• src/main.rs
• src/parse.rs
• src/rename.rs
• src/renamed.rs

Motivation

What does the third argument to a constructor mean? With a small point or pair, you can probably remember. With a configuration value containing half a dozen integers, it becomes a small memory test every time you read the code. Let’s give those fields names.

Fun’s records build on the datatypes we already have. We’ll use dot syntax to read a field and require every record type to have just one constructor. This avoids two awkward properties of traditional Haskell selectors. Access cannot fail because we picked the wrong constructor, and field names don’t consume ordinary function names. Two record types can both have an x field [Marlow (2010); Mitchell & Fletcher (n.d.)].

The interesting work is in inference. When we see p.x, how much do we know about p? We’ll arrange for information elsewhere in the expression to help answer that question.

The Language, Now

data Point = Point { x :: Int, y :: Int }

move p = p { x = p.x + 1 }

main = move (Point { y = 4, x = 3 })

Construction must supply every field exactly once. Its expressions run in written order, even when that differs from declaration order. Positional construction and patterns remain available. A record pattern may omit fields, which become wildcards: Point { x = n } binds only the first coordinate.

Projection and update bind more tightly than application. Thus f p.x means f (p.x), and f p { x = 3 } means f (p { x = 3 }). The section (.x) is shorthand for a lambda. Chained access such as shape.origin.x projects twice. An update preserves the receiver’s complete type, including its type arguments.

data Label = Label { x :: String }

coordinate :: Point -> Int
coordinate p = p.x

The signature identifies which x is meant. The parenthesized expression annotation (p :: Point).x works too. If only one record declares a field, the checker can infer its receiver type without an annotation.

Theory

Two declarations with identical fields still describe different types. That is what nominal means here. A Point doesn’t become some other record merely because both happen to contain x and y. A structural or row-polymorphic system could instead let a function accept any record with the fields it needs (Pierce 2002). We’re choosing the nominal design so field access can resolve to a particular constructor and slot before runtime.

Projection introduces a wanted constraint linking the receiver and result types:

$$\frac{\Gamma ⊢e:\tau \mathsf{Has}(\tau ,x,\alpha )}{\Gamma ⊢e.x:\alpha }\text{(Projection)}$$

Has is an internal checking obligation. It is never generalized into a scheme. For a unique field name, the checker immediately unifies the receiver with that record type, using fresh parameters. Otherwise it waits for the receiver’s nominal head to become known. Before generalizing a binding group it repeats resolution to a fixpoint. Any remaining field wanted produces E0245 and an annotation hint.

GHC’s record-dot proposal is useful prior art for the surface syntax. Its HasField mechanism supports a different form of overloaded access. Fun’s field solver always chooses a concrete nominal record before elaboration (Mitchell and Fletcher, n.d.).

Implementation

Classifying the dot

Whitespace is significant for this token. f.g means projection, while f . g uses the ordinary composition operator. The post-pass compares original token spans before trivia capture and layout can obscure adjacency:

#![allow(unused)]
fn main() {
/// Classify dot adjacency before trivia capture and layout can erase spacing.
fn projection_dots(
    file: FileId,
    tokens: &mut [Spanned],
    errors: &mut Vec<Diagnostic>,
) {
    for i in 1..tokens.len().saturating_sub(1) {
        if !matches!(&tokens[i].1,Token::Operator(op) if op==".")
            || tokens[i].2 != tokens[i + 1].0
            || !matches!(tokens[i + 1].1, Token::Ident(_))
        {
            continue;
        }
        if tokens[i - 1].2 != tokens[i].0 {
            continue;
        }
        if tokens[i - 1].1 == Token::Left {
            tokens[i].1 = Token::ProjSection;
            if !matches!(
                tokens[i + 2..].iter().find(|(_, t, _)| !matches!(
                    t,
                    Token::LineComment(_) | Token::BlockComment(_)
                )),
                Some((_, Token::Right, _))
            ) {
                errors.push(Diagnostic::error(
                    ErrorCode::ProjectionDot,
                    "a projection section must have the form (.field)",
                    Span::new(file, tokens[i].0, tokens[i].2),
                ));
            }
        } else if matches!(
            tokens[i - 1].1,
            Token::Ident(_)
                | Token::Right
                | Token::BracketClose
                | Token::Close
                | Token::Int(_)
                | Token::Char(_)
                | Token::String(_)
        ) {
            tokens[i].1 = Token::Proj;
        }
    }
}
}

The token preceding a projection must be an identifier, literal, or closing delimiter. A dot immediately following ( and preceding a variable identifier is a projection-section token. Other dots remain operators. In particular, the same rule leaves x .y as an ordinary operator occurrence.

E0004 diagnoses malformed recognized sections such as (.x y). The formatter keeps dot and label tokens adjacent and moves attached comments outside that sequence. Both decisions are tested because a whitespace-only rewrite could otherwise change the program’s meaning.

Keeping field metadata nominal

Each record constructor retains field labels alongside its field types. Datatype validation rejects a record mixed with other constructors (E0240) and repeated declaration labels (E0104). Named construction checks missing, duplicate, and unknown fields with E0241, E0242, and E0243 respectively.

Record patterns are converted to positional constructor patterns during renaming. The renamer looks up each label’s slot and fills every omitted slot with a wildcard. Consequently the pattern checker and Core lint need no new record-pattern rule. No field is added to the value environment.

Solving field obligations

A wanted records the receiver type, label, fresh field type, source site, and inference level. Sites distinguish individual fields within an update:

#![allow(unused)]
fn main() {
/// A field site's position distinguishes updates of several named slots.
pub type FieldSite = (u32, usize);

/// Field constraints never enter a polymorphic scheme.
#[derive(Clone)]
struct FieldWanted {
    record: Type,
    label: String,
    field: Type,
    site: FieldSite,
    span: crate::source::Span,
    level: u32,
}
}

The projection inference branch creates that obligation and returns its fresh result type. Successful resolution later unifies the result with the instantiated field declaration:

#![allow(unused)]
fn main() {
Kind::Project(e, label) => {
    let record = self.infer(env, e)?;
    let field = self.fresh();
    self.field(
        record,
        label.clone(),
        field.clone(),
        (expr.node, 0),
        expr,
    )?;
    Ok(field)
}
}

solve_field either identifies a constructor and field slot, reports a type with no such field (E0244), or leaves an unknown receiver unresolved. The surrounding loop repeats because one resolved field may identify the receiver of another:

#![allow(unused)]
fn main() {
fn solve_fields(
    &mut self,
    complete: Option<u32>,
) -> Result<(), Diagnostic> {
    loop {
        let pending = std::mem::take(&mut self.wanted);
        let count = pending.len();
        for wanted in pending {
            if !self.solve_field(&wanted)? {
                self.wanted.push(wanted);
            }
        }
        if self.wanted.len() == count {
            break;
        }
    }
    if let Some(level) = complete
        && let Some(w) = self.wanted.iter().find(|w| w.level > level)
    {
        let mut error = Diagnostic::error(
            ErrorCode::AmbiguousField,
            format!("ambiguous field access .{}", w.label),
            w.span,
        );
        error.notes.push(
            "add a type annotation to identify the record type".into(),
        );
        return Err(error);
    }
    Ok(())
}
}

Signature-directed checking supplies lambda parameter types before their bodies are visited. This matters when a local binding accesses a shared field. The outer signature must be available before that local group is generalized. The existing rigid signature check still rejects an annotation that claims too much polymorphism.

Elaborating strict construction and access

Field order in source is independent of field order in memory. Construction therefore introduces a strict let for each supplied expression, then builds a constructor using those variables in declaration order:

#![allow(unused)]
fn main() {
Kind::Record(id, fields) => {
    let declaration =
        self.constructors[id.index as usize].clone();
    let arguments = self.typed.instantiations[&expr.node]
        .iter()
        .map(|t| convert(t, variables))
        .collect::<Vec<_>>();
    let mut values = vec![Expr::Lit(Lit::Int(0)); fields.len()];
    let mut locals = vec![];
    for (label, e) in fields {
        let index = declaration
            .labels
            .as_ref()
            .unwrap()
            .iter()
            .position(|n| n == label)
            .unwrap();
        let parameter = Id {
            name: self.sess.fresh_id("$field"),
            ty: instantiate(
                &declaration.fields[index],
                &declaration.parameters,
                &arguments,
            ),
        };
        locals.push(BindGroup {
            recursive: false,
            binds: vec![Bind {
                name: parameter.clone(),
                rhs: Box::new(self.expression(e, variables)),
            }],
        });
        values[index] = Expr::Var(parameter);
    }
    let mut body = Expr::Con(id.clone(), arguments, values);
    for local in locals.into_iter().rev() {
        body = Expr::Let(local, Box::new(body));
    }
    body
}
}

Projection evaluates its receiver once, matches its sole constructor, and returns the selected field binder. Update uses the same match, evaluates replacement expressions in source order, and rebuilds the constructor with unchanged fields in their original slots. The result type equals the receiver type, so an update cannot turn Box Int into Box Bool.

Core sees only constructs introduced in Chapter 11. Independent lint checks their types, and the interpreter executes ordinary matches and constructors. Its value printer consults the constructor’s labels to print Point {x = 3, y = 4} in declaration order. Later native projection will become a field load.

Running It

$ cd crates/ch12_records
$ cargo run -q -- run tests/programs/records/nested.fun --lint
(3,Outer {inner = P {x = 10, y = 4}})
$ cargo run -q -- dump --pass=types tests/programs/records/shared-signature.fun
main : Int
$ cargo test --test records

Try giving a second record an x field and remove the annotation from a projection. The ambiguity error shows why field names alone aren’t always enough. Another useful experiment is to put different errors in a receiver and an updated field. The first error should follow source evaluation order, even though the final fields are stored in declaration order.

Exercises

1. Introductory. define a polymorphic Box a record and infer the type of its projection section.
2. Intermediate. Add another record with the same field label, observe the ambiguity error, and resolve it with a signature.
3. Intermediate. Explain why another uniquely named field can disambiguate an earlier unresolved access in the same binding group.
4. Advanced. Write a construction whose source field order differs from its declaration order and whose first failure reveals the evaluation order.
5. Advanced. Identify the parts of inference and generalization that would need to change to support row-polymorphic access. Do not add that feature here.

Further Reading

The Haskell Report describes traditional record construction, update, and selector functions (Simon Marlow 2010). GHC proposal 282 motivates record-dot syntax and its relationship to overloaded field access (Mitchell and Fletcher, n.d.). Pierce develops structural record typing, a useful comparison with Fun’s nominal choice (Pierce 2002).

Chapter 13: Kinds and Type Constructors

New files

• src/kinds.rs

Changed files

• src/types.rs
• src/typecheck.rs
• src/core_lint.rs
• src/ast.rs
• src/core.rs
• src/core_type.rs
• src/data.rs
• src/elaborate.rs
• src/lexer.rs
• src/lib.rs
• src/main.rs
• src/parse.rs
• src/rename.rs

Motivation

Int describes a value. Maybe Int does too. But Maybe on its own is waiting for another type before it can describe a value. We already handle this by counting a datatype’s arguments. What happens when one of those arguments is itself something like Maybe?

Consider a field with type f a. Here f must accept a type, while a fills that argument. We need a way to describe their different jobs. These descriptions are called kinds. They look reassuringly familiar, using arrows and * instead of the richer collection of ordinary types.

Much of the machinery we need is already familiar too. We’ll infer kinds by solving equations, just as we inferred types. It’s a nice example of a compiler idea earning its keep a second time.

The Language, Now

data Wrap f a = Wrap (f a)

unwrap :: Wrap Maybe Int -> Maybe Int
unwrap (Wrap x) = x

main = unwrap (Wrap (Just 42))

Wrap has kind (* -> *) -> * -> *. A recursive declaration such as data Fix f = Fix (f (Fix f)) gives Fix kind (* -> *) -> *. Declaration dependencies are grouped into strongly connected components. Each component is inferred before its unconstrained kind variables default to *.

type Pair a = (a,a)

type Count = Int

addPair :: Pair Count -> Count
addPair (x,y) = x + y

main = addPair (20,22)

A synonym introduces no constructor or runtime representation. It must be fully applied, even where a partially applied datatype would have the right kind. Cycles are rejected, including unused cycles. E0301 reports a kind mismatch, E0302 a partial synonym, and E0303 a synonym cycle. The type constructors [], (,), (,,), and (->) may appear unapplied where their kinds permit.

Theory

Read Maybe :: * -> * much like a function type. It accepts one type of values and produces another. Applying it to Int :: * gives Maybe Int :: *. The kind application rule writes down that same step.

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

Function arguments and results must each have kind *. A constructor field must also have kind *: a value cannot inhabit the unapplied type constructor Maybe. The distinction between kinds and types follows the presentation of higher-order type operators in Pierce (Pierce 2002). Fun infers kinds but does not add type-level lambdas or explicit kind annotations.

Synonym substitution follows the Haskell report’s fully applied convention (Simon Marlow 2010). Expanding arguments before entering a synonym permits Id (Id Int) without mistaking the repeated name for a declaration cycle. A stack of definitions detects actual recursion during expansion.

Implementation

Kinds classify type constructors in the same way that types classify terms. The implementation combines kind unification, an occurs check, and dependency ordering to infer those classifications.

#![allow(unused)]
fn main() {
pub enum Kind {
    Star,
    Arrow(Box<Kind>, Box<Kind>),
    Meta(u32),
}
}

Store::unify follows solutions, compares arrow structure, and rejects a metavariable occurring inside its own proposed solution. finish defaults unsolved cells only after all fields in a declaration component were checked.

#![allow(unused)]
fn main() {
pub fn unify(
    &mut self,
    a: &Kind,
    b: &Kind,
    span: Span,
) -> Result<(), Diagnostic> {
    let (a, b) = (self.zonk(a), self.zonk(b));
    match (&a, &b) {
        _ if a == b => Ok(()),
        (Kind::Meta(n), k) | (k, Kind::Meta(n))
            if !self.occurs(*n, k) =>
        {
            self.solutions[*n as usize] = Some(k.clone());
            Ok(())
        }
        (Kind::Arrow(a, b), Kind::Arrow(c, d)) => {
            self.unify(a, c, span)?;
            self.unify(b, d, span)
        }
        _ => Err(Diagnostic::error(
            ErrorCode::Kind,
            format!("cannot unify kind {a} with {b}"),
            span,
        )),
    }
}
}

The declaration pass first installs every head, then reuses Chapter 9’s Tarjan implementation. Signatures infer implicit variable kinds against that closed table. The immutable datatype environment validates synonym use and converts the expanded syntax to inference types.

The type store now records a kind on each metavariable. Instantiating a scheme copies its quantified kinds as well as freshening its variables. Unification of f a with Maybe Int separates the final application from each side, solving f = Maybe and a = Int without requiring either to be a value type.

Core keeps a kind table keyed by unique type binder identities. Lint independently checks applications, constructor arguments, and function operands against it. Internal type variables absent from every enclosing scheme receive a closed witness of the right kind. These compiler-only type constants have no values or source syntax and disappear at erasure. This extends the Int witness used in Chapter 10 to kinds for which Int is unsuitable.

Running It

$ cd crates/ch13_kinds
$ cargo run -q -- run tests/programs/kinds/wrapper.fun --lint
Just 42
$ cargo run -q -- dump --pass=types tests/programs/kinds/wrapper.fun
main : Maybe Int
$ cargo run -q -- check tests/programs/kinds/synonym-self.fun
E0303

The last command fails and points to the bad kind application. Try a partially applied datatype constructor next, then a partially applied synonym. The former can be useful at a higher kind, while the latter is rejected by our synonym rules. Having the same apparent number of missing arguments doesn’t make the two declarations interchangeable.

Exercises

1. Warm-up. Infer the kind of data Compose f g a = Compose (f (g a)).
2. Intermediate. Explain why data Bad f = Bad (f f) fails the occurs check.
3. Intermediate. Trace kind inference through mutually dependent declarations.
4. Advanced. Find a term whose elaboration needs an internal witness of kind * -> *, and inspect the corresponding Core application.

Further Reading

• Pierce’s treatment of type operators (Pierce 2002).
• The Haskell report’s datatype and synonym rules (Simon Marlow 2010).
• Higher-order type operators and System F-omega (Pierce 2002).

Chapter 14: Type Classes

New files

• src/classes.rs
• src/evidence.rs
• src/elaborate/dictionaries.rs
• src/primitives.rs

Changed files

• src/typecheck.rs
• src/elaborate.rs
• src/types.rs
• src/ast.rs
• src/core.rs
• src/core_lint.rs
• src/core_type.rs
• src/data.rs
• src/desugar.rs
• src/eval.rs
• src/fixity.rs
• src/kinds.rs
• src/lexer.rs
• src/lib.rs
• src/main.rs
• src/parse.rs
• src/rename.rs
• src/renamed.rs
• src/syn.rs

Motivation

How do we compare two lists? We compare their elements, which means we need to know how to compare those elements. We could pass an equality function into every list comparison. That works, but we’d soon spend a lot of our time passing around the same handful of operations.

Type classes let the compiler do that plumbing. We describe the operations in a class and provide implementations in instances. The compiler works out which implementation a call needs and passes it along.

The lovely part is that we don’t need a mysterious new runtime feature. A class becomes a record of functions, usually called a dictionary. Once we’ve made those arguments explicit, our existing Core interpreter can run the result. In this chapter we’ll follow that translation all the way through.

The Language, Now

Let’s define a class and give it an instance for integers.

class Value a where
  value :: a -> Int

instance Value Int where
  value x = x + 1

main = value 41

Class parameters may have higher kinds. A method unwrap :: f a -> a gives its class parameter f kind * -> *. The remaining variable a is independently polymorphic. Classes may have superclasses and default method bodies. Instance methods accept ordinary equations, guards, and local where bindings.

The Prelude now defines Eq, Ord, Show, Num, Fractional, Semigroup, and Monoid. Arithmetic and comparisons resolve to methods. Literals remain monomorphic. 1 has type Int, while 1.0 has type Double. Consequently 1 + 2.0 fails. toDouble 1 + 2.0 succeeds. There is no defaulting.

same :: Ord a => a -> a -> Bool
same x y = x == y

main = same [1,2] [1,2]

Ord provides an Eq superclass, so the signature supplies enough evidence. An absent instance reports E0210. Malformed or overlapping instances and missing methods report E0211. A constraint whose variable is absent from the result type reports E0230: for example, show Nothing cannot choose the element’s Show instance. An explicit Maybe Int annotation resolves that ambiguity.

Double adds floating arithmetic, comparisons, conversions, and mathematical functions. Primitive names remain private to the embedded Prelude. The source still has no IO, so run prints the value of main. ++ still appends strings in this chapter. List ++ belongs to the complete Prelude chapter. <> already supports both strings and lists.

Theory

The type Eq a => a -> a -> Bool says we can compare two values of a if someone supplies equality for a. The part before => is the context. When we use a function with this type, inference creates a request for that equality operation. We call this a wanted constraint.

Some requests have immediate answers, such as the instance for Int. Others remain requests about a type variable. When we generalize a binding, those can become part of its scheme so callers supply the answer. Constraints involving an outer variable instead belong to the enclosing scope. Jones gives an executable account of these operations (Jones 1999).

Finding an instance is only half the job. We also need something to pass at runtime. That is the evidence for a constraint. An Ord a dictionary already contains its Eq a superclass dictionary. Given Eq a, the list instance can build a dictionary for Eq [a]. Following these steps constructs an ordinary expression, made from dictionary variables, field selections, and instance applications. There is no runtime search left to perform.

Signatures are checked with rigid skolems and their context as givens. Signed bindings may be used polymorphically inside their own bodies. Following the Haskell report (Simon Marlow 2010), type-inference dependencies omit edges to signed bindings. Runtime dependencies retain those edges, since recursive functions still need a shared recursive environment. These are two different uses of the same source dependency graph.

Generalization remains unrestricted. A constrained value such as comparison = (==) elaborates to a function taking a dictionary. Its body is evaluated when that dictionary is supplied, so source-level sharing is lost. Fun accepts this consequence of dictionary passing. Purity makes it sound.

Implementation

classes.rs implements superclass search, instance matching, and entailment. The main inferencer continues to use mutable, level-based metavariables. The small immutable map used to match an instance head is local to that lookup. It is not an alternative substitution-based type checker.

#![allow(unused)]
fn main() {
pub enum Evidence {
    Given(usize, Vec<usize>),
    Instance(usize, Vec<Type>, Vec<Evidence>),
}
}

A given stores its position in the lexical dictionary environment and a path through superclass fields. An instance proof stores the selected instance, its type arguments, and proofs of its prerequisites.

#![allow(unused)]
fn main() {
pub fn resolve(
    &self,
    goal: &Predicate,
    givens: &[Predicate],
    span: Span,
) -> Result<Evidence, Diagnostic> {
    for (i, given) in givens.iter().enumerate() {
        if given.ty == goal.ty
            && let Some(path) =
                self.super_path(&given.class, &goal.class)
        {
            return Ok(Evidence::Given(i, path));
        }
    }
    let (i, args, context) =
        self.by_instance(goal).ok_or_else(|| {
            error(
                ErrorCode::NoInstance,
                format!("no instance for {} {}", goal.class, goal.ty),
                span,
            )
        })?;
    let proofs = context
        .iter()
        .map(|p| self.resolve(p, givens, span))
        .collect::<Result<Vec<_>, _>>()?;
    Ok(Evidence::Instance(i, args, proofs))
}
}

Class validation checks superclass cycles, method membership, extra method constraints, distinct variables in nominal instance heads, overlap, and superclass availability. Kind inference processes superclass dependencies before defaulting unconstrained class kinds. Instance contexts may mention only the head’s variables. Solving therefore descends into structurally smaller types.

Field constraints still run before class constraints at generalization. After zonking, evidence.rs records the class proofs at variable occurrences while their lexical givens are available. Elaboration consumes these checked proofs.

#![allow(unused)]
fn main() {
pub struct EvVar {
    pub node: u32,
    pub index: usize,
}
}

elaborate/dictionaries.rs declares one nominal Core dictionary type per class. Its fields contain superclass dictionaries followed by methods. Method-local quantifiers become System F polymorphism inside the field type. This does not add rank-N signatures to the source language. Each instance becomes a global value, abstracted over its type variables and context dictionaries. Method selectors are ordinary matches on the dictionary constructor.

#![allow(unused)]
fn main() {
pub(super) fn dictionary_type(&self, class: &str, ty: Type) -> Type {
    let c = &self.constructors[self.dicts[class]];
    instantiate(&c.result, &c.parameters, &[ty])
}
}

Defaults get named globals, and each missing implementation is checked from a copy of its default body specialized to the instance. This keeps strict dictionary construction from tying a recursive value knot. Dictionary-introduced dependencies are ordered before evaluation. Recursive non-function initialization is rejected. The evaluator installs function closures before evaluating values, and each unconstrained top-level value is still evaluated once.

primitives.rs supplies fixed primitive signatures and implementations. Integer operations retain 63-bit wrapping. Floating display uses shortest round-trip digits with the specified positional range, signed exponents, and explicit special values. Tests cover negative zero, boundary magnitudes, Unicode strings, and failed conversions. The shared runtime chapter will move the non-trivial operations into fun-rt.

Running It

$ cd crates/ch14_classes
$ cargo run -q -- run tests/programs/classes/minimal.fun --lint
42
$ cargo run -q -- dump --pass=types tests/programs/classes/principal-type.fun
main : Num a => a -> a -> a
$ cargo run -q -- check tests/programs/classes/mixed-literals.fun
E0201

The failing command also prints a labelled diagnostic. --dump=core exposes $D dictionary types, $f instance globals, and explicit dictionary applications. The small dictionary snapshots disable the Prelude to keep those examples readable. Ordinary builds compile the embedded Prelude before the user’s scope. Shadowing a Prelude name cannot change the Prelude’s own references.

Expression annotations also work without enclosing parentheses. There is one place to be careful. Inside a case guard, parenthesize an annotation so its type arrow can’t be confused with the arrow leading to the alternative’s body.

Exercises

1. Warm-up. Inspect the dictionary arguments for equality on [Maybe Int].
2. Intermediate. Write an instance whose context is insufficient for its superclass, then identify the missing proof.
3. Intermediate. Explain why show Nothing is ambiguous but show (Nothing :: Maybe Int) is not.
4. Advanced. Compare the type-inference and runtime dependency components of the polymorphic-recursion fixture.
5. Advanced. Corrupt a superclass dictionary’s Core type and add a lint regression that does not invoke surface inference.

Further Reading

• Typing Haskell in Haskell (Jones 1999).
• Constructor classes and higher-kinded parameters (Jones 1993).
• Classes and instances in the language reference (Simon Marlow 2010).
• The Haskell report’s binding groups and instance restrictions (Simon Marlow 2010).

Chapter 15: Monads, Do Notation and IO

New files

• src/io_lower.rs

Changed files

• src/desugar.rs
• src/eval.rs
• src/typecheck.rs
• src/ast.rs
• src/data.rs
• src/elaborate.rs
• src/fixity.rs
• src/kinds.rs
• src/layout.rs
• src/lexer.rs
• src/lib.rs
• src/main.rs
• src/primitives.rs
• src/rename.rs
• src/session.rs

Motivation

So far, our programs have had a rather limited relationship with the outside world. The driver evaluates main, prints the answer, and goes home. Let’s write programs that can ask a question, read a response, and decide what to do next.

We want to keep ordinary expressions pure, so evaluating an IO value won’t perform its effects. We’ll represent an action as a value and run it at an explicit boundary. That distinction lets us build and combine actions using the functions we already know.

The type classes from Chapter 14 give us a way to describe these combinations. Functor, Applicative, and Monad work with IO, but they also describe useful operations on Maybe, Either, and lists. We’ll start with what the operations do and expand the syntax by hand. There’s plenty to understand here without adding mystique to the vocabulary.

The Language, Now

A complete program now has main :: IO (), whether that signature is written or inferred. The smallest example calls the new Prelude printer:

main = putStrLn "hello"

do notation also works for ordinary data. Here the two binds extract values from Just, and pure constructs the result in the same Maybe instance:

main = print (do { x <- Just 20; y <- Just 22; pure (x+y) })

A block must end with an expression. A statement x <- action binds x only in the remaining statements. A statement let introduces local declarations without an in. Patterns may be nested, including tuples, lists, as-patterns, and nominal record patterns. A failed refutable pattern calls error with its source location. Fun has no MonadFail, so failure is a runtime error even when the surrounding monad is Maybe.

putStr, putStrLn, getLine, print, and exitWith provide the program’s external interface. mapM, mapM_, sequence_, when, and unless express common sequencing patterns. A missing or wrongly typed entry point reports E0250. A body that violates its explicit signature can instead fail during signature checking with E0203.

Theory

Suppose an action produces an a, and the rest of our program knows how to use that a to make the next action. Bind connects the two. Its second argument is a function because the next action may depend on the first result. Read this type slowly from left to right (Jones 1993).

$$\mathsf{Monad}m\Rightarrow m\alpha \to (\alpha \to m\beta )\to m\beta$$

For IO, the source checker treats IO as an abstract nominal constructor. Core represents an action as a function from unit to its result:

$$\mathsf{IO}\alpha \Rightarrow ()\to \alpha$$

The unit argument gives us somewhere to put the delay. Constructing the function doesn’t run its body. returnIO builds a function that returns its saved value, while bindIO builds one that runs the first action and passes the result to the next. The effectful primitives sit inside those bodies.

Only the trusted Prelude and compiler can use this representation. Source programs see abstract IO a values, so they can’t apply an action to () and run it wherever they please. That boundary is what lets ordinary Fun expressions remain pure.

Strictness still applies. Constructing putStrLn "hello" evaluates its string argument and returns an action. It does not print. Constructing an action with error "bad" as an eagerly demanded argument can fail before the action runs. Sequencing controls effects, not evaluation of arbitrary pure arguments. The Haskell report describes the analogous do translations (Simon Marlow 2010), but its lazy evaluation must not be imported into Fun’s operational account.

The monad laws describe intended instance behavior. The compiler checks types, not those equations. In particular, equations involving nontermination need care in a strict language. Dictionary passing remains the mechanism from Chapter 14: no new class dispatch appears in the evaluator.

Implementation

The parser calls desugar::do_block before lexical renaming. Processing the statements backwards makes the remaining block the continuation of each bind. A variable pattern becomes a lambda directly. A refutable pattern introduces a case with a failure alternative. Its temporary name cannot be written as a source identifier.

#![allow(unused)]
fn main() {
use crate::{
    data::{ConId, DataEnv},
    diagnostics::{Diagnostic, ErrorCode},
    renamed::{self, BindGroup, Expr, Kind, Pat, PatKind, Row, RowBody},
    session::{Session, Stop},
    source::Span,
    syn,
};
struct Desugar<'a> {
    sess: &'a mut Session,
    data: &'a DataEnv,
}
impl Desugar<'_> {
    fn node(&mut self, kind: Kind, span: Span) -> Expr {
        Expr {
            kind,
            span,
            node: self.sess.fresh_node(),
        }
    }
    fn constructor(&mut self, name: &str, span: Span) -> ConId {
        if let Some(info) = self.data.constructor(name) {
            return info.id.clone();
        }
        self.sess.emit(Diagnostic::error(
            ErrorCode::UnboundConstructor,
            format!("sugar requires constructor {name} from the Prelude"),
            span,
        ));
        ConId {
            index: 0,
            name: name.into(),
        }
    }
    fn tuple(&mut self, n: usize, span: Span) -> ConId {
        if !matches!(n, 0 | 2 | 3) {
            self.sess.emit(Diagnostic::error(
                ErrorCode::Parse,
                "only unit, pairs, and triples are supported",
                span,
            ));
        }
        self.constructor(
            &format!("({})", ",".repeat(n.saturating_sub(1))),
            span,
        )
    }
    fn pattern(&mut self, p: Pat) -> Pat {
        let span = p.span;
        let kind = match p.kind {
            PatKind::List(ps) => {
                let nil = self.constructor("[]", span);
                let cons = self.constructor(":", span);
                let mut tail = Pat {
                    kind: PatKind::Con(nil, vec![]),
                    span,
                };
                for p in ps.into_iter().rev() {
                    tail = Pat {
                        kind: PatKind::Con(
                            cons.clone(),
                            vec![self.pattern(p), tail],
                        ),
                        span,
                    };
                }
                return tail;
            }
            PatKind::Tuple(ps) => PatKind::Con(
                self.tuple(ps.len(), span),
                ps.into_iter().map(|p| self.pattern(p)).collect(),
            ),
            PatKind::Con(id, ps) => PatKind::Con(
                id,
                ps.into_iter().map(|p| self.pattern(p)).collect(),
            ),
            PatKind::As(id, p) => {
                PatKind::As(id, Box::new(self.pattern(*p)))
            }
            PatKind::Int(n) => PatKind::Int((n << 1) >> 1),
            other => other,
        };
        Pat { kind, span }
    }
    fn groups(&mut self, groups: Vec<BindGroup>) -> Vec<BindGroup> {
        groups
            .into_iter()
            .map(|mut g| {
                for b in &mut g.binds {
                    b.rhs = self.expression(b.rhs.clone());
                }
                g
            })
            .collect()
    }
    fn row(&mut self, row: Row) -> Row {
        let body = match row.body {
            RowBody::Plain(e) => {
                RowBody::Plain(Box::new(self.expression(*e)))
            }
            RowBody::Guarded(gs) => RowBody::Guarded(
                gs.into_iter()
                    .map(|(g, e)| (self.expression(g), self.expression(e)))
                    .collect(),
            ),
        };
        Row {
            patterns: row
                .patterns
                .into_iter()
                .map(|p| self.pattern(p))
                .collect(),
            body,
            locals: self.groups(row.locals),
            span: row.span,
        }
    }
    fn equations(&mut self, rows: Vec<Row>, span: Span) -> Expr {
        let mut rows: Vec<_> =
            rows.into_iter().map(|r| self.row(r)).collect();
        if rows.len() == 1
            && rows[0]
                .patterns
                .iter()
                .all(|p| matches!(p.kind, PatKind::Var(_)))
            && matches!(rows[0].body, RowBody::Plain(_))
        {
            let row = rows.pop().unwrap();
            let RowBody::Plain(body) = row.body else {
                unreachable!()
            };
            let mut body = *body;
            if !row.locals.is_empty() {
                body =
                    self.node(Kind::Let(row.locals, Box::new(body)), span);
            }
            for p in row.patterns.into_iter().rev() {
                let PatKind::Var(id) = p.kind else {
                    unreachable!()
                };
                body = self.node(Kind::Lam(id, Box::new(body)), span);
            }
            return body;
        }
        // ANCHOR: equations-match
        let params: Vec<_> = (0..rows[0].patterns.len())
            .map(|_| self.sess.fresh_id("$match"))
            .collect();
        let scruts = params
            .iter()
            .map(|id| self.node(Kind::Var(id.clone()), span))
            .collect();
        let mut body = self.node(Kind::Match(scruts, rows), span);
        for id in params.into_iter().rev() {
            body = self.node(Kind::Lam(id, Box::new(body)), span);
        }
        body
        // ANCHOR_END: equations-match
    }
    fn expression(&mut self, expr: Expr) -> Expr {
        let mut work = vec![(Some(expr), None)];
        let mut values: Vec<Expr> = Vec::new();
        while let Some((expr, saved)) = work.pop() {
            match expr {
                Some(Expr {
                    kind: Kind::App(f, a),
                    node,
                    span,
                }) => {
                    work.push((None, Some((node, span))));
                    work.push((Some(*a), None));
                    work.push((Some(*f), None));
                }
                Some(expr) => values.push(self.expression_leaf(expr)),
                None => {
                    let a = values.pop().expect("application argument");
                    let f = values.pop().expect("application function");
                    let (node, span) = saved.expect("application metadata");
                    values.push(Expr {
                        node,
                        span,
                        kind: Kind::App(Box::new(f), Box::new(a)),
                    });
                }
            }
        }
        values.pop().expect("desugared root")
    }
    fn expression_leaf(&mut self, expr: Expr) -> Expr {
        let span = expr.span;
        let kind = match expr.kind {
            Kind::Record(id, fields) => Kind::Record(
                id,
                fields
                    .into_iter()
                    .map(|(n, e)| (n, self.expression(e)))
                    .collect(),
            ),
            Kind::Project(e, n) => {
                Kind::Project(Box::new(self.expression(*e)), n)
            }
            Kind::Update(e, fields) => Kind::Update(
                Box::new(self.expression(*e)),
                fields
                    .into_iter()
                    .map(|(n, e)| (n, self.expression(e)))
                    .collect(),
            ),
            Kind::Annotated(e, t) => {
                Kind::Annotated(Box::new(self.expression(*e)), t)
            }
            Kind::Bool(b) => Kind::Con(
                self.constructor(if b { "True" } else { "False" }, span),
            ),
            Kind::Equations(rows) => return self.equations(rows, span),
            Kind::PatternLam(patterns, body) => {
                return self.equations(
                    vec![Row {
                        patterns,
                        body: RowBody::Plain(body),
                        locals: vec![],
                        span,
                    }],
                    span,
                );
            }
            Kind::Case(e, rows) => Kind::Match(
                vec![self.expression(*e)],
                rows.into_iter().map(|r| self.row(r)).collect(),
            ),
            Kind::If(c, a, b) => {
                let c = self.expression(*c);
                let a = self.expression(*a);
                let b = self.expression(*b);
                let rows = [("True", a), ("False", b)]
                    .into_iter()
                    .map(|(name, body)| Row {
                        patterns: vec![Pat {
                            kind: PatKind::Con(
                                self.constructor(name, span),
                                vec![],
                            ),
                            span,
                        }],
                        body: RowBody::Plain(Box::new(body)),
                        locals: vec![],
                        span,
                    })
                    .collect();
                Kind::Match(vec![c], rows)
            }
            Kind::List(es) => {
                let nil = self.constructor("[]", span);
                let cons = self.constructor(":", span);
                let mut tail = self.node(Kind::Con(nil), span);
                for e in es.into_iter().rev() {
                    let con = self.node(Kind::Con(cons.clone()), span);
                    let head = self.expression(e);
                    let app = self.node(
                        Kind::App(Box::new(con), Box::new(head)),
                        span,
                    );
                    tail = self.node(
                        Kind::App(Box::new(app), Box::new(tail)),
                        span,
                    );
                }
                return tail;
            }
            Kind::Tuple(es) => {
                let id = self.tuple(es.len(), span);
                let mut value = self.node(Kind::Con(id), span);
                for e in es {
                    let e = self.expression(e);
                    value = self.node(
                        Kind::App(Box::new(value), Box::new(e)),
                        span,
                    );
                }
                return value;
            }
            Kind::Lam(id, b) => {
                Kind::Lam(id, Box::new(self.expression(*b)))
            }
            Kind::App(a, b) => Kind::App(
                Box::new(self.expression(*a)),
                Box::new(self.expression(*b)),
            ),
            Kind::Let(gs, b) => {
                Kind::Let(self.groups(gs), Box::new(self.expression(*b)))
            }
            Kind::Neg(a) => Kind::Neg(Box::new(self.expression(*a))),
            Kind::Binary(op, a, b) => Kind::Binary(
                op,
                Box::new(self.expression(*a)),
                Box::new(self.expression(*b)),
            ),
            Kind::Match(..) => {
                unreachable!("Match is produced by this pass")
            }
            other => other,
        };
        Expr {
            kind,
            span,
            node: expr.node,
        }
    }
}
/// Produce Syn after names are resolved, preserving row scopes and guard order.
pub fn desugar(
    sess: &mut Session,
    program: renamed::Program,
) -> Result<syn::Program, Stop> {
    let groups = {
        let mut pass = Desugar {
            sess,
            data: &program.data,
        };
        pass.groups(program.groups)
    };
    sess.finish(syn::Program {
        classes: program.classes,
        data: program.data,
        groups,
        primitives: program.primitives,
        main: program.main,
        span: program.span,
    })
}
/// Statements are lowered before name resolution so ordinary lexical scopes apply.
pub enum Statement {
    Expr(crate::ast::Expr),
    Bind(crate::ast::Pat, crate::ast::Expr),
    Let(Vec<crate::ast::Binding>),
}
pub fn do_pattern(
    e: crate::ast::Expr,
) -> Result<crate::ast::Pat, Diagnostic> {
    use crate::ast::{Kind as K, Pat as P, PatKind as PK};
    let span = e.span;
    let kind = match e.kind {
        K::Chain(a, pairs, None) if pairs.is_empty() => {
            return do_pattern(*a);
        }
        K::Chain(a, pairs, None)
            if pairs.iter().all(|(op, _)| op == ":") =>
        {
            let mut elements = vec![do_pattern(*a)?];
            for (_, e) in pairs {
                elements.push(do_pattern(e)?);
            }
            let mut tail = elements.pop().unwrap();
            for head in elements.into_iter().rev() {
                tail = P {
                    kind: PK::Con(":".into(), vec![head, tail]),
                    span,
                };
            }
            return Ok(tail);
        }
        K::PatternAs(n, p) => PK::As(n, Box::new(do_pattern(*p)?)),
        K::Paren(a) => return do_pattern(*a),
        K::Var(n) if n == "_" => PK::Wild,
        K::Var(n) if n.starts_with(char::is_uppercase) => {
            PK::Con(n, vec![])
        }
        K::Var(n) => PK::Var(n),
        K::App(a, b) => {
            let mut p = do_pattern(*a)?;
            if let PK::Con(_, ps) = &mut p.kind {
                ps.push(do_pattern(*b)?);
                return Ok(p);
            } else {
                return Err(Diagnostic::error(
                    ErrorCode::Parse,
                    "invalid do pattern",
                    span,
                ));
            }
        }
        K::Int(n) => PK::Int(n),
        K::Double(n) => PK::Double(n),
        K::Char(c) => PK::Char(c),
        K::String(s) => PK::String(s),
        K::Neg(a) => {
            if let K::Int(n) = a.kind {
                PK::Int(-n)
            } else {
                return Err(Diagnostic::error(
                    ErrorCode::Parse,
                    "invalid negative pattern",
                    span,
                ));
            }
        }
        K::List(es) => PK::List(
            es.into_iter().map(do_pattern).collect::<Result<_, _>>()?,
        ),
        K::Tuple(es) => PK::Tuple(
            es.into_iter().map(do_pattern).collect::<Result<_, _>>()?,
        ),
        K::Update(a, fs) => {
            fn record(
                mut p: P,
                fields: Vec<(String, P)>,
            ) -> Result<P, Diagnostic> {
                p.kind = match p.kind {
                    PK::As(n, p) => {
                        PK::As(n, Box::new(record(*p, fields)?))
                    }
                    PK::Con(n, ps) if ps.is_empty() => {
                        PK::Record(n, fields)
                    }
                    _ => {
                        return Err(Diagnostic::error(
                            ErrorCode::Parse,
                            "invalid record pattern",
                            p.span,
                        ));
                    }
                };
                Ok(p)
            }
            let fields = fs
                .into_iter()
                .map(|(n, e)| Ok((n, do_pattern(e)?)))
                .collect::<Result<_, Diagnostic>>()?;
            return record(do_pattern(*a)?, fields);
        }
        K::Record(n, fs) => PK::Record(
            n,
            fs.into_iter()
                .map(|(n, e)| Ok((n, do_pattern(e)?)))
                .collect::<Result<_, Diagnostic>>()?,
        ),
        _ => {
            return Err(Diagnostic::error(
                ErrorCode::Parse,
                "invalid do pattern",
                span,
            ));
        }
    };
    Ok(P { kind, span })
}
/// Expand do syntax into ordinary applications, matches, and local bindings.
pub fn do_block(
    statements: Vec<Statement>,
    span: Span,
) -> Result<crate::ast::Expr, Diagnostic> {
    use crate::ast::{
        Expr as E, Kind as K, Pat as P, PatKind as PK, Row as R,
        RowBody as B,
    };
    let node = |kind| E { kind, span };
    let app = |a, b| node(K::App(Box::new(a), Box::new(b)));
    let mut statements = statements;
    let Some(Statement::Expr(mut body)) = statements.pop() else {
        return Err(Diagnostic::error(
            ErrorCode::Parse,
            "do must end with an expression",
            span,
        ));
    };
    for statement in statements.into_iter().rev() {
        body = match statement {
            Statement::Expr(e) => {
                app(app(node(K::Var(">>".into())), e), body)
            }
            Statement::Let(bs) => node(K::LetGroup(bs, Box::new(body))),
            Statement::Bind(p, e) => {
                let continuation = match &p.kind {
                    PK::Var(n) => node(K::Lam(n.clone(), Box::new(body))),
                    PK::Wild => node(K::Lam("$do".into(), Box::new(body))),
                    _ => {
                        let site = p.span;
                        let rows = vec![
                            R {
                                patterns: vec![p],
                                body: B::Plain(Box::new(body)),
                                locals: vec![],
                                span: site,
                            },
                            R {
                                patterns: vec![P {
                                    kind: PK::Wild,
                                    span: site,
                                }],
                                body: B::Plain(Box::new(E {
                                    kind: K::DoFail,
                                    span: site,
                                })),
                                locals: vec![],
                                span: site,
                            },
                        ];
                        node(K::Lam(
                            "$do".into(),
                            Box::new(node(K::Case(
                                Box::new(node(K::Var("$do".into()))),
                                rows,
                            ))),
                        ))
                    }
                };
                app(app(node(K::Var(">>=".into())), e), continuation)
            }
        };
    }
    Ok(body)
}
}

This placement differs from a separate post-renaming desugaring pass: generated bindings go through the same scope checker as handwritten ones. The helper do_pattern validates the pattern-shaped syntax on the left of <-. The span-bearing DoFail node is later translated into an ordinary error call with its file, line, and column. No do node reaches Core.

Only the Prelude’s trusted FileId lets the checker relate its IO implementation to unit-taking functions. User-visible schemes remain nominal. After elaboration, io_lower::lower traverses all Core types before lint: binder types, type applications, constructor fields, match result types, and dictionary types. Replacing only IO a at the outermost level would miss higher-kinded uses such as a Monad IO dictionary. The traversal also replaces the unapplied constructor IO with the partially applied function constructor (->) ().

The runner first installs function closures and evaluates strict top-level values in dependency order, then applies the entry point to unit:

#![allow(unused)]
fn main() {
use crate::{
    ast::Op,
    core::{self, Bind, BindGroup, Expr, Id, Lit},
};
use std::{cell::RefCell, rc::Rc};
/// Language termination is separate from an ordinary runtime failure.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Failure {
    Runtime(String),
    Exit(i32),
}
impl From<String> for Failure {
    fn from(s: String) -> Self {
        Self::Runtime(s)
    }
}
impl From<&str> for Failure {
    fn from(s: &str) -> Self {
        Self::Runtime(s.into())
    }
}
impl std::fmt::Display for Failure {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Runtime(s) => write!(f, "{s}"),
            Self::Exit(n) => write!(f, "exit {n}"),
        }
    }
}
type Env = Vec<(Id, Value)>;
#[derive(Clone, Debug)]
/// A closure captures outer declarations and an optional immutable recursive-group recipe.
pub enum Value {
    Lit(Lit),
    Con(crate::data::ConId, Vec<Value>, Option<Vec<String>>),
    Closure {
        parameter: Id,
        body: Rc<Expr>,
        env: Rc<Env>,
        recursive: Option<Rc<Vec<Bind>>>,
    },
}
impl std::fmt::Display for Value {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        self.print(f, 0)
    }
}
impl Value {
    fn print(
        &self,
        f: &mut std::fmt::Formatter<'_>,
        precedence: u8,
    ) -> std::fmt::Result {
        match self {
            Self::Lit(Lit::Double(n))
                if f64::from_bits(*n).is_sign_negative()
                    && precedence > 6 =>
            {
                write!(
                    f,
                    "({})",
                    crate::primitives::show_double(f64::from_bits(*n))
                )
            }
            Self::Lit(Lit::Int(n)) if *n < 0 && precedence > 6 => {
                write!(f, "({n})")
            }
            Self::Lit(l) => write!(f, "{l}"),
            Self::Closure { .. } => write!(f, "<function>"),
            Self::Con(id, fields, Some(labels)) => {
                if precedence > 10 {
                    write!(f, "(")?;
                }
                write!(f, "{} {{", id.name)?;
                for (i, (name, value)) in
                    labels.iter().zip(fields).enumerate()
                {
                    if i > 0 {
                        write!(f, ", ")?;
                    }
                    write!(f, "{name} = ")?;
                    value.print(f, 0)?;
                }
                write!(f, "}}")?;
                if precedence > 10 {
                    write!(f, ")")?;
                }
                Ok(())
            }
            Self::Con(id, fields, None) => match id.name.as_str() {
                "[]" => write!(f, "[]"),
                ":" => {
                    write!(f, "[")?;
                    let mut value = self;
                    let mut first = true;
                    while let Self::Con(c, fs, _) = value {
                        if c.name == "[]" {
                            break;
                        }
                        if !first {
                            write!(f, ",")?;
                        }
                        first = false;
                        fs[0].print(f, 0)?;
                        value = &fs[1];
                    }
                    write!(f, "]")
                }
                "()" | "(,)" | "(,,)" => {
                    write!(f, "(")?;
                    for (i, v) in fields.iter().enumerate() {
                        if i > 0 {
                            write!(f, ",")?;
                        }
                        v.print(f, 0)?;
                    }
                    write!(f, ")")
                }
                _ => {
                    let parens = precedence > 10 && !fields.is_empty();
                    if parens {
                        write!(f, "(")?;
                    }
                    write!(f, "{}", id.name)?;
                    for v in fields {
                        write!(f, " ")?;
                        v.print(f, 11)?;
                    }
                    if parens {
                        write!(f, ")")?;
                    }
                    Ok(())
                }
            },
        }
    }
}
pub fn normalize(n: i64) -> i64 {
    (n << 1) >> 1
}
/// Rebuild a recursive group's closures from a shared immutable recipe. The
/// recipe captures the outer environment, never the closures themselves.
// ANCHOR: recursive-closures
fn recursive_values(bindings: Rc<Vec<Bind>>, env: Rc<Env>) -> Env {
    let mut values = Vec::new();
    for binding in bindings.iter() {
        let mut rhs = &*binding.rhs;
        while let Expr::TyLam(_, inner) = rhs {
            rhs = inner;
        }
        let Expr::Lam(parameter, body) = rhs else {
            unreachable!("recursive lambda invariant")
        };
        let value = Value::Closure {
            parameter: parameter.clone(),
            body: Rc::new(*body.clone()),
            env: env.clone(),
            recursive: Some(bindings.clone()),
        };
        values.push((binding.name.clone(), value));
    }
    values
}
fn bind_group(
    group: &BindGroup,
    env: &mut Env,
    fuel: &mut usize,
    program: &core::Program,
    globals: &RefCell<Env>,
) -> Result<(), Failure> {
    if group.recursive {
        env.extend(recursive_values(
            Rc::new(group.binds.clone()),
            Rc::new(env.clone()),
        ));
    } else {
        for binding in &group.binds {
            let value =
                evaluate(&binding.rhs, env, fuel, program, globals)?;
            env.push((binding.name.clone(), value));
        }
    }
    Ok(())
}
fn evaluate(
    expr: &Expr,
    env: &Env,
    fuel: &mut usize,
    program: &core::Program,
    globals: &RefCell<Env>,
) -> Result<Value, Failure> {
    *fuel = fuel.checked_sub(1).ok_or("step limit exceeded")?;
    match expr {
        Expr::Lit(l) => Ok(Value::Lit(l.clone())),
        Expr::TyLam(_, body) | Expr::TyApp(body, _) => {
            evaluate(body, env, fuel, program, globals)
        }
        Expr::Global(n) => globals
            .borrow()
            .iter()
            .find(|(id, _)| id.unique() == n.unique())
            .map(|(_, v)| v.clone())
            .ok_or_else(|| {
                Failure::Runtime(format!(
                    "internal error: uninitialized global {n}"
                ))
            }),
        Expr::Var(n) => env
            .iter()
            .rev()
            .find(|(name, _)| name == n)
            .map(|(_, v)| v.clone())
            .ok_or_else(|| {
                Failure::Runtime(format!("internal error: unbound {n}"))
            }),
        Expr::Lam(parameter, body) => Ok(Value::Closure {
            parameter: parameter.clone(),
            body: Rc::new(*body.clone()),
            env: Rc::new(env.clone()),
            recursive: None,
        }),
        // ANCHOR: application
        Expr::App(function, argument) => {
            let function = evaluate(function, env, fuel, program, globals)?;
            let argument = evaluate(argument, env, fuel, program, globals)?;
            if let Value::Closure {
                parameter,
                body,
                env,
                recursive,
            } = &function
            {
                let mut local = (**env).clone();
                if let Some(bindings) = recursive {
                    local.extend(recursive_values(
                        bindings.clone(),
                        env.clone(),
                    ));
                }
                local.push((parameter.clone(), argument));
                evaluate(body, &local, fuel, program, globals)
            } else {
                Err("internal error: non-function application".into())
            }
        }
        // ANCHOR_END: application
        Expr::Let(group, body) => {
            let mut local = env.clone();
            bind_group(group, &mut local, fuel, program, globals)?;
            evaluate(body, &local, fuel, program, globals)
        }
        Expr::Con(id, _, fields) => Ok(Value::Con(
            id.clone(),
            fields
                .iter()
                .map(|e| evaluate(e, env, fuel, program, globals))
                .collect::<Result<_, _>>()?,
            program.constructors[id.index as usize].labels.clone(),
        )),
        Expr::PatternFail(span, _) => Err(failure(program, *span).into()),
        Expr::Match(m) => {
            let values = m
                .scruts
                .iter()
                .map(|id| {
                    evaluate(
                        &Expr::Var(id.clone()),
                        env,
                        fuel,
                        program,
                        globals,
                    )
                })
                .collect::<Result<Vec<_>, _>>()?;
            for row in &m.rows {
                let mut local = env.clone();
                if !row
                    .pats
                    .iter()
                    .zip(&values)
                    .all(|(p, v)| matches_pattern(p, v, &mut local))
                {
                    continue;
                }
                for group in &row.locals {
                    bind_group(group, &mut local, fuel, program, globals)?;
                }
                match &row.body {
                    core::RowBody::Plain(e) => {
                        return evaluate(e, &local, fuel, program, globals);
                    }
                    core::RowBody::Guarded(gs) => {
                        for (g, e) in gs {
                            let value = evaluate(
                                g, &local, fuel, program, globals,
                            )?;
                            if matches!(value,Value::Con(id,_,_) if id.name=="True")
                            {
                                return evaluate(
                                    e, &local, fuel, program, globals,
                                );
                            }
                        }
                    }
                }
            }
            Err(failure(program, m.span).into())
        }
        Expr::Prim(op, _, args, _) => {
            let values = args
                .iter()
                .map(|a| evaluate(a, env, fuel, program, globals))
                .collect::<Result<Vec<_>, _>>()?;
            primitive(*op, &values, program, globals)
        }
    }
}
fn primitive(
    op: Op,
    args: &[Value],
    program: &core::Program,
    _globals: &RefCell<Env>,
) -> Result<Value, Failure> {
    if let Op::Runtime(p) = op {
        return crate::primitives::evaluate(p, args, program);
    }
    if let [Value::Lit(Lit::String(a)), Value::Lit(Lit::String(b))] = args
        && op == Op::Append
    {
        return Ok(Value::Lit(Lit::String(format!("{a}{b}"))));
    }
    let [Value::Lit(Lit::Int(a)), Value::Lit(Lit::Int(b))] = args else {
        return Err("internal error: primitive operands".into());
    };
    if matches!(op, Op::Eq | Op::Lt | Op::Le) {
        let yes = match op {
            Op::Eq => a == b,
            Op::Lt => a < b,
            _ => a <= b,
        };
        let name = if yes { "True" } else { "False" };
        let c = program
            .constructors
            .iter()
            .find(|c| c.id.name == name)
            .ok_or("internal error: missing Bool constructor")?;
        return Ok(Value::Con(c.id.clone(), vec![], c.labels.clone()));
    }
    let value = match op {
        Op::Runtime(p) => {
            return crate::primitives::evaluate(p, args, program);
        }
        Op::Add => Lit::Int(normalize(a.wrapping_add(*b))),
        Op::Sub => Lit::Int(normalize(a.wrapping_sub(*b))),
        Op::Mul => Lit::Int(normalize(a.wrapping_mul(*b))),
        Op::Eq | Op::Lt | Op::Le => unreachable!(),
        Op::Div | Op::Mod => {
            if *b == 0 {
                return Err("divide by zero".into());
            }
            let (mut q, mut r) = (a / b, a % b);
            if r != 0 && (r < 0) != (*b < 0) {
                q -= 1;
                r += b;
            }
            Lit::Int(normalize(if op == Op::Div { q } else { r }))
        }
        Op::Append => {
            return Err("internal error: string append on Int".into());
        }
    };
    Ok(Value::Lit(value))
}
/// Evaluate top-level values exactly once in dependency order, then select main's value.
fn execute(
    program: &core::Program,
    mut fuel: usize,
    io: bool,
) -> Result<String, Failure> {
    let globals = RefCell::new(vec![]);
    for group in &program.groups {
        for b in &group.binds {
            if core::is_function(&b.rhs) {
                let value = evaluate(
                    &b.rhs,
                    &vec![],
                    &mut fuel,
                    program,
                    &globals,
                )?;
                globals.borrow_mut().push((b.name.clone(), value));
            }
        }
    }
    for group in &program.groups {
        for b in &group.binds {
            if !core::is_function(&b.rhs) {
                let value = evaluate(
                    &b.rhs,
                    &vec![],
                    &mut fuel,
                    program,
                    &globals,
                )?;
                globals.borrow_mut().push((b.name.clone(), value));
            }
        }
    }
    let value = globals
        .borrow()
        .iter()
        .find(|(n, _)| n.unique() == program.main.unique())
        .map(|(_, v)| v.clone())
        .ok_or("internal error: missing main")?;
    if io {
        let unit = program
            .constructors
            .iter()
            .find(|c| c.id.name == "()")
            .unwrap();
        let action = Expr::App(
            Box::new(Expr::Global(program.main.clone())),
            Box::new(Expr::Con(unit.id.clone(), vec![], vec![])),
        );
        evaluate(&action, &vec![], &mut fuel, program, &globals)?;
        Ok(String::new())
    } else {
        Ok(value.to_string())
    }
}
/// Evaluate a pure fragment; retained for compiler tests and REPL inspection.
pub fn run(program: &core::Program, fuel: usize) -> Result<String, String> {
    execute(program, fuel, false).map_err(|e| e.to_string())
}
fn failure(program: &core::Program, span: crate::source::Span) -> String {
    let site = program
        .locations
        .iter()
        .find(|(s, _)| *s == span)
        .map(|(_, s)| s.as_str())
        .unwrap_or("<unknown>:1:1");
    format!("pattern match failure at {site}")
}
fn matches_pattern(p: &core::Pat, v: &Value, env: &mut Env) -> bool {
    match p {
        core::Pat::Wild => true,
        core::Pat::Var(id) => {
            env.push((id.clone(), v.clone()));
            true
        }
        core::Pat::As(id, p) => {
            env.push((id.clone(), v.clone()));
            matches_pattern(p, v, env)
        }
        core::Pat::Lit(Lit::Double(n)) => {
            matches!(v,Value::Lit(Lit::Double(m)) if f64::from_bits(*n)==f64::from_bits(*m))
        }
        core::Pat::Lit(l) => matches!(v,Value::Lit(actual) if l==actual),
        core::Pat::Con(id, ps) => match v {
            Value::Con(actual, vs, _)
                if id == actual && ps.len() == vs.len() =>
            {
                ps.iter().zip(vs).all(|(p, v)| matches_pattern(p, v, env))
            }
            _ => false,
        },
    }
}
/// Initialize globals, then run the checked IO action exactly once.
pub fn run_io(program: &core::Program, fuel: usize) -> Result<(), Failure> {
    execute(program, fuel, true).map(|_| ())
}
}

An unused top-level action is still a value initialized at startup. Its body is not entered, as this regression demonstrates:

unused = putStrLn "bad"

main = putStrLn "ok"

The evaluator distinguishes a language error from a requested process exit. This distinction prevents exitWith 7 from being printed as an error message:

#![allow(unused)]
fn main() {
use crate::{
    ast::Op,
    core::{self, Bind, BindGroup, Expr, Id, Lit},
};
use std::{cell::RefCell, rc::Rc};
impl From<String> for Failure {
    fn from(s: String) -> Self {
        Self::Runtime(s)
    }
}
impl From<&str> for Failure {
    fn from(s: &str) -> Self {
        Self::Runtime(s.into())
    }
}
impl std::fmt::Display for Failure {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Runtime(s) => write!(f, "{s}"),
            Self::Exit(n) => write!(f, "exit {n}"),
        }
    }
}
type Env = Vec<(Id, Value)>;
#[derive(Clone, Debug)]
/// A closure captures outer declarations and an optional immutable recursive-group recipe.
pub enum Value {
    Lit(Lit),
    Con(crate::data::ConId, Vec<Value>, Option<Vec<String>>),
    Closure {
        parameter: Id,
        body: Rc<Expr>,
        env: Rc<Env>,
        recursive: Option<Rc<Vec<Bind>>>,
    },
}
impl std::fmt::Display for Value {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        self.print(f, 0)
    }
}
impl Value {
    fn print(
        &self,
        f: &mut std::fmt::Formatter<'_>,
        precedence: u8,
    ) -> std::fmt::Result {
        match self {
            Self::Lit(Lit::Double(n))
                if f64::from_bits(*n).is_sign_negative()
                    && precedence > 6 =>
            {
                write!(
                    f,
                    "({})",
                    crate::primitives::show_double(f64::from_bits(*n))
                )
            }
            Self::Lit(Lit::Int(n)) if *n < 0 && precedence > 6 => {
                write!(f, "({n})")
            }
            Self::Lit(l) => write!(f, "{l}"),
            Self::Closure { .. } => write!(f, "<function>"),
            Self::Con(id, fields, Some(labels)) => {
                if precedence > 10 {
                    write!(f, "(")?;
                }
                write!(f, "{} {{", id.name)?;
                for (i, (name, value)) in
                    labels.iter().zip(fields).enumerate()
                {
                    if i > 0 {
                        write!(f, ", ")?;
                    }
                    write!(f, "{name} = ")?;
                    value.print(f, 0)?;
                }
                write!(f, "}}")?;
                if precedence > 10 {
                    write!(f, ")")?;
                }
                Ok(())
            }
            Self::Con(id, fields, None) => match id.name.as_str() {
                "[]" => write!(f, "[]"),
                ":" => {
                    write!(f, "[")?;
                    let mut value = self;
                    let mut first = true;
                    while let Self::Con(c, fs, _) = value {
                        if c.name == "[]" {
                            break;
                        }
                        if !first {
                            write!(f, ",")?;
                        }
                        first = false;
                        fs[0].print(f, 0)?;
                        value = &fs[1];
                    }
                    write!(f, "]")
                }
                "()" | "(,)" | "(,,)" => {
                    write!(f, "(")?;
                    for (i, v) in fields.iter().enumerate() {
                        if i > 0 {
                            write!(f, ",")?;
                        }
                        v.print(f, 0)?;
                    }
                    write!(f, ")")
                }
                _ => {
                    let parens = precedence > 10 && !fields.is_empty();
                    if parens {
                        write!(f, "(")?;
                    }
                    write!(f, "{}", id.name)?;
                    for v in fields {
                        write!(f, " ")?;
                        v.print(f, 11)?;
                    }
                    if parens {
                        write!(f, ")")?;
                    }
                    Ok(())
                }
            },
        }
    }
}
pub fn normalize(n: i64) -> i64 {
    (n << 1) >> 1
}
/// Rebuild a recursive group's closures from a shared immutable recipe. The
/// recipe captures the outer environment, never the closures themselves.
// ANCHOR: recursive-closures
fn recursive_values(bindings: Rc<Vec<Bind>>, env: Rc<Env>) -> Env {
    let mut values = Vec::new();
    for binding in bindings.iter() {
        let mut rhs = &*binding.rhs;
        while let Expr::TyLam(_, inner) = rhs {
            rhs = inner;
        }
        let Expr::Lam(parameter, body) = rhs else {
            unreachable!("recursive lambda invariant")
        };
        let value = Value::Closure {
            parameter: parameter.clone(),
            body: Rc::new(*body.clone()),
            env: env.clone(),
            recursive: Some(bindings.clone()),
        };
        values.push((binding.name.clone(), value));
    }
    values
}
fn bind_group(
    group: &BindGroup,
    env: &mut Env,
    fuel: &mut usize,
    program: &core::Program,
    globals: &RefCell<Env>,
) -> Result<(), Failure> {
    if group.recursive {
        env.extend(recursive_values(
            Rc::new(group.binds.clone()),
            Rc::new(env.clone()),
        ));
    } else {
        for binding in &group.binds {
            let value =
                evaluate(&binding.rhs, env, fuel, program, globals)?;
            env.push((binding.name.clone(), value));
        }
    }
    Ok(())
}
fn evaluate(
    expr: &Expr,
    env: &Env,
    fuel: &mut usize,
    program: &core::Program,
    globals: &RefCell<Env>,
) -> Result<Value, Failure> {
    *fuel = fuel.checked_sub(1).ok_or("step limit exceeded")?;
    match expr {
        Expr::Lit(l) => Ok(Value::Lit(l.clone())),
        Expr::TyLam(_, body) | Expr::TyApp(body, _) => {
            evaluate(body, env, fuel, program, globals)
        }
        Expr::Global(n) => globals
            .borrow()
            .iter()
            .find(|(id, _)| id.unique() == n.unique())
            .map(|(_, v)| v.clone())
            .ok_or_else(|| {
                Failure::Runtime(format!(
                    "internal error: uninitialized global {n}"
                ))
            }),
        Expr::Var(n) => env
            .iter()
            .rev()
            .find(|(name, _)| name == n)
            .map(|(_, v)| v.clone())
            .ok_or_else(|| {
                Failure::Runtime(format!("internal error: unbound {n}"))
            }),
        Expr::Lam(parameter, body) => Ok(Value::Closure {
            parameter: parameter.clone(),
            body: Rc::new(*body.clone()),
            env: Rc::new(env.clone()),
            recursive: None,
        }),
        // ANCHOR: application
        Expr::App(function, argument) => {
            let function = evaluate(function, env, fuel, program, globals)?;
            let argument = evaluate(argument, env, fuel, program, globals)?;
            if let Value::Closure {
                parameter,
                body,
                env,
                recursive,
            } = &function
            {
                let mut local = (**env).clone();
                if let Some(bindings) = recursive {
                    local.extend(recursive_values(
                        bindings.clone(),
                        env.clone(),
                    ));
                }
                local.push((parameter.clone(), argument));
                evaluate(body, &local, fuel, program, globals)
            } else {
                Err("internal error: non-function application".into())
            }
        }
        // ANCHOR_END: application
        Expr::Let(group, body) => {
            let mut local = env.clone();
            bind_group(group, &mut local, fuel, program, globals)?;
            evaluate(body, &local, fuel, program, globals)
        }
        Expr::Con(id, _, fields) => Ok(Value::Con(
            id.clone(),
            fields
                .iter()
                .map(|e| evaluate(e, env, fuel, program, globals))
                .collect::<Result<_, _>>()?,
            program.constructors[id.index as usize].labels.clone(),
        )),
        Expr::PatternFail(span, _) => Err(failure(program, *span).into()),
        Expr::Match(m) => {
            let values = m
                .scruts
                .iter()
                .map(|id| {
                    evaluate(
                        &Expr::Var(id.clone()),
                        env,
                        fuel,
                        program,
                        globals,
                    )
                })
                .collect::<Result<Vec<_>, _>>()?;
            for row in &m.rows {
                let mut local = env.clone();
                if !row
                    .pats
                    .iter()
                    .zip(&values)
                    .all(|(p, v)| matches_pattern(p, v, &mut local))
                {
                    continue;
                }
                for group in &row.locals {
                    bind_group(group, &mut local, fuel, program, globals)?;
                }
                match &row.body {
                    core::RowBody::Plain(e) => {
                        return evaluate(e, &local, fuel, program, globals);
                    }
                    core::RowBody::Guarded(gs) => {
                        for (g, e) in gs {
                            let value = evaluate(
                                g, &local, fuel, program, globals,
                            )?;
                            if matches!(value,Value::Con(id,_,_) if id.name=="True")
                            {
                                return evaluate(
                                    e, &local, fuel, program, globals,
                                );
                            }
                        }
                    }
                }
            }
            Err(failure(program, m.span).into())
        }
        Expr::Prim(op, _, args, _) => {
            let values = args
                .iter()
                .map(|a| evaluate(a, env, fuel, program, globals))
                .collect::<Result<Vec<_>, _>>()?;
            primitive(*op, &values, program, globals)
        }
    }
}
fn primitive(
    op: Op,
    args: &[Value],
    program: &core::Program,
    _globals: &RefCell<Env>,
) -> Result<Value, Failure> {
    if let Op::Runtime(p) = op {
        return crate::primitives::evaluate(p, args, program);
    }
    if let [Value::Lit(Lit::String(a)), Value::Lit(Lit::String(b))] = args
        && op == Op::Append
    {
        return Ok(Value::Lit(Lit::String(format!("{a}{b}"))));
    }
    let [Value::Lit(Lit::Int(a)), Value::Lit(Lit::Int(b))] = args else {
        return Err("internal error: primitive operands".into());
    };
    if matches!(op, Op::Eq | Op::Lt | Op::Le) {
        let yes = match op {
            Op::Eq => a == b,
            Op::Lt => a < b,
            _ => a <= b,
        };
        let name = if yes { "True" } else { "False" };
        let c = program
            .constructors
            .iter()
            .find(|c| c.id.name == name)
            .ok_or("internal error: missing Bool constructor")?;
        return Ok(Value::Con(c.id.clone(), vec![], c.labels.clone()));
    }
    let value = match op {
        Op::Runtime(p) => {
            return crate::primitives::evaluate(p, args, program);
        }
        Op::Add => Lit::Int(normalize(a.wrapping_add(*b))),
        Op::Sub => Lit::Int(normalize(a.wrapping_sub(*b))),
        Op::Mul => Lit::Int(normalize(a.wrapping_mul(*b))),
        Op::Eq | Op::Lt | Op::Le => unreachable!(),
        Op::Div | Op::Mod => {
            if *b == 0 {
                return Err("divide by zero".into());
            }
            let (mut q, mut r) = (a / b, a % b);
            if r != 0 && (r < 0) != (*b < 0) {
                q -= 1;
                r += b;
            }
            Lit::Int(normalize(if op == Op::Div { q } else { r }))
        }
        Op::Append => {
            return Err("internal error: string append on Int".into());
        }
    };
    Ok(Value::Lit(value))
}
/// Evaluate top-level values exactly once in dependency order, then select main's value.
fn execute(
    program: &core::Program,
    mut fuel: usize,
    io: bool,
) -> Result<String, Failure> {
    let globals = RefCell::new(vec![]);
    for group in &program.groups {
        for b in &group.binds {
            if core::is_function(&b.rhs) {
                let value = evaluate(
                    &b.rhs,
                    &vec![],
                    &mut fuel,
                    program,
                    &globals,
                )?;
                globals.borrow_mut().push((b.name.clone(), value));
            }
        }
    }
    for group in &program.groups {
        for b in &group.binds {
            if !core::is_function(&b.rhs) {
                let value = evaluate(
                    &b.rhs,
                    &vec![],
                    &mut fuel,
                    program,
                    &globals,
                )?;
                globals.borrow_mut().push((b.name.clone(), value));
            }
        }
    }
    let value = globals
        .borrow()
        .iter()
        .find(|(n, _)| n.unique() == program.main.unique())
        .map(|(_, v)| v.clone())
        .ok_or("internal error: missing main")?;
    if io {
        let unit = program
            .constructors
            .iter()
            .find(|c| c.id.name == "()")
            .unwrap();
        let action = Expr::App(
            Box::new(Expr::Global(program.main.clone())),
            Box::new(Expr::Con(unit.id.clone(), vec![], vec![])),
        );
        evaluate(&action, &vec![], &mut fuel, program, &globals)?;
        Ok(String::new())
    } else {
        Ok(value.to_string())
    }
}
/// Evaluate a pure fragment; retained for compiler tests and REPL inspection.
pub fn run(program: &core::Program, fuel: usize) -> Result<String, String> {
    execute(program, fuel, false).map_err(|e| e.to_string())
}
/// Initialize globals, then run the checked IO action exactly once.
pub fn run_io(program: &core::Program, fuel: usize) -> Result<(), Failure> {
    execute(program, fuel, true).map(|_| ())
}
fn failure(program: &core::Program, span: crate::source::Span) -> String {
    let site = program
        .locations
        .iter()
        .find(|(s, _)| *s == span)
        .map(|(_, s)| s.as_str())
        .unwrap_or("<unknown>:1:1");
    format!("pattern match failure at {site}")
}
fn matches_pattern(p: &core::Pat, v: &Value, env: &mut Env) -> bool {
    match p {
        core::Pat::Wild => true,
        core::Pat::Var(id) => {
            env.push((id.clone(), v.clone()));
            true
        }
        core::Pat::As(id, p) => {
            env.push((id.clone(), v.clone()));
            matches_pattern(p, v, env)
        }
        core::Pat::Lit(Lit::Double(n)) => {
            matches!(v,Value::Lit(Lit::Double(m)) if f64::from_bits(*n)==f64::from_bits(*m))
        }
        core::Pat::Lit(l) => matches!(v,Value::Lit(actual) if l==actual),
        core::Pat::Con(id, ps) => match v {
            Value::Con(actual, vs, _)
                if id == actual && ps.len() == vs.len() =>
            {
                ps.iter().zip(vs).all(|(p, v)| matches_pattern(p, v, env))
            }
            _ => false,
        },
    }
}
/// Language termination is separate from an ordinary runtime failure.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Failure {
    Runtime(String),
    Exit(i32),
}
}

The driver flushes stdout at completion and before runtime diagnostics. Input primitives flush before reading, so a prompt reaches the user before the program blocks. The test runner accepts .in files and sends identical input to each engine. A pipe-handshake regression checks flushing independently of terminal buffering.

Existing programs need a small adjustment here. The driver no longer prints main for us, so we put the printing in the program itself. If a value has no Show instance, we’ll need to supply one or choose something printable from it. The old value printer remains available through --print-value for inspecting compiler fragments.

Running It

From the repository root, enter the chapter crate. These commands print an explicit action’s output and its inferred entry-point type:

$ cd crates/ch15_io
$ cargo run -q -- run tests/programs/io/hello.fun --lint
hello
$ cargo run -q -- dump --pass=types tests/programs/io/hello.fun
main : IO ()
$ cargo run -q -- run tests/programs/io/deferred.fun --lint
ok

Use --pass=core to find the dictionary arguments and the lambda taking unit. It’s worth comparing an unused print action with one that is actually sequenced by main. Both are values, but only the latter’s body runs. The Core interpreter is still our execution engine in this chapter.

Exercises

1. Warm-up. Replace the second Just in the example with a suitably annotated Nothing. Explain why its continuation is not called.
2. Warm-up. Compare constructing an unused print action with constructing one whose string argument calls error.
3. Intermediate. Trace the generated scopes for a do block containing a let, a tuple bind, and a shadowing bind.
4. Intermediate. Inspect a Monad IO dictionary in Core and identify every type affected by IO lowering.
5. Advanced. Extend the pipe-handshake test to issue two prompts and verify the order without relying on a terminal’s line buffering.

Further Reading

• The report’s do expressions and monadic library (Simon Marlow 2010).
• Higher-kinded constructor classes (Jones 1993).
• Dictionary passing and qualified types (Jones 1999).

Chapter 16: Pattern-Match Compilation

New files

• src/match_compile.rs
• src/usefulness.rs
• src/env.rs

Changed files

• src/core.rs
• src/core_lint.rs
• src/eval.rs
• src/io_lower.rs
• src/lib.rs
• src/main.rs

Motivation

Our interpreter tries patterns from top to bottom, which makes their meaning easy to follow. A native compiler needs to turn that process into instructions that inspect tags, load fields, and branch. We could translate each pattern separately, but we’d often inspect the same value again and again.

Instead, we’ll look at the patterns together. Put them in a matrix, choose a useful test, and divide the remaining work according to its result. This gives us a decision tree. Join points let different paths share the code they reach, including the next clause when a guard fails.

We can also ask whether any inputs slip through the patterns, or whether an earlier clause has already caught everything a later clause could match. It’s a pleasing connection. Understanding the shapes of values helps us both run patterns and explain mistakes in them.

The Language, Now

There is no new source syntax. Earlier programs keep the same results, including guards that fail after their patterns match:

f (Just x) | x < 0 = 0
f (Just x) = x
f Nothing = 99

main = print (f (Just 42))

The first clause recognizes Just 42, but its guard fails. Execution must try the second clause and return 42. It must not report pattern failure or skip to the Nothing clause. Local where bindings remain in scope for the guards and right-hand side of their own equation.

The checker can now show us holes in a match. W0001 includes example inputs that aren’t covered, and W0002 points out a clause that earlier clauses have made unreachable. These are warnings, so the program can still run. Encountering an uncovered input at runtime still reports fun: pattern match failure at FILE:LINE:COL.

Theory

Think of a match as a matrix whose rows are clauses and whose columns are scrutinees. Specializing a column for constructor C keeps rows that can match C, removes that constructor, and inserts its fields as new columns. A default matrix retains rows whose selected pattern can match any other value. This is the decision-tree approach described by Maranget (Maranget 2008).

Fun chooses the first column containing a refutable pattern in the first row. That simple heuristic is deterministic and easy to trace. It is not a claim to minimize the number of tests for every matrix. Wildcards, variables, and as-patterns do not inspect a value. Their bindings are recorded for the eventual clause body. Constructor patterns expose fields only after their tag has matched.

Finite datatypes have known constructor families. Integer and character literals need a default path because a finite set of tested literals cannot exhaust their value domain. String patterns become equality tests. Double patterns also use primitive equality, preserving the language’s floating comparison behavior, including equality of positive and negative zero.

Usefulness asks whether a candidate pattern vector admits a value not matched by preceding covering rows (Maranget 2007). A useless source row is redundant. A useful all-wildcard candidate supplies a missing-case witness. Guards complicate coverage because a matching pattern may still fall through. The implementation treats a guarded row as covering only when one guard is literally True. It does not attempt to prove arbitrary Boolean expressions.

One Question, Two Checks

There’s a neat way to turn both warnings into the same question. Does this pattern match anything the earlier patterns missed? Maranget calls such a pattern useful. We’ll write U(P, q) for this question, with earlier rows P and candidate pattern vector q. A witness is an actual shape that slips past P and matches q (Maranget 2007).

For reachability, P contains the covering rows before the current clause and q is that clause’s pattern vector. For exhaustiveness, P contains all covering rows and q is an all-wildcard vector. The first query asks whether a clause adds any cases. The second asks whether anything is still missing. It’s the rows together that determine coverage. A clause can be unreachable even when no single earlier clause covers it completely.

Consider a function with two arguments, Maybe Bool and Bool:

choose Nothing     _     = 0
choose (Just True) _     = 1
choose (Just _)    False = 2

Ignore the right-hand sides and retain the argument columns:

Ask whether (_, _) is useful. The first column contains both constructors of Maybe, so examine each constructor family member. Specializing for Nothing discards rows 2 and 3 and leaves a wildcard for the second argument. That branch is covered. Specializing for Just discards row 1 and replaces the first column with the constructor’s single field:

The True branch is covered by row 2. In the False branch, only row 3 remains, and it covers a second argument of False. The uncovered second argument is True. Rebuilding the constructor around the field gives the witness (Just False, True) for the original argument vector. Adding choose (Just False) True = 3 completes this match. Any subsequent clause is unreachable, even though no original clause alone covered every input.

Specialization and the Default Matrix

usefulness.rs implements the search on the first column. The selected pattern and constructor family determine the next problem:

1. Constructor candidate. For C(p1, ..., pk), keep rows headed by C or a wildcard. Replace C by its fields. Expand a wildcard to k wildcards. Drop rows headed by other constructors, and make the same expansion in the query.
2. Wildcard candidate, complete family. If every constructor of the column’s datatype appears, specialize for each. Any useful branch supplies a witness.
3. Wildcard candidate, incomplete family. Search the default matrix: retain only wildcard-headed rows and drop their first column. A useful suffix can be prefixed by a missing constructor. Literal domains are handled through this path, choosing a literal absent from the tested heads.

The zero-column case distinguishes an empty matrix from an empty row. With no rows, nothing covers the remaining empty vector, so it is useful. With an empty row, an earlier clause already matches everything left, so it is not useful. These small base cases let the search handle nested constructors without enumerating all values of a recursive datatype.

On return, the algorithm rebuilds each stripped constructor around the witness fields. Fun’s useful therefore returns an optional pattern vector, rather than just a Boolean. The warning driver can print a concrete missing shape, add that shape to its temporary coverage matrix, and search again for up to three examples.

Guards and the Limits of Coverage

A guarded clause can be unreachable because earlier clauses already cover its patterns. It can’t usually establish coverage itself, since its guard might fail. Fun checks the row against earlier coverage, then adds it only if it is unguarded or has a syntactically literal True guard. It does not solve arbitrary guard expressions. Consequently a reported gap can reflect this conservative policy, and a useful pattern does not prove that its guard will ever succeed.

The analysis uses typed constructor families and treats variables as wildcards. As-pattern names do not change coverage. It does not prove that recursive field types are inhabited. Compilation and checking remain separate. The decision tree must preserve clause order and guard fallthrough regardless of these warnings.

Sharing the Decision Tree

A join point names a continuation local to an expression. Its parameters carry the values needed by the shared body, and every jump is a fully applied tail transfer. Unlike an ordinary function, a join cannot escape or be passed as a value. This distinction anticipates the later use of joins in ANF (Maurer et al. 2017).

Implementation

The compiler’s internal row separates the remaining patterns from the eventual right-hand side. values records the values bound along the current decision path. target and params identify the shared clause body.

#![allow(unused)]
fn main() {
use crate::{
    core::{self, Alt, AltCon, Expr, Id, Pat, RowBody, Type},
    names,
    session::{Session, Stop},
    source::Span,
};
use std::collections::BTreeMap;
struct Compiler<'a> {
    sess: &'a mut Session,
    constructors: Vec<core::ConDecl>,
    truths: std::collections::BTreeSet<u32>,
}
impl Compiler<'_> {
    fn fresh(&mut self, ty: Type) -> Id {
        Id {
            name: self.sess.fresh_id("$case"),
            ty,
        }
    }
    fn fields(&self, con: &crate::data::ConId, ty: &Type) -> Vec<Type> {
        let c = &self.constructors[con.index as usize];
        let args = match ty {
            Type::Con(_, args) => args.as_slice(),
            Type::Bool => &[],
            _ => unreachable!("typed data scrutinee"),
        };
        c.fields
            .iter()
            .map(|t| crate::elaborate::instantiate(t, &c.parameters, args))
            .collect()
    }
    fn boolean(
        &mut self,
        test: Expr,
        yes: Expr,
        no: Expr,
        result: &Type,
    ) -> Expr {
        let truth = self
            .constructors
            .iter()
            .find(|c| c.id.name == "True")
            .unwrap()
            .id
            .clone();
        Expr::Case(
            Box::new(test),
            self.fresh(Type::Bool),
            result.clone(),
            vec![
                Alt {
                    con: AltCon::Con(truth),
                    binders: vec![],
                    rhs: yes,
                },
                Alt {
                    con: AltCon::Default,
                    binders: vec![],
                    rhs: no,
                },
            ],
        )
    }
    fn group(&mut self, g: core::BindGroup) -> core::BindGroup {
        core::BindGroup {
            recursive: g.recursive,
            binds: g
                .binds
                .into_iter()
                .map(|mut b| {
                    b.rhs = Box::new(self.expr(*b.rhs));
                    b
                })
                .collect(),
        }
    }
    fn expr(&mut self, e: Expr) -> Expr {
        match e {
            Expr::Match(m) => self.compile(m),
            Expr::Lam(i, b) => Expr::Lam(i, Box::new(self.expr(*b))),
            Expr::TyLam(v, b) => Expr::TyLam(v, Box::new(self.expr(*b))),
            Expr::TyApp(b, t) => Expr::TyApp(Box::new(self.expr(*b)), t),
            e @ Expr::App(..) => {
                let mut work = vec![Some(e)];
                let mut output = Vec::new();
                while let Some(job) = work.pop() {
                    match job {
                        Some(Expr::App(a, b)) => {
                            work.push(None);
                            work.push(Some(*b));
                            work.push(Some(*a));
                        }
                        Some(e) => output.push(self.expr(e)),
                        None => {
                            let b = output.pop().unwrap();
                            let a = output.pop().unwrap();
                            output
                                .push(Expr::App(Box::new(a), Box::new(b)));
                        }
                    }
                }
                output.pop().unwrap()
            }
            Expr::Let(g, b) => {
                Expr::Let(self.group(g), Box::new(self.expr(*b)))
            }
            Expr::Con(c, ts, args) => Expr::Con(
                c,
                ts,
                args.into_iter().map(|e| self.expr(e)).collect(),
            ),
            Expr::Prim(p, ts, args, s) => Expr::Prim(
                p,
                ts,
                args.into_iter().map(|e| self.expr(e)).collect(),
                s,
            ),
            other => other,
        }
    }
    fn compile(&mut self, m: core::Match) -> Expr {
        crate::usefulness::warn(
            self.sess,
            &m,
            &self.constructors,
            &self.truths,
        );
        let mut rows = vec![];
        let mut bodies = vec![];
        for r in m.rows {
            let mut params = vec![];
            for p in &r.pats {
                binders(p, &mut params)
            }
            let target = self.sess.fresh_id("$rhs");
            rows.push(Row {
                pats: r.pats,
                values: BTreeMap::new(),
                target: target.clone(),
                params: params.clone(),
            });
            bodies.push((target, params, r.locals, r.body));
        }
        let mut definitions = vec![];
        for (index, (target, params, locals, body)) in
            bodies.into_iter().enumerate().rev()
        {
            let fail = self.sess.fresh_id("$fail");
            let mut body = match body {
                RowBody::Plain(e) => self.expr(*e),
                RowBody::Guarded(gs) => {
                    let residual = self.tree(
                        m.scruts.clone(),
                        rows[index + 1..].to_vec(),
                        &m.result,
                        m.span,
                    );
                    definitions.push((fail.clone(), vec![], residual));
                    let mut fallback =
                        Expr::Jump(fail.clone(), vec![], m.result.clone());
                    for (g, e) in gs.into_iter().rev() {
                        let g = self.expr(g);
                        let e = self.expr(e);
                        fallback = self.boolean(g, e, fallback, &m.result)
                    }
                    fallback
                }
            };
            for g in locals.into_iter().rev() {
                body = Expr::Let(self.group(g), Box::new(body))
            }
            definitions.push((target, params, body));
        }
        let mut body = self.tree(m.scruts, rows, &m.result, m.span);
        for (id, params, rhs) in definitions.into_iter().rev() {
            body = Expr::Join(id, params, Box::new(rhs), Box::new(body))
        }
        body
    }
    fn tree(
        &mut self,
        scruts: Vec<Id>,
        mut rows: Vec<Row>,
        result: &Type,
        span: Span,
    ) -> Expr {
        if rows.is_empty() {
            return Expr::PatternFail(span, result.clone());
        }
        // Bind variables/as-patterns without copying their unique Core binders.
        for row in &mut rows {
            for (p, s) in row.pats.iter_mut().zip(&scruts) {
                loop {
                    match p.clone() {
                        Pat::Var(id) => {
                            row.values.insert(id.unique(), s.clone());
                            *p = Pat::Wild;
                            break;
                        }
                        Pat::As(id, inner) => {
                            row.values.insert(id.unique(), s.clone());
                            *p = *inner
                        }
                        _ => break,
                    }
                }
            }
        }
        let Some(column) =
            rows[0].pats.iter().position(|p| !matches!(p, Pat::Wild))
        else {
            let row = &rows[0];
            return Expr::Jump(
                row.target.clone(),
                row.params
                    .iter()
                    .map(|p| Expr::Var(row.values[&p.unique()].clone()))
                    .collect(),
                result.clone(),
            );
        };
        let scrut = scruts[column].clone();
        let mut heads = vec![];
        for row in &rows {
            let head = match &row.pats[column] {
                Pat::Con(c, _) => AltCon::Con(c.clone()),
                Pat::Lit(l) => AltCon::Lit(l.clone()),
                _ => continue,
            };
            if !heads.contains(&head) {
                heads.push(head)
            }
        }
        let mut alts = vec![];
        for head in heads {
            let fields = match &head {
                AltCon::Con(c) => self.fields(c, &scrut.ty),
                _ => vec![],
            };
            let params = fields
                .into_iter()
                .map(|t| self.fresh(t))
                .collect::<Vec<_>>();
            let mut specialized = vec![];
            for mut row in rows.clone() {
                let p = row.pats.remove(column);
                let fields = match (&head, p) {
                    (_, Pat::Wild) => vec![Pat::Wild; params.len()],
                    (AltCon::Con(c), Pat::Con(d, ps)) if *c == d => ps,
                    (AltCon::Lit(a), Pat::Lit(b)) if *a == b => vec![],
                    _ => continue,
                };
                row.pats.splice(column..column, fields);
                specialized.push(row)
            }
            let mut columns = scruts.clone();
            columns.splice(column..=column, params.clone());
            let rhs = self.tree(columns, specialized, result, span);
            alts.push(Alt {
                con: head,
                binders: params,
                rhs,
            });
        }
        let mut defaults = vec![];
        for mut row in rows {
            if matches!(row.pats[column], Pat::Wild) {
                row.pats.remove(column);
                defaults.push(row)
            }
        }
        let mut columns = scruts;
        columns.remove(column);
        let fallback = self.tree(columns, defaults, result, span);
        if matches!(scrut.ty, Type::String | Type::Double) {
            let mut body = fallback;
            for alt in alts.into_iter().rev() {
                let AltCon::Lit(l) = alt.con else {
                    unreachable!()
                };
                let primitive = if matches!(scrut.ty, Type::String) {
                    crate::primitives::Prim::StrEq
                } else {
                    crate::primitives::Prim::DblEq
                };
                let test = Expr::Prim(
                    crate::ast::Op::Runtime(primitive),
                    vec![],
                    vec![Expr::Var(scrut.clone()), Expr::Lit(l)],
                    span,
                );
                body = self.boolean(test, alt.rhs, body, result);
            }
            body
        } else {
            alts.push(Alt {
                con: AltCon::Default,
                binders: vec![],
                rhs: fallback,
            });
            Expr::Case(
                Box::new(Expr::Var(scrut.clone())),
                self.fresh(scrut.ty),
                result.clone(),
                alts,
            )
        }
    }
}
fn binders(p: &Pat, out: &mut Vec<Id>) {
    match p {
        Pat::Var(i) => out.push(i.clone()),
        Pat::As(i, p) => {
            out.push(i.clone());
            binders(p, out)
        }
        Pat::Con(_, ps) => {
            for p in ps {
                binders(p, out)
            }
        }
        _ => {}
    }
}
/// Compile every nested match; generated binders come from the shared unique supply.
pub fn compile(
    sess: &mut Session,
    mut program: core::Program,
) -> Result<core::Program, Stop> {
    let mut compiler = Compiler {
        sess,
        constructors: program.constructors.clone(),
        truths: program.groups.iter().flat_map(|g| &g.binds)
            .filter(|b| matches!(&*b.rhs, Expr::Con(c, _, _) if c.name == "True"))
            .map(|b| b.name.unique()).collect(),
    };
    program.groups = program
        .groups
        .into_iter()
        .map(|g| compiler.group(g))
        .collect();
    compiler.sess.finish(program)
}
#[derive(Clone)]
struct Row {
    pats: Vec<Pat>,
    values: BTreeMap<u32, Id>,
    target: names::Id,
    params: Vec<Id>,
}
}

Before building tests, Compiler::compile assigns each clause a parameterized right-hand-side join. It also compiles the residual matrix following that clause into a failure join. Guards run in order. If all fail, a jump enters that residual matrix. Several leaves can therefore reach one clause body without copying it, and several failed guards can use one fallback.

A constructor branch must bind fields at the scrutinee’s actual type arguments. The helper looks up the declaration and substitutes its parameters:

#![allow(unused)]
fn main() {
fn fields(&self, con: &crate::data::ConId, ty: &Type) -> Vec<Type> {
    let c = &self.constructors[con.index as usize];
    let args = match ty {
        Type::Con(_, args) => args.as_slice(),
        Type::Bool => &[],
        _ => unreachable!("typed data scrutinee"),
    };
    c.fields
        .iter()
        .map(|t| crate::elaborate::instantiate(t, &c.parameters, args))
        .collect()
}
}

For example, specializing Just at Maybe Int binds an Int, not the declaration’s uninstantiated type variable. The same rule matters for a record projection: its single-constructor match now becomes a tag branch and ordinary field binders. Core lint independently checks these instantiated types.

Compiler::tree handles the matrix recursively. An empty matrix becomes PatternFail. A first row with no refutable patterns jumps to its clause join, passing the values accumulated for its binders. Otherwise the selected column produces a flat Case, or equality tests for string and Double literals, with specialized subtrees and a default subtree.

The warning pass uses the original nested patterns, before that representation is lost. Its specialization helper is the matrix operation traced above:

#![allow(unused)]
fn main() {
use crate::{
    core::{ConDecl, Lit, Match, Pat, RowBody, Type},
    diagnostics::{Diagnostic, ErrorCode, Severity},
    session::Session,
};
fn peel(p: &Pat) -> &Pat {
    if let Pat::As(_, p) = p { peel(p) } else { p }
}
fn wild(p: &Pat) -> bool {
    matches!(peel(p), Pat::Wild | Pat::Var(_))
}
fn same(a: &Pat, b: &Pat) -> bool {
    match (peel(a), peel(b)) {
        (Pat::Con(a, _), Pat::Con(b, _)) => a == b,
        (Pat::Lit(Lit::Double(a)), Pat::Lit(Lit::Double(b))) => {
            f64::from_bits(*a) == f64::from_bits(*b)
        }
        (Pat::Lit(a), Pat::Lit(b)) => a == b,
        _ => false,
    }
}
fn fields(head: &Pat, ty: &Type, cons: &[ConDecl]) -> Vec<Type> {
    match peel(head) {
        Pat::Con(id, _) => {
            let c = &cons[id.index as usize];
            let args = match ty {
                Type::Con(_, args) => args.as_slice(),
                _ => &[],
            };
            c.fields
                .iter()
                .map(|t| {
                    crate::elaborate::instantiate(t, &c.parameters, args)
                })
                .collect()
        }
        _ => vec![],
    }
}
fn family(ty: &Type, cons: &[ConDecl]) -> Vec<Pat> {
    cons.iter()
        .filter(|c| match (&c.result, ty) {
            (Type::Bool, Type::Bool) => true,
            (Type::Con(a, _), Type::Con(b, _)) => a == b,
            _ => false,
        })
        .map(|c| Pat::Con(c.id.clone(), vec![Pat::Wild; c.fields.len()]))
        .collect()
}
/// Return a witness matched by the query but not by any covering row.
pub fn useful(
    matrix: &[Vec<Pat>],
    query: &[Pat],
    types: &[Type],
    cons: &[ConDecl],
) -> Option<Vec<Pat>> {
    if query.is_empty() {
        return matrix.is_empty().then(Vec::new);
    }
    let q = peel(&query[0]);
    if !wild(q) {
        let mut ts = fields(q, &types[0], cons);
        let n = ts.len();
        ts.extend_from_slice(&types[1..]);
        let mut qs = match q {
            Pat::Con(_, ps) => ps.clone(),
            _ => vec![],
        };
        qs.extend_from_slice(&query[1..]);
        let mut witness =
            useful(&specialize(matrix, q, n), &qs, &ts, cons)?;
        let children = witness.drain(..n).collect();
        let p = match q {
            Pat::Con(c, _) => Pat::Con(c.clone(), children),
            _ => q.clone(),
        };
        witness.insert(0, p);
        return Some(witness);
    }
    let heads = matrix
        .iter()
        .filter(|r| !wild(&r[0]))
        .map(|r| peel(&r[0]).clone())
        .collect::<Vec<_>>();
    let all = family(&types[0], cons);
    if !all.is_empty()
        && all.iter().all(|h| heads.iter().any(|p| same(h, p)))
    {
        for head in all {
            let mut ts = fields(&head, &types[0], cons);
            let n = ts.len();
            ts.extend_from_slice(&types[1..]);
            let mut qs = vec![Pat::Wild; n];
            qs.extend_from_slice(&query[1..]);
            if let Some(mut w) =
                useful(&specialize(matrix, &head, n), &qs, &ts, cons)
            {
                let children = w.drain(..n).collect();
                let Pat::Con(c, _) = head else { unreachable!() };
                w.insert(0, Pat::Con(c, children));
                return Some(w);
            }
        }
        None
    } else {
        let defaults = matrix
            .iter()
            .filter(|r| wild(&r[0]))
            .map(|r| r[1..].to_vec())
            .collect::<Vec<_>>();
        let mut witness =
            useful(&defaults, &query[1..], &types[1..], cons)?;
        let missing = all
            .into_iter()
            .find(|h| !heads.iter().any(|p| same(h, p)))
            .unwrap_or_else(|| {
                for n in 0..=heads.len() {
                    let p = match types[0] {
                        Type::Int => Pat::Lit(Lit::Int(n as i64)),
                        Type::Char => Pat::Lit(Lit::Char(
                            char::from_u32(97 + n as u32).unwrap_or('\0'),
                        )),
                        Type::String => {
                            Pat::Lit(Lit::String("x".repeat(n)))
                        }
                        Type::Double => {
                            Pat::Lit(Lit::Double((n as f64).to_bits()))
                        }
                        _ => return Pat::Wild,
                    };
                    if !heads.iter().any(|h| same(&p, h)) {
                        return p;
                    }
                }
                unreachable!()
            });
        witness.insert(0, missing);
        Some(witness)
    }
}
fn covers(
    body: &RowBody,
    truths: &std::collections::BTreeSet<u32>,
) -> bool {
    match body {
        RowBody::Plain(_) => true,
        RowBody::Guarded(gs) => gs.iter().any(|(g, _)| match g {
            crate::core::Expr::Con(c, _, _) => c.name == "True",
            crate::core::Expr::Global(id) => truths.contains(&id.unique()),
            _ => false,
        }),
    }
}
/// Warnings do not alter the decision tree; unmatched execution still fails at runtime.
pub fn warn(
    sess: &mut Session,
    m: &Match,
    cons: &[ConDecl],
    truths: &std::collections::BTreeSet<u32>,
) {
    let types = m.scruts.iter().map(|i| i.ty.clone()).collect::<Vec<_>>();
    let mut matrix = vec![];
    for (index, row) in m.rows.iter().enumerate() {
        if useful(&matrix, &row.pats, &types, cons).is_none()
            && !(index > 0 && m.rows[index - 1].span == row.span)
        {
            let mut d = Diagnostic::error(
                ErrorCode::Redundant,
                "clause can never match",
                row.span,
            );
            d.severity = Severity::Warning;
            sess.emit(d);
        }
        if covers(&row.body, truths) {
            matrix.push(row.pats.clone())
        }
    }
    let mut missing = vec![];
    for _ in 0..3 {
        let Some(p) =
            useful(&matrix, &vec![Pat::Wild; types.len()], &types, cons)
        else {
            break;
        };
        missing.push(
            p.iter()
                .map(ToString::to_string)
                .collect::<Vec<_>>()
                .join(" "),
        );
        matrix.push(p)
    }
    if !missing.is_empty() {
        let mut d = Diagnostic::error(
            ErrorCode::NonExhaustive,
            "non-exhaustive pattern match",
            m.span,
        );
        d.severity = Severity::Warning;
        d.notes.push(format!("missing: {}", missing.join("; ")));
        sess.emit(d)
    }
}
fn specialize(
    matrix: &[Vec<Pat>],
    head: &Pat,
    arity: usize,
) -> Vec<Vec<Pat>> {
    matrix
        .iter()
        .filter_map(|row| {
            let mut fields = if wild(&row[0]) {
                vec![Pat::Wild; arity]
            } else if same(&row[0], head) {
                match peel(&row[0]) {
                    Pat::Con(_, ps) => ps.clone(),
                    _ => vec![],
                }
            } else {
                return None;
            };
            fields.extend_from_slice(&row[1..]);
            Some(fields)
        })
        .collect()
}
}

useful carries the candidate vector and column types alongside the matrix. Its driver repeatedly asks for useful witnesses and records diagnostics:

#![allow(unused)]
fn main() {
use crate::{
    core::{ConDecl, Lit, Match, Pat, RowBody, Type},
    diagnostics::{Diagnostic, ErrorCode, Severity},
    session::Session,
};
fn peel(p: &Pat) -> &Pat {
    if let Pat::As(_, p) = p { peel(p) } else { p }
}
fn wild(p: &Pat) -> bool {
    matches!(peel(p), Pat::Wild | Pat::Var(_))
}
fn same(a: &Pat, b: &Pat) -> bool {
    match (peel(a), peel(b)) {
        (Pat::Con(a, _), Pat::Con(b, _)) => a == b,
        (Pat::Lit(Lit::Double(a)), Pat::Lit(Lit::Double(b))) => {
            f64::from_bits(*a) == f64::from_bits(*b)
        }
        (Pat::Lit(a), Pat::Lit(b)) => a == b,
        _ => false,
    }
}
fn specialize(
    matrix: &[Vec<Pat>],
    head: &Pat,
    arity: usize,
) -> Vec<Vec<Pat>> {
    matrix
        .iter()
        .filter_map(|row| {
            let mut fields = if wild(&row[0]) {
                vec![Pat::Wild; arity]
            } else if same(&row[0], head) {
                match peel(&row[0]) {
                    Pat::Con(_, ps) => ps.clone(),
                    _ => vec![],
                }
            } else {
                return None;
            };
            fields.extend_from_slice(&row[1..]);
            Some(fields)
        })
        .collect()
}
fn fields(head: &Pat, ty: &Type, cons: &[ConDecl]) -> Vec<Type> {
    match peel(head) {
        Pat::Con(id, _) => {
            let c = &cons[id.index as usize];
            let args = match ty {
                Type::Con(_, args) => args.as_slice(),
                _ => &[],
            };
            c.fields
                .iter()
                .map(|t| {
                    crate::elaborate::instantiate(t, &c.parameters, args)
                })
                .collect()
        }
        _ => vec![],
    }
}
fn family(ty: &Type, cons: &[ConDecl]) -> Vec<Pat> {
    cons.iter()
        .filter(|c| match (&c.result, ty) {
            (Type::Bool, Type::Bool) => true,
            (Type::Con(a, _), Type::Con(b, _)) => a == b,
            _ => false,
        })
        .map(|c| Pat::Con(c.id.clone(), vec![Pat::Wild; c.fields.len()]))
        .collect()
}
/// Return a witness matched by the query but not by any covering row.
pub fn useful(
    matrix: &[Vec<Pat>],
    query: &[Pat],
    types: &[Type],
    cons: &[ConDecl],
) -> Option<Vec<Pat>> {
    if query.is_empty() {
        return matrix.is_empty().then(Vec::new);
    }
    let q = peel(&query[0]);
    if !wild(q) {
        let mut ts = fields(q, &types[0], cons);
        let n = ts.len();
        ts.extend_from_slice(&types[1..]);
        let mut qs = match q {
            Pat::Con(_, ps) => ps.clone(),
            _ => vec![],
        };
        qs.extend_from_slice(&query[1..]);
        let mut witness =
            useful(&specialize(matrix, q, n), &qs, &ts, cons)?;
        let children = witness.drain(..n).collect();
        let p = match q {
            Pat::Con(c, _) => Pat::Con(c.clone(), children),
            _ => q.clone(),
        };
        witness.insert(0, p);
        return Some(witness);
    }
    let heads = matrix
        .iter()
        .filter(|r| !wild(&r[0]))
        .map(|r| peel(&r[0]).clone())
        .collect::<Vec<_>>();
    let all = family(&types[0], cons);
    if !all.is_empty()
        && all.iter().all(|h| heads.iter().any(|p| same(h, p)))
    {
        for head in all {
            let mut ts = fields(&head, &types[0], cons);
            let n = ts.len();
            ts.extend_from_slice(&types[1..]);
            let mut qs = vec![Pat::Wild; n];
            qs.extend_from_slice(&query[1..]);
            if let Some(mut w) =
                useful(&specialize(matrix, &head, n), &qs, &ts, cons)
            {
                let children = w.drain(..n).collect();
                let Pat::Con(c, _) = head else { unreachable!() };
                w.insert(0, Pat::Con(c, children));
                return Some(w);
            }
        }
        None
    } else {
        let defaults = matrix
            .iter()
            .filter(|r| wild(&r[0]))
            .map(|r| r[1..].to_vec())
            .collect::<Vec<_>>();
        let mut witness =
            useful(&defaults, &query[1..], &types[1..], cons)?;
        let missing = all
            .into_iter()
            .find(|h| !heads.iter().any(|p| same(h, p)))
            .unwrap_or_else(|| {
                for n in 0..=heads.len() {
                    let p = match types[0] {
                        Type::Int => Pat::Lit(Lit::Int(n as i64)),
                        Type::Char => Pat::Lit(Lit::Char(
                            char::from_u32(97 + n as u32).unwrap_or('\0'),
                        )),
                        Type::String => {
                            Pat::Lit(Lit::String("x".repeat(n)))
                        }
                        Type::Double => {
                            Pat::Lit(Lit::Double((n as f64).to_bits()))
                        }
                        _ => return Pat::Wild,
                    };
                    if !heads.iter().any(|h| same(&p, h)) {
                        return p;
                    }
                }
                unreachable!()
            });
        witness.insert(0, missing);
        Some(witness)
    }
}
fn covers(
    body: &RowBody,
    truths: &std::collections::BTreeSet<u32>,
) -> bool {
    match body {
        RowBody::Plain(_) => true,
        RowBody::Guarded(gs) => gs.iter().any(|(g, _)| match g {
            crate::core::Expr::Con(c, _, _) => c.name == "True",
            crate::core::Expr::Global(id) => truths.contains(&id.unique()),
            _ => false,
        }),
    }
}
/// Warnings do not alter the decision tree; unmatched execution still fails at runtime.
pub fn warn(
    sess: &mut Session,
    m: &Match,
    cons: &[ConDecl],
    truths: &std::collections::BTreeSet<u32>,
) {
    let types = m.scruts.iter().map(|i| i.ty.clone()).collect::<Vec<_>>();
    let mut matrix = vec![];
    for (index, row) in m.rows.iter().enumerate() {
        if useful(&matrix, &row.pats, &types, cons).is_none()
            && !(index > 0 && m.rows[index - 1].span == row.span)
        {
            let mut d = Diagnostic::error(
                ErrorCode::Redundant,
                "clause can never match",
                row.span,
            );
            d.severity = Severity::Warning;
            sess.emit(d);
        }
        if covers(&row.body, truths) {
            matrix.push(row.pats.clone())
        }
    }
    let mut missing = vec![];
    for _ in 0..3 {
        let Some(p) =
            useful(&matrix, &vec![Pat::Wild; types.len()], &types, cons)
        else {
            break;
        };
        missing.push(
            p.iter()
                .map(ToString::to_string)
                .collect::<Vec<_>>()
                .join(" "),
        );
        matrix.push(p)
    }
    if !missing.is_empty() {
        let mut d = Diagnostic::error(
            ErrorCode::NonExhaustive,
            "non-exhaustive pattern match",
            m.span,
        );
        d.severity = Severity::Warning;
        d.notes.push(format!("missing: {}", missing.join("; ")));
        sess.emit(d)
    }
}
}

Generated do-pattern fallback rows share the originating span. The diagnostic pass suppresses redundant warnings for those synthetic adjacent rows, while retaining warnings for source clauses. Warning analysis does not choose the runtime branches. A mistake in a warning must not silently change evaluation.

Core lint now checks flat alternative shape, constructor field types, globally unique binders, and join argument types and arities. A jump must be in tail position relative to its join. Entering a non-tail subexpression clears the available outer joins. The subexpression may establish its own local joins. The Core interpreter keeps evaluation and return frames in an explicit vector. A source call changes the current expression and environment rather than calling Rust recursively. A jump unwinds frames to its lexical join and transfers control to that body. Closures borrow code through stable indices, so calling a function does not clone its syntax tree. Constructor and environment destruction also use a worklist, preventing a long list from overflowing the stack when released. Tests run non-tail recursion and list reclamation on a 256 KiB host stack.

Saved environments share an immutable balanced tree. Capturing a scope copies one Rc, while adding a binding copies only the search path. env.rs implements the update with a work vector. This keeps a growing scope from being copied in full whenever the interpreter saves a continuation. Recursive closures refer to a machine-owned group by index, so calls reuse the group without creating a reference-count cycle.

Running It

$ cd crates/ch16_match
$ cargo run -q -- run tests/programs/match/guard-fallback.fun --lint
42
$ cargo run -q -- dump --pass=types tests/programs/match/guard-fallback.fun
main : IO ()

For the transformation itself, dump the same file with --pass=core and then --pass=match. The former retains nested Match. The latter exposes flat Case, right-hand-side joins, and guard-failure jumps. The dumps include the Prelude, so the small no-Prelude cases in tests/matches.rs are useful for studying one decision tree at a time.

We check the translation by running matches both before and after compilation. Coverage needs its own check. For small Boolean patterns we can enumerate all possible inputs and compare that direct answer with the usefulness algorithm. This catches a different kind of mistake from a wrong runtime branch.

Exercises

1. Warm-up. Draw the decision tree for the example and mark the failing guard’s destination.
2. Intermediate. Add a wildcard clause before a constructor clause and predict the redundant-clause warning before running the checker.
3. Intermediate. Specialize a two-column matrix whose first row begins with a variable and whose second pattern is a constructor.
4. Advanced. Change the column heuristic in an experimental copy. Compare tree sizes while keeping the full before/after execution corpus unchanged.
5. Advanced. Construct malformed Core that jumps to an outer join from a non-tail expression, and explain the continuation that would be discarded.

Further Reading

• Decision trees and column-selection heuristics (Maranget 2008).
• Usefulness, exhaustiveness, and redundancy (Maranget 2007).
• Join points as a compiler intermediate representation (Maurer et al. 2017).
• Source pattern and guard semantics (Simon Marlow 2010).

For a standalone Rust treatment of the same matrix operations, see Patternkit. Fun keeps its implementation in the chapter so that the checking algorithm remains visible here.

Chapter 17: The Prelude and Deriving

New files

• src/derive.rs

Changed files

• src/primitives.rs
• src/desugar.rs
• src/ast.rs
• src/core_lint.rs
• src/eval.rs
• src/lexer.rs
• src/lib.rs
• src/main.rs
• src/rename.rs

Motivation

A language starts to feel like a language when you can reach for map, foldr, or maybe without writing them yourself every time. We now have enough Fun to write its standard library in Fun. That’s a good milestone!

We’ll also teach the compiler to write the repetitive parts. Given a datatype, deriving generates an ordinary instance for equality, ordering, or display. The generated code goes through the same checker as code we’d write by hand. There’s no secret equality operation in the interpreter waiting to rescue it.

This chapter brings the interpreted language together. Take a little time to play with it before we head into the back end. Small library functions are also excellent compiler examples. Their types and definitions often tell the whole story in just a few lines.

The Language, Now

A datatype may request deriving Eq or a nonempty parenthesized list drawn from Eq, Ord, and Show. This example constructs its record fields in a different order from their declaration:

data P a = P {x :: a, y :: Int} deriving (Eq, Ord, Show)

main = print (Just (P {y=2,x=Left 1} :: P (Either Int Bool)))

Derived equality compares constructors and then their fields. Ordering uses constructor declaration order, followed by lexicographic field order. Derived Show prints record fields in declaration order, regardless of construction order, and inserts parentheses around nested constructor applications where needed. Lists use comma-separated brackets. [Char] is still a list, not a string. Functions have no derived comparison or display instance.

The completed Prelude provides list folds and traversals, finite generation, string splitting and joining, numeric conversions, character operations, and monadic control. [a..b] is an inclusive Int range. iterateN produces a bounded sequence. Infinite lists are unavailable because constructor fields are strict. foldl' and foldl have the same strict behavior here.

Use ++ to append lists and <> to append strings. Numeric literals still have fixed types, so sum and product operate on Int lists. Their starting values are integer literals, and Fun’s Num class has no operation for turning a literal into an arbitrary numeric type.

Putting Small Functions Together

Now we can write something compact enough to read in one breath.

total = sum . map (\x -> x * x) . filter even

main = print (total [1..10])

This prints 220. Read the composition from right to left. Keep the even numbers, square each one, then add them up. Each function does one familiar job, and (.) connects the result of one to the input of the next. We don’t have to name a loop index or describe how to advance through the list.

That is a beautiful way to express the calculation. It doesn’t mean the work has vanished. Fun is strict, and this program builds intermediate lists. Later optimizations could remove them, but the useful separation is already here. We can understand what the program means before choosing how to make it faster.

Theory

Imagine writing equality for a tree by hand. Empty trees are equal. Two nodes are equal when their corresponding fields are equal. Different constructors aren’t equal. The datatype declaration already tells us enough to write those clauses, so let’s have the compiler write them.

That’s deriving. We generate an ordinary instance, then check it just as we would check a handwritten one. The Haskell Report specifies the structural behavior (Simon Marlow 2010). We adapt it to Fun’s records, primitive strings, and smaller Show interface.

A parameter used in a field usually introduces a corresponding instance constraint. A phantom parameter does not. For data Token a = Token Int, equality needs no Eq a dictionary because no value of type a is examined. Type synonyms must be expanded before deciding which parameters occur in fields. The normal instance solver then checks whether the generated context actually suffices for every field operation (Jones 1999). Deriving is not an escape from those checks.

Printing constructors has a small but important wrinkle. Just (Left 3) needs parentheses, but Left 3 on its own doesn’t. A function of type a -> String can’t see where its result will be used. We need to pass that surrounding precedence in as well.

Fun’s Show dictionary has an internal _showsPrec method for this purpose. Handwritten instances inherit a default, while derived instances implement it structurally. Top-level show starts at precedence zero. Positional constructor arguments use eleven, which asks nested constructor applications to parenthesize themselves. Record fields use ordinary show inside their labelled braces.

Strictness changes another familiar library definition. An ordinary top-level undefined = error "undefined" would fail during startup, even if unused. Instead, an unshadowed reference to the Prelude’s undefined is a scoped abbreviation for applying a unit-taking helper. This preserves failure at the use site without introducing a thunk or a lazy binding. The evaluation-strategy distinction from Chapter 5 remains essential (Pierce 2002).

Implementation

derive::derive runs immediately before class collection and lexical renaming. Generated terms retain the datatype’s source span, so a rejected field operation can point back to the declaration. The pass expands aliases when collecting used parameters, selects one of three generators, and appends ordinary instance declarations:

#![allow(unused)]
fn main() {
use crate::{
    ast::*,
    diagnostics::{Diagnostic, ErrorCode},
    session::{Session, Stop},
    source::Span,
};
use std::collections::BTreeSet;
struct Builder {
    span: Span,
}
impl Builder {
    fn expr(&self, kind: Kind) -> Expr {
        Expr {
            kind,
            span: self.span,
        }
    }
    fn var(&self, name: &str) -> Expr {
        self.expr(Kind::Var(name.into()))
    }
    fn string(&self, text: &str) -> Expr {
        self.expr(Kind::String(text.into()))
    }
    fn call(&self, name: &str, args: Vec<Expr>) -> Expr {
        args.into_iter().fold(self.var(name), |f, x| {
            self.expr(Kind::App(Box::new(f), Box::new(x)))
        })
    }
    fn pat(&self, name: &str) -> Pat {
        Pat {
            kind: PatKind::Var(name.into()),
            span: self.span,
        }
    }
    fn constructor(&self, c: &ConstructorDecl, prefix: &str) -> Pat {
        Pat {
            kind: PatKind::Con(
                c.name.clone(),
                (0..c.fields.len())
                    .map(|i| self.pat(&format!("{prefix}{i}")))
                    .collect(),
            ),
            span: self.span,
        }
    }
    fn row(&self, patterns: Vec<Pat>, expr: Expr) -> Row {
        Row {
            patterns,
            body: RowBody::Plain(Box::new(expr)),
            locals: vec![],
            span: self.span,
        }
    }
    fn binding(&self, name: &str, rows: Vec<Row>) -> Binding {
        Binding {
            name: name.into(),
            rhs: self.expr(Kind::Equations(rows)),
            nonrecursive: vec![],
            span: self.span,
        }
    }
    fn append(&self, pieces: Vec<Expr>) -> Expr {
        pieces
            .into_iter()
            .reduce(|a, b| self.call("<>", vec![a, b]))
            .unwrap_or_else(|| self.string(""))
    }
    fn eq(&self, d: &DataDecl) -> Binding {
        let mut rows = vec![];
        for (i, a) in d.constructors.iter().enumerate() {
            for (j, b) in d.constructors.iter().enumerate() {
                let mut rhs =
                    self.var(if i == j { "True" } else { "False" });
                if i == j {
                    for k in (0..a.fields.len()).rev() {
                        let test = self.call(
                            "==",
                            vec![
                                self.var(&format!("x{k}")),
                                self.var(&format!("y{k}")),
                            ],
                        );
                        rhs = self.expr(Kind::If(
                            Box::new(test),
                            Box::new(rhs),
                            Box::new(self.var("False")),
                        ));
                    }
                }
                rows.push(self.row(
                    vec![
                        self.constructor(a, "x"),
                        self.constructor(b, "y"),
                    ],
                    rhs,
                ));
            }
        }
        self.binding("==", rows)
    }
    fn ord(&self, d: &DataDecl) -> Binding {
        let mut rows = vec![];
        for (i, a) in d.constructors.iter().enumerate() {
            for (j, b) in d.constructors.iter().enumerate() {
                let mut rhs = self.var(if i < j {
                    "LT"
                } else if i > j {
                    "GT"
                } else {
                    "EQ"
                });
                if i == j {
                    for k in (0..a.fields.len()).rev() {
                        let comparison = self.call(
                            "compare",
                            vec![
                                self.var(&format!("x{k}")),
                                self.var(&format!("y{k}")),
                            ],
                        );
                        let equal = Pat {
                            kind: PatKind::Con("EQ".into(), vec![]),
                            span: self.span,
                        };
                        rhs = self.expr(Kind::Case(
                            Box::new(comparison),
                            vec![
                                self.row(vec![equal], rhs),
                                self.row(
                                    vec![self.pat("order")],
                                    self.var("order"),
                                ),
                            ],
                        ));
                    }
                }
                rows.push(self.row(
                    vec![
                        self.constructor(a, "x"),
                        self.constructor(b, "y"),
                    ],
                    rhs,
                ));
            }
        }
        self.binding("compare", rows)
    }
    fn show(&self, d: &DataDecl) -> Vec<Binding> {
        let mut rows = vec![];
        for c in &d.constructors {
            let mut pieces = vec![self.string(&c.name)];
            if let Some(labels) = &c.labels {
                pieces.push(self.string(" {"));
                for (i, label) in labels.iter().enumerate() {
                    pieces.push(self.string(&format!(
                        "{}{label} = ",
                        if i == 0 { "" } else { ", " }
                    )));
                    pieces.push(
                        self.call("show", vec![self.var(&format!("x{i}"))]),
                    );
                }
                pieces.push(self.string("}"));
            } else {
                for i in 0..c.fields.len() {
                    pieces.push(self.string(" "));
                    pieces.push(self.call(
                        "_showsPrec",
                        vec![
                            self.expr(Kind::Int(11)),
                            self.var(&format!("x{i}")),
                        ],
                    ));
                }
            }
            let mut rhs = self.append(pieces);
            if !c.fields.is_empty() {
                let test = self.call(
                    ">",
                    vec![self.var("p"), self.expr(Kind::Int(10))],
                );
                rhs = self.call("_showParen", vec![test, rhs]);
            }
            rows.push(
                self.row(
                    vec![self.pat("p"), self.constructor(c, "x")],
                    rhs,
                ),
            );
        }
        let show = self.binding(
            "show",
            vec![self.row(
                vec![self.pat("value")],
                self.call(
                    "_showsPrec",
                    vec![self.expr(Kind::Int(0)), self.var("value")],
                ),
            )],
        );
        vec![show, self.binding("_showsPrec", rows)]
    }
}
fn variables(ty: &TypeSyntax, out: &mut BTreeSet<String>) {
    match ty {
        TypeSyntax::Name(n) => {
            out.insert(n.clone());
        }
        TypeSyntax::App(a, b) | TypeSyntax::Arrow(a, b) => {
            variables(a, out);
            variables(b, out);
        }
        TypeSyntax::Qualified(_, t) => variables(t, out),
    }
}
/// Generate only Eq, Ord and Show. Generated terms retain the declaration span.
pub fn derive(
    sess: &mut Session,
    program: &mut Program,
) -> Result<(), Stop> {
    for d in &program.data {
        if d.deriving.is_empty() {
            continue;
        }
        let build = Builder { span: d.span };
        let mut used = BTreeSet::new();
        for c in &d.constructors {
            for ty in &c.fields {
                let expanded =
                    crate::kinds::expand(ty, &program.aliases, d.span)
                        .map_err(|e| {
                            sess.emit(e);
                            Stop
                        })?;
                variables(&expanded, &mut used);
            }
        }
        for class in &d.deriving {
            let methods = match class.as_str() {
                "Eq" => vec![build.eq(d)],
                "Ord" => vec![build.ord(d)],
                "Show" => build.show(d),
                _ => {
                    sess.emit(Diagnostic::error(
                        ErrorCode::Instance,
                        "only Eq, Ord and Show can be derived",
                        d.span,
                    ));
                    return Err(Stop);
                }
            };
            let context = d
                .parameters
                .iter()
                .filter(|p| used.contains(*p))
                .map(|p| PredicateSyntax {
                    class: class.clone(),
                    variable: p.clone(),
                })
                .collect();
            let head = d.parameters.iter().fold(
                TypeSyntax::Name(d.name.clone()),
                |a, p| {
                    TypeSyntax::App(
                        Box::new(a),
                        Box::new(TypeSyntax::Name(p.clone())),
                    )
                },
            );
            program.instances.push(InstanceDecl {
                class: class.clone(),
                head,
                context,
                methods,
                span: d.span,
            });
        }
    }
    Ok(())
}
}

The builders construct the existing surface expression and pattern types. Equality generates a clause for each pair of constructors. Unequal constructors return False. Matching constructors compare fields from left to right, stopping at the first unequal pair:

#![allow(unused)]
fn main() {
fn eq(&self, d: &DataDecl) -> Binding {
    let mut rows = vec![];
    for (i, a) in d.constructors.iter().enumerate() {
        for (j, b) in d.constructors.iter().enumerate() {
            let mut rhs =
                self.var(if i == j { "True" } else { "False" });
            if i == j {
                for k in (0..a.fields.len()).rev() {
                    let test = self.call(
                        "==",
                        vec![
                            self.var(&format!("x{k}")),
                            self.var(&format!("y{k}")),
                        ],
                    );
                    rhs = self.expr(Kind::If(
                        Box::new(test),
                        Box::new(rhs),
                        Box::new(self.var("False")),
                    ));
                }
            }
            rows.push(self.row(
                vec![
                    self.constructor(a, "x"),
                    self.constructor(b, "y"),
                ],
                rhs,
            ));
        }
    }
    self.binding("==", rows)
}
}

Ordering follows the same constructor-pair structure. For a matching pair it compares each field, continuing only when the result is EQ. Show instead builds string expressions from constructor names, field labels, punctuation, and recursive _showsPrec calls. These expressions pass through ordinary renaming, inference, dictionary elaboration, match compilation, and Core lint. Requesting an unsupported class reports E0211. Requesting Ord without the required equality evidence also fails through the existing instance checks.

The library lives in prelude.fun, embedded ahead of the user program. Its private helper references are resolved within that scope, so a user binding cannot silently change the implementation of a Prelude function. Inclusive ranges check the upper bound before incrementing. A range ending at the largest 63-bit integer must terminate rather than wrap around.

Character classification and simple case conversion use checked-in Unicode 17.0.0 tables in unicode.fun. tools/unicode.py records the upstream source and its digest, and the data license is retained. The generated tables are ordinary compact Fun strings. General-category predicates and simple case mappings therefore execute through the language rather than adding a large set of new primitives. isDigit deliberately recognizes ASCII decimal digits. Not every character with a Unicode numeric classification satisfies it.

A library also teaches us where the compiler is doing unnecessary work. Walking a list shouldn’t copy its entire tail at every step. We share immutable constructor field vectors with Rc, and Core lint removes local bindings on scope exit instead of copying its whole environment. These are useful reminders to look at the cost of our Rust representation as well as the Fun program.

Running It

$ cd crates/ch17_prelude
$ cargo run -q -- run tests/programs/prelude/derive-show-record.fun --lint
Just (P {x = Left 1, y = 2})
$ cargo run -q -- dump --pass=types tests/programs/prelude/derive-show-record.fun
main : IO ()

The output demonstrates both declaration-order record fields and parentheses around the record constructor beneath Just. --pass=core shows the generated instance dictionaries. --pass=match shows their compiled structural tests. The separate derive-show-tree and derive-show-literals fixtures cover nested applications and escaping.

Library edge cases make good experiments. Try a singleton range at the largest Int, an empty list passed to a fold, or a derived instance with a phantom parameter. The little examples are doing real work here. A boundary case can explain a library definition more clearly than a long ordinary input.

Exercises

1. Warm-up. Derive Eq, Ord, and Show for a two-constructor tree and compare the result with a handwritten instance.
2. Intermediate. Add an unused datatype parameter and inspect whether its dictionary appears in the derived instance context.
3. Intermediate. Trace the precedence passed while displaying Just (Left (Just 3)).
4. Intermediate. Test a singleton range at the maximum Int and explain why the order of the bound check and increment matters.
5. Advanced. Measure constructor-tail copying on a Unicode lookup before and after immutable field-vector sharing, without changing the Fun program.

Further Reading

• Standard derived instances and the Prelude (Simon Marlow 2010).
• Instance contexts and entailment (Jones 1999).
• Classes and derived instances in the Haskell Report (Simon Marlow 2010).
• Operational semantics and evaluation strategies (Pierce 2002).

Chapter 18: A-Normal Form and Join Points

New files

• src/erase.rs
• src/anf.rs
• src/anf_simplify.rs
• src/anf_machine.rs
• src/anf_lint.rs

Changed files

• src/lib.rs
• src/main.rs

Motivation

Consider f (g x) (h y). To run it, we need to evaluate the function and its arguments in the right order, keep the result of g x while computing h y, and finally make the call. Our interpreter has been doing that bookkeeping for us. A code generator needs to see the steps.

A-normal form, usually shortened to ANF, writes those intermediate results down as named bindings. Function calls and other operations then take simple operands rather than nested computations. The name sounds rather grand for what amounts to introducing some useful local variables.

This also gives us a good place to bring back the CEK machine from Chapter 5. We’ll run ANF with an explicit continuation stack, now with all of Fun’s data, dictionaries, IO, and join points. We can compare its answers with Core while getting the program ready for native code.

The Language, Now

Let’s follow a case expression whose result is used by another computation.

main = print (3 + (case Just 4 of { Just x -> x; Nothing -> 0 }))

Whichever alternative returns a value, the program must add three and print once. ANF makes that common continuation explicit as a join rather than copying it into each alternative. The new --engine=anf selects the iterative machine and is the default. --engine=core retains the reference interpreter.

--no-simplify exposes the ANF produced before the optional rewrites. Both forms must preserve stdout, the first stderr line, and process status. In particular, strict evaluation still runs an unused binding’s initializer. A failing division cannot disappear merely because its result has no uses.

Theory

In f (g x) (h y), the interesting work is in the calls. The names themselves just refer to values. ANF makes that distinction part of the syntax. An atom is a literal or a reference to an available value. A right-hand side performs one operation on atoms, and a Let gives the result a name. Nested evaluation has become an explicit sequence (Flanagan et al. 1993).

Conversion receives a context describing what to do with a result. At the end of a function it returns the atom. Inside an expression it binds the atom and continues. At the end of a case alternative it can jump to a shared continuation. This representation keeps joins local and second-class, following the motivation for join points discussed by Maurer and colleagues (Maurer et al. 2017). It does not turn every function into a function that explicitly receives a continuation.

Type erasure is justified by the role of System F’s type abstractions and applications: they select and describe computations but do not themselves perform runtime work (Pierce 2002). Dictionary arguments are different. They contain actual method implementations and must remain as ordinary values. IO already has its unit-function representation before erasure.

Tail position is a property of the remaining work. If a function call supplies the current function’s result directly, the machine needs no return frame for that activation. A non-tail call must remember its pending computation. Constant host-stack use therefore does not imply constant memory for every recursive program. Pending non-tail work can still grow the explicit continuation stack. This is the practical advantage of making the CEK continuation visible (Felleisen and Friedman 1986).

Implementation

erase::erase preserves the order of global initialization while removing executable type information. A postorder worklist drops TyLam and TyApp, keeps dictionary terms, and rejects any nested Match that escaped the previous pass. Read-only constructor and location metadata remains available for primitives, printers, and diagnostics.

#![allow(unused)]
fn main() {
use crate::{ast::Op, core, data::ConId, names::Id, source::Span};
#[derive(Clone, Debug)]
/// Untyped Core retains strict evaluation order and lexical join points.
pub enum Expr {
    Var(Id),
    Global(Id),
    Lit(core::Lit),
    Lam(Id, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Let(bool, Vec<(Id, Expr)>, Box<Expr>),
    Con(ConId, Vec<Expr>),
    Prim(Op, Vec<Expr>, Span),
    Case(Box<Expr>, Id, Vec<(core::AltCon, Vec<Id>, Expr)>),
    Join(Id, Vec<Id>, Box<Expr>, Box<Expr>),
    Jump(Id, Vec<Expr>),
    Fail(Span),
}
#[derive(Clone, Debug)]
/// Ordered globals and runtime constructor/location metadata.
pub struct Program {
    pub globals: Vec<(Id, Expr)>,
    pub metadata: core::Program,
}
/// Postorder erasure uses an explicit worklist, including long constructor spines.
fn expr(root: &core::Expr) -> Expr {
    use core::Expr as C;
    let mut todo = vec![(root, false)];
    let mut results: Vec<Expr> = vec![];
    while let Some((e, done)) = todo.pop() {
        let children: Vec<&core::Expr> = match e {
            C::Lam(_, e) | C::TyLam(_, e) | C::TyApp(e, _) => vec![e],
            C::App(f, a) => vec![f, a],
            C::Let(g, b) => g
                .binds
                .iter()
                .map(|b| b.rhs.as_ref())
                .chain(std::iter::once(b.as_ref()))
                .collect(),
            C::Con(_, _, es) | C::Prim(_, _, es, _) | C::Jump(_, es, _) => {
                es.iter().collect()
            }
            C::Case(e, _, _, alts) => std::iter::once(e.as_ref())
                .chain(alts.iter().map(|a| &a.rhs))
                .collect(),
            C::Join(_, _, b, r) => vec![b, r],
            C::Match(_) => panic!("match compilation precedes erasure"),
            _ => vec![],
        };
        if !done {
            todo.push((e, true));
            todo.extend(children.into_iter().rev().map(|c| (c, false)));
            continue;
        }
        let start = results.len() - children.len();
        let mut parts = results.split_off(start).into_iter();

        let result = match e {
            C::Var(i) => Expr::Var(i.name.clone()),
            C::Global(i) => Expr::Global(i.name.clone()),
            C::Lit(l) => Expr::Lit(l.clone()),
            C::TyLam(..) | C::TyApp(..) => parts.next().unwrap(),
            C::Lam(i, _) => {
                Expr::Lam(i.name.clone(), Box::new(parts.next().unwrap()))
            }
            C::App(..) => Expr::App(
                Box::new(parts.next().unwrap()),
                Box::new(parts.next().unwrap()),
            ),
            C::Let(g, _) => {
                let bs = g
                    .binds
                    .iter()
                    .map(|b| (b.name.name.clone(), parts.next().unwrap()))
                    .collect();
                Expr::Let(g.recursive, bs, Box::new(parts.next().unwrap()))
            }
            C::Con(c, _, _) => Expr::Con(c.clone(), parts.collect()),
            C::Prim(p, _, _, s) => Expr::Prim(*p, parts.collect(), *s),
            C::Case(_, i, _, alts) => {
                let e = parts.next().unwrap();
                let alts = alts
                    .iter()
                    .map(|a| {
                        (
                            a.con.clone(),
                            a.binders
                                .iter()
                                .map(|i| i.name.clone())
                                .collect(),
                            parts.next().unwrap(),
                        )
                    })
                    .collect();
                Expr::Case(Box::new(e), i.name.clone(), alts)
            }
            C::Join(j, ps, _, _) => Expr::Join(
                j.clone(),
                ps.iter().map(|i| i.name.clone()).collect(),
                Box::new(parts.next().unwrap()),
                Box::new(parts.next().unwrap()),
            ),
            C::Jump(j, _, _) => Expr::Jump(j.clone(), parts.collect()),
            C::PatternFail(s, _) => Expr::Fail(*s),
            C::Match(_) => {
                unreachable!("match compilation precedes erasure")
            }
        };
        results.push(result);
    }
    results.pop().unwrap()
}
/// Compact syntax uses an explicit print stack and bounded indentation. Debug's
/// indentation grows with depth and makes even a linear tree quadratic in bytes.
impl std::fmt::Display for Expr {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        enum Work<'a> {
            Expr(&'a Expr),
            Text(String),
        }
        let mut todo = vec![Work::Expr(self)];
        while let Some(work) = todo.pop() {
            match work {
                Work::Text(s) => write!(f, "{s}")?,
                Work::Expr(e) => {
                    let mut parts = vec![];
                    match e {
                        Expr::Var(v) => write!(f, "{v}")?,
                        Expr::Global(v) => write!(f, "@{v}")?,
                        Expr::Lit(l) => write!(f, "{l}")?,
                        Expr::Lam(v, b) => {
                            write!(f, "(lambda {v}. ")?;
                            parts.push(Work::Expr(b));
                            parts.push(Work::Text(")".into()));
                        }
                        Expr::App(a, b) => {
                            write!(f, "(")?;
                            parts.extend([
                                Work::Expr(a),
                                Work::Text(" ".into()),
                                Work::Expr(b),
                                Work::Text(")".into()),
                            ]);
                        }
                        Expr::Con(c, es) => {
                            write!(f, "({}", c.name)?;
                            for e in es {
                                parts.push(Work::Text(" ".into()));
                                parts.push(Work::Expr(e));
                            }
                            parts.push(Work::Text(")".into()));
                        }
                        Expr::Prim(p, es, _) => {
                            write!(f, "({}", p.text())?;
                            for e in es {
                                parts.push(Work::Text(" ".into()));
                                parts.push(Work::Expr(e));
                            }
                            parts.push(Work::Text(")".into()));
                        }
                        Expr::Jump(j, es) => {
                            write!(f, "(jump {j}")?;
                            for e in es {
                                parts.push(Work::Text(" ".into()));
                                parts.push(Work::Expr(e));
                            }
                            parts.push(Work::Text(")".into()));
                        }
                        Expr::Let(rec, bs, b) => {
                            write!(
                                f,
                                "(let{} ",
                                if *rec { "rec" } else { "" }
                            )?;
                            for (v, e) in bs {
                                parts.push(Work::Text(format!("{v} = ")));
                                parts.push(Work::Expr(e));
                                parts.push(Work::Text(";\n".into()));
                            }
                            parts.extend([
                                Work::Text("in ".into()),
                                Work::Expr(b),
                                Work::Text(")".into()),
                            ]);
                        }
                        Expr::Case(e, v, alts) => {
                            write!(f, "(case ")?;
                            parts.extend([
                                Work::Expr(e),
                                Work::Text(format!(" as {v} {{\n")),
                            ]);
                            for (c, ps, e) in alts {
                                let c = match c {
                                    core::AltCon::Con(c) => c.name.clone(),
                                    core::AltCon::Lit(l) => l.to_string(),
                                    core::AltCon::Default => "_".into(),
                                };
                                parts.push(Work::Text(c));
                                for p in ps {
                                    parts.push(Work::Text(format!(" {p}")));
                                }
                                parts.extend([
                                    Work::Text(" -> ".into()),
                                    Work::Expr(e),
                                    Work::Text(";\n".into()),
                                ]);
                            }
                            parts.push(Work::Text("})".into()));
                        }
                        Expr::Join(j, ps, b, r) => {
                            write!(f, "(join {j}")?;
                            for p in ps {
                                write!(f, " {p}")?;
                            }
                            write!(f, " = ")?;
                            parts.extend([
                                Work::Expr(b),
                                Work::Text("\nin ".into()),
                                Work::Expr(r),
                                Work::Text(")".into()),
                            ]);
                        }
                        Expr::Fail(s) => write!(f, "fail {s:?}")?,
                    }
                    todo.extend(parts.into_iter().rev());
                }
            }
        }
        Ok(())
    }
}
/// Destroy an owned erased tree without recursively following Box edges.
pub fn discard(root: Expr) {
    let mut todo = vec![root];
    while let Some(e) = todo.pop() {
        match e {
            Expr::Lam(_, b) => todo.push(*b),
            Expr::App(a, b) | Expr::Join(_, _, a, b) => {
                todo.push(*a);
                todo.push(*b);
            }
            Expr::Let(_, bs, b) => {
                todo.push(*b);
                todo.extend(bs.into_iter().map(|(_, e)| e));
            }
            Expr::Con(_, es) | Expr::Prim(_, es, _) | Expr::Jump(_, es) => {
                todo.extend(es)
            }
            Expr::Case(e, _, alts) => {
                todo.push(*e);
                todo.extend(alts.into_iter().map(|(_, _, e)| e));
            }
            _ => {}
        }
    }
}
/// Erase executable types only; read-only metadata supports diagnostics and printers.
pub fn erase(mut program: core::Program) -> Program {
    let globals = program
        .groups
        .iter()
        .flat_map(|g| &g.binds)
        .map(|b| (b.name.name.clone(), expr(&b.rhs)))
        .collect();
    // Consuming Core must not recursively destroy its nested expressions.
    let mut todo = program
        .groups
        .drain(..)
        .flat_map(|g| g.binds.into_iter().map(|b| *b.rhs))
        .collect::<Vec<_>>();
    while let Some(e) = todo.pop() {
        use core::Expr as C;
        match e {
            C::Lam(_, b) | C::TyLam(_, b) | C::TyApp(b, _) => todo.push(*b),
            C::App(a, b) | C::Join(_, _, a, b) => {
                todo.push(*a);
                todo.push(*b);
            }
            C::Let(g, b) => {
                todo.push(*b);
                todo.extend(g.binds.into_iter().map(|b| *b.rhs));
            }
            C::Con(_, _, es) | C::Prim(_, _, es, _) | C::Jump(_, es, _) => {
                todo.extend(es)
            }
            C::Case(e, _, _, alts) => {
                todo.push(*e);
                todo.extend(alts.into_iter().map(|a| a.rhs));
            }
            C::Match(_) => {
                unreachable!("match compilation precedes erasure")
            }
            _ => {}
        }
    }
    Program {
        globals,
        metadata: program,
    }
}
}

The ANF Grammar

Here is the control language in symbolic form. We use $a$ for an atom, $r$ for a right-hand side, and $e$ for a complete ANF body. Each row corresponds to a Rust variant below.

$$\begin{array}{rlrl}e& =\text{let}x=r\text{in}e& & \text{strict binding}\\ & \mid \text{letrec}\{\overline{x=\lambda \overline{y}.e_1}\}\text{in}{e}_2& & \text{recursive functions}\\ & \mid \text{join}j(\overline{x})=e_1\text{in}{e}_2& & \text{local continuation}\\ & \mid \text{jump}j(\overline{a})& & \text{jump to a join}\\ & \mid \text{case}a\text{of}\{\overline{q\overline{x}\to e}\}& & \text{branch on an atom}\\ & \mid \text{return}a& & \text{return a value}\\ & \mid \text{tailcall}a(\overline{a})& & \text{replace this activation}\\ & \mid {\text{fail}}_s& & \text{pattern failure at span }s\end{array}$$

An overbar means a sequence. The name $j$ identifies a join point, while $q$ is an alternative’s constructor tag, literal, or default marker. Constructor alternatives bind their fields to $\overline{x}$. Literal and default alternatives have no field binders.

The smaller pieces explain the “normal form” part of the name. An operand is always an atom, never another call waiting to happen.

$$\begin{array}{rlrl}a& =x& & \text{local variable}\\ & \mid g& & \text{global reference}\\ & \mid \ell & & \text{literal}\\ r& =a& & \text{atom}\\ & \mid a(\overline{a})& & \text{function call}\\ & \mid K(\overline{a})& & \text{constructor}\\ & \mid p(\overline{a})& & \text{primitive operation}\\ & \mid \lambda \overline{x}.e& & \text{function value}\\ & \mid \text{field}ai& & \text{field at index }i\end{array}$$

Here $K$ names a constructor and $p$ a primitive. Primitive source spans are omitted from the grammar. Unlike Core’s lambdas, these lambdas can take several parameters, and there are no type abstractions or type applications left.

The distinction between a call and a tail call is now visible in the syntax. $\mathsf{let}x=f(a)\mathsf{in}e$ saves work to do after the call. $\mathsf{tailcall}f(a)$ has no such body. A jump also has no following body, but stays inside the current function and transfers to a local join point.

The ANF control language separates ordinary bindings, recursive closures, branches, joins, and terminal transfers. Fail preserves the source span of a pattern failure:

#![allow(unused)]
fn main() {
use crate::{
    ast::Op,
    core::{self, AltCon, Lit},
    data::ConId,
    erase,
    names::Id,
    session::Session,
    source::Span,
};
use std::{collections::BTreeMap, rc::Rc};
/// An erased binder keeps its unique identity and diagnostic spelling.
pub type Var = Id;
/// Syntax is immutable and shared between closures and machine states.
pub type Body = Rc<Anf>;
#[derive(Clone, Debug, PartialEq, Eq)]
/// Atoms cannot perform work or fail when read from a well-scoped environment.
pub enum Atom {
    Var(Var),
    Global(Id),
    Lit(Lit),
}
#[derive(Clone, Debug)]
/// Lambda parameters are merged only across syntactically adjacent lambdas.
pub struct Lambda {
    pub params: Vec<Var>,
    pub body: Body,
}
#[derive(Clone, Debug)]
/// One strict computation whose operands have already been evaluated.
pub enum Rhs {
    Atom(Atom),
    Call(Atom, Vec<Atom>),
    Con(ConId, Vec<Atom>),
    Prim(Op, Vec<Atom>, Span),
    Lambda(Lambda),
    Field(Atom, u32),
}
#[derive(Clone, Debug)]
/// Global initialization order is preserved from typed Core.
pub struct Program {
    pub globals: Vec<(Id, Body)>,
    pub metadata: core::Program,
}
#[derive(Clone)]
enum Context {
    Return,
    Jump(Id),
    Bind(Var, Body),
}
struct Convert<'a> {
    sess: &'a mut Session,
    arities: BTreeMap<Id, usize>,
}
fn arity(mut e: &erase::Expr) -> usize {
    let mut n = 0;
    while let erase::Expr::Lam(_, b) = e {
        n += 1;
        e = b;
    }
    n
}
fn collect(e: &erase::Expr, out: &mut BTreeMap<Id, usize>) {
    use erase::Expr as E;
    let mut todo = vec![e];
    while let Some(e) = todo.pop() {
        match e {
            E::Let(_, bs, b) => {
                for (v, e) in bs {
                    let n = arity(e);
                    if n > 0 {
                        out.insert(v.clone(), n);
                    }
                    todo.push(e);
                }
                todo.push(b);
            }
            E::Lam(_, b) => todo.push(b),
            E::App(a, b) | E::Join(_, _, a, b) => {
                todo.push(a);
                todo.push(b);
            }
            E::Con(_, es) | E::Prim(_, es, _) | E::Jump(_, es) => {
                todo.extend(es)
            }
            E::Case(e, _, alts) => {
                todo.push(e);
                todo.extend(alts.iter().map(|(_, _, e)| e));
            }
            _ => {}
        }
    }
}
impl Convert<'_> {
    fn fresh(&mut self) -> Var {
        self.sess.fresh_id("$a")
    }
    fn finish(&mut self, a: Atom, k: Context) -> Body {
        Rc::new(match k {
            Context::Return => Anf::Ret(a),
            Context::Jump(j) => Anf::Jump(j, vec![a]),
            Context::Bind(v, b) => Anf::Let(v, Rhs::Atom(a), b),
        })
    }
    fn rhs(&mut self, r: Rhs, k: Context) -> Body {
        if let Context::Bind(v, b) = k {
            return Rc::new(Anf::Let(v, r, b));
        }
        if let (Rhs::Call(f, args), Context::Return) = (&r, &k) {
            return Rc::new(Anf::TailCall(f.clone(), args.clone()));
        }
        let v = self.fresh();
        let rest = self.finish(Atom::Var(v.clone()), k);
        Rc::new(Anf::Let(v, r, rest))
    }
    /// Tasks hold pending compiler work. Neither expression depth nor the
    /// number of operands adds a Rust call frame.
    fn expr(&mut self, e: erase::Expr, k: Context) -> Body {
        use erase::Expr as E;
        enum Work {
            Expr(erase::Expr, Context),
            Bindings(Vec<(Var, erase::Expr)>),
            Lambda(Vec<Var>, Context),
            Rec(Vec<(Var, Vec<Var>)>),
            Case(
                erase::Expr,
                Var,
                Vec<(AltCon, Vec<Var>)>,
                Option<(Id, Var, Body)>,
            ),
            Join(Id, Vec<Var>, Option<(Id, Var, Body)>),
            Call(erase::Expr, Var, Vec<erase::Expr>, Var),
        }
        fn peel(mut e: erase::Expr) -> (Vec<Var>, erase::Expr) {
            let mut ps = vec![];
            while let E::Lam(v, b) = e {
                ps.push(v);
                e = *b;
            }
            (ps, e)
        }
        fn branch(
            k: Context,
            sess: &mut Session,
        ) -> (Context, Option<(Id, Var, Body)>) {
            match k {
                Context::Bind(v, b) => {
                    let j = sess.fresh_id("$cont");
                    (Context::Jump(j.clone()), Some((j, v, b)))
                }
                k => (k, None),
            }
        }
        fn wrap(body: Body, cont: Option<(Id, Var, Body)>) -> Body {
            match cont {
                Some((j, v, b)) => Rc::new(Anf::Join(j, vec![v], b, body)),
                None => body,
            }
        }
        let mut todo = vec![Work::Expr(e, k)];
        let mut results: Vec<Body> = vec![];
        while let Some(work) = todo.pop() {
            match work {
                Work::Bindings(mut bs) => {
                    if let Some((v, e)) = bs.pop() {
                        let b = results.pop().unwrap();
                        todo.push(Work::Bindings(bs));
                        todo.push(Work::Expr(e, Context::Bind(v, b)));
                    }
                }
                Work::Lambda(params, k) => {
                    let body = results.pop().unwrap();
                    results.push(
                        self.rhs(Rhs::Lambda(Lambda { params, body }), k),
                    );
                }
                Work::Rec(bs) => {
                    let bodies =
                        results.split_off(results.len() - bs.len());
                    let rest = results.pop().unwrap();
                    let bs = bs
                        .into_iter()
                        .zip(bodies)
                        .map(|((v, params), body)| {
                            (v, Lambda { params, body })
                        })
                        .collect();
                    results.push(Rc::new(Anf::LetRec(bs, rest)));
                }
                Work::Case(e, v, heads, cont) => {
                    let bodies =
                        results.split_off(results.len() - heads.len());
                    let alts = heads
                        .into_iter()
                        .zip(bodies)
                        .map(|((c, ps), b)| (c, ps, b))
                        .collect();
                    let b = wrap(
                        Rc::new(Anf::Case(Atom::Var(v.clone()), alts)),
                        cont,
                    );
                    todo.push(Work::Expr(e, Context::Bind(v, b)));
                }
                Work::Join(j, ps, cont) => {
                    let rest = results.pop().unwrap();
                    let body = results.pop().unwrap();
                    results.push(wrap(
                        Rc::new(Anf::Join(j, ps, body, rest)),
                        cont,
                    ));
                }
                Work::Call(head, f, args, result) => {
                    let rest = results.pop().unwrap();
                    let vars: Vec<_> =
                        args.iter().map(|_| self.fresh()).collect();
                    let atoms =
                        vars.iter().cloned().map(Atom::Var).collect();
                    let b = self.rhs(
                        Rhs::Call(Atom::Var(f.clone()), atoms),
                        Context::Bind(result, rest),
                    );
                    let bs = std::iter::once((f, head))
                        .chain(vars.into_iter().zip(args))
                        .collect();
                    results.push(b);
                    todo.push(Work::Bindings(bs));
                }
                Work::Expr(e, k) => {
                    match e {
                        E::Var(v) => {
                            results.push(self.finish(Atom::Var(v), k))
                        }
                        E::Global(v) => {
                            results.push(self.finish(Atom::Global(v), k))
                        }
                        E::Lit(l) => {
                            results.push(self.finish(Atom::Lit(l), k))
                        }
                        node @ E::Lam(..) => {
                            let (ps, body) = peel(node);
                            todo.push(Work::Lambda(ps, k));
                            todo.push(Work::Expr(body, Context::Return));
                        }
                        node @ E::App(..) => {
                            let mut head = node;
                            let mut args = vec![];

                            while let E::App(f, a) = head {
                                args.push(*a);
                                head = *f;
                            }
                            args.reverse();

                            let known = match &head {
                                E::Var(v) | E::Global(v) => {
                                    self.arities.get(v).copied()
                                }
                                E::Lam(..) => Some(arity(&head)),
                                _ => None,
                            };
                            // Unknown calls execute before evaluating their next argument.
                            let n = known.unwrap_or(1).min(args.len());
                            let extra = args.split_off(n);

                            let f = self.fresh();
                            if extra.is_empty() {
                                let vars: Vec<_> = args
                                    .iter()
                                    .map(|_| self.fresh())
                                    .collect();
                                let atoms = vars
                                    .iter()
                                    .cloned()
                                    .map(Atom::Var)
                                    .collect();
                                results.push(self.rhs(
                                    Rhs::Call(Atom::Var(f.clone()), atoms),
                                    k,
                                ));
                                todo.push(Work::Bindings(
                                    std::iter::once((f, head))
                                        .chain(vars.into_iter().zip(args))
                                        .collect(),
                                ));
                            } else {
                                let result = self.fresh();
                                let application = extra.into_iter().fold(
                                    E::Var(result.clone()),
                                    |f, a| E::App(Box::new(f), Box::new(a)),
                                );
                                todo.push(Work::Call(
                                    head, f, args, result,
                                ));
                                todo.push(Work::Expr(application, k));
                            }
                        }
                        E::Let(rec, bs, b) => {
                            if rec {
                                let (heads, bodies): (Vec<_>, Vec<_>) = bs
                                    .into_iter()
                                    .map(|(v, e)| {
                                        let (ps, e) = peel(e);
                                        ((v, ps), e)
                                    })
                                    .unzip();
                                todo.push(Work::Rec(heads));
                                todo.extend(bodies.into_iter().rev().map(
                                    |e| Work::Expr(e, Context::Return),
                                ));
                            } else {
                                todo.push(Work::Bindings(bs));
                            }
                            todo.push(Work::Expr(*b, k));
                        }
                        node @ (E::Con(..) | E::Prim(..) | E::Jump(..)) => {
                            let args = match &node {
                                E::Con(_, es)
                                | E::Prim(_, es, _)
                                | E::Jump(_, es) => es,
                                _ => unreachable!(),
                            };
                            let vars: Vec<_> =
                                args.iter().map(|_| self.fresh()).collect();
                            let atoms = vars
                                .iter()
                                .cloned()
                                .map(Atom::Var)
                                .collect();
                            let (args, body) = match node {
                                E::Con(c, es) => {
                                    (es, self.rhs(Rhs::Con(c, atoms), k))
                                }
                                E::Prim(p, es, s) => (
                                    es,
                                    self.rhs(Rhs::Prim(p, atoms, s), k),
                                ),
                                E::Jump(j, es) => {
                                    (es, Rc::new(Anf::Jump(j, atoms)))
                                }
                                _ => unreachable!(),
                            };
                            results.push(body);
                            todo.push(Work::Bindings(
                                vars.into_iter().zip(args).collect(),
                            ));
                        }
                        E::Case(e, v, alts) => {
                            let (k, cont) = branch(k, self.sess);
                            let (heads, bodies): (Vec<_>, Vec<_>) = alts
                                .into_iter()
                                .map(|(c, ps, b)| ((c, ps), b))
                                .unzip();
                            todo.push(Work::Case(*e, v, heads, cont));
                            todo.extend(
                                bodies
                                    .into_iter()
                                    .rev()
                                    .map(|e| Work::Expr(e, k.clone())),
                            );
                        }
                        E::Join(j, ps, b, r) => {
                            let (k, cont) = branch(k, self.sess);
                            todo.push(Work::Join(j, ps, cont));
                            todo.push(Work::Expr(*r, k.clone()));
                            todo.push(Work::Expr(*b, k));
                        }
                        E::Fail(s) => results.push(Rc::new(Anf::Fail(s))),
                    }
                }
            }
        }
        assert_eq!(results.len(), 1);
        results.pop().unwrap()
    }
}
/// Normalize left-to-right, sharing every non-tail continuation exactly once.
pub fn convert(sess: &mut Session, program: erase::Program) -> Program {
    let mut arities = BTreeMap::new();
    for (v, e) in &program.globals {
        if arity(e) > 0 {
            arities.insert(v.clone(), arity(e));
        }
        collect(e, &mut arities);
    }
    let mut c = Convert { sess, arities };
    let globals = program
        .globals
        .into_iter()
        .map(|(v, e)| (v, c.expr(e, Context::Return)))
        .collect();
    Program {
        globals,
        metadata: program.metadata,
    }
}
impl std::fmt::Display for Atom {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Var(v) => write!(f, "{v}"),
            Self::Global(v) => write!(f, "@{v}"),
            Self::Lit(l) => write!(f, "{l}"),
        }
    }
}
fn list<T: std::fmt::Display>(items: &[T]) -> String {
    items
        .iter()
        .map(ToString::to_string)
        .collect::<Vec<_>>()
        .join(", ")
}
impl std::fmt::Display for Rhs {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Atom(a) => write!(f, "{a}"),
            Self::Call(a, args) => write!(f, "call {a}({})", list(args)),
            Self::Con(c, args) => write!(f, "{}({})", c.name, list(args)),
            Self::Prim(p, args, _) => {
                write!(f, "{}({})", p.text(), list(args))
            }
            Self::Lambda(l) => {
                write!(f, "lambda ({}) {{ {} }}", list(&l.params), l.body)
            }
            Self::Field(a, i) => write!(f, "field {a}[{i}]"),
        }
    }
}
impl std::fmt::Display for Anf {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        enum Work<'a> {
            Body(&'a Anf),
            Rhs(&'a Rhs),
            Text(String),
        }
        let mut todo = vec![Work::Body(self)];
        while let Some(work) = todo.pop() {
            let mut parts = vec![];
            match work {
                Work::Text(s) => write!(f, "{s}")?,
                Work::Rhs(Rhs::Lambda(l)) => {
                    write!(f, "lambda ({}) {{ ", list(&l.params))?;
                    parts.extend([
                        Work::Body(&l.body),
                        Work::Text(" }".into()),
                    ]);
                }
                Work::Rhs(r) => write!(f, "{r}")?,
                Work::Body(b) => match b {
                    Self::Let(v, r, b) => {
                        write!(f, "let {v} = ")?;
                        parts.extend([
                            Work::Rhs(r),
                            Work::Text(";\n".into()),
                            Work::Body(b),
                        ]);
                    }
                    Self::LetRec(bs, b) => {
                        for (v, l) in bs {
                            parts.extend([
                                Work::Text(format!(
                                    "rec {v}({}) = {{ ",
                                    list(&l.params)
                                )),
                                Work::Body(&l.body),
                                Work::Text(" }\n".into()),
                            ]);
                        }
                        parts.push(Work::Body(b));
                    }
                    Self::Join(j, ps, b, r) => {
                        write!(f, "join {j}({}) = {{ ", list(ps))?;
                        parts.extend([
                            Work::Body(b),
                            Work::Text(" };\n".into()),
                            Work::Body(r),
                        ]);
                    }
                    Self::Jump(j, args) => {
                        write!(f, "jump {j}({})", list(args))?
                    }
                    Self::Case(a, alts) => {
                        writeln!(f, "case {a} {{")?;
                        for (c, ps, b) in alts {
                            let head = match c {
                                AltCon::Con(c) => c.name.clone(),
                                AltCon::Lit(l) => l.to_string(),
                                AltCon::Default => "_".into(),
                            };
                            parts.extend([
                                Work::Text(format!(
                                    "{head}({}) -> {{ ",
                                    list(ps)
                                )),
                                Work::Body(b),
                                Work::Text(" }\n".into()),
                            ]);
                        }
                        parts.push(Work::Text("}".into()));
                    }
                    Self::Ret(a) => write!(f, "return {a}")?,
                    Self::TailCall(fun, args) => {
                        write!(f, "tail {fun}({})", list(args))?
                    }
                    Self::Fail(s) => write!(f, "fail {s:?}")?,
                },
            }
            todo.extend(parts.into_iter().rev());
        }
        Ok(())
    }
}
/// Drain child edges explicitly when the last owner releases a deep ANF tree.
impl Drop for Anf {
    fn drop(&mut self) {
        fn edges(node: &mut Anf, todo: &mut Vec<Body>) {
            fn take(b: &mut Body) -> Body {
                std::mem::replace(
                    b,
                    Rc::new(Anf::Ret(Atom::Lit(Lit::Int(0)))),
                )
            }
            match node {
                Anf::Let(_, r, b) => {
                    todo.push(take(b));
                    if let Rhs::Lambda(l) = r {
                        todo.push(take(&mut l.body));
                    }
                }
                Anf::LetRec(bs, b) => {
                    todo.push(take(b));
                    todo.extend(bs.drain(..).map(|(_, l)| l.body));
                }
                Anf::Join(_, _, b, r) => {
                    todo.push(take(b));
                    todo.push(take(r));
                }
                Anf::Case(_, alts) => {
                    todo.extend(alts.drain(..).map(|(_, _, b)| b))
                }
                _ => {}
            }
        }
        let mut todo = vec![];
        edges(self, &mut todo);
        while let Some(b) = todo.pop() {
            if let Ok(mut node) = Rc::try_unwrap(b) {
                edges(&mut node, &mut todo);
                // Empty this node before Drop runs again on the local variable.
                // Its remaining children are only leaf placeholders.
            }
        }
    }
}
#[derive(Clone, Debug)]
/// Jumps transfer within a function; tail calls replace its activation.
pub enum Anf {
    Let(Var, Rhs, Body),
    LetRec(Vec<(Var, Lambda)>, Body),
    Join(Id, Vec<Var>, Body, Body),
    Jump(Id, Vec<Atom>),
    Case(Atom, Vec<(AltCon, Vec<Var>, Body)>),
    Ret(Atom),
    TailCall(Atom, Vec<Atom>),
    Fail(Span),
}
}