Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Chapter 17: Capstone — Running Every Feature at Once and Watching What Composes

Sixteen chapters ago, we counted the lines in a Lua file and checked whether it contained the word "print". That was it — one string lookup, one Salsa query. Now we have a type checker. It handles unions, generics, classes, cross-file dependencies, narrowing, and environment merging. It catches real type errors. It re-checks incrementally when you edit a file.

This chapter doesn’t introduce new features. Instead, it runs all of them together and watches what happens when they interact. A type checker is more than its features — it’s the way they compose. Narrowing without merging is useless (the narrowed type is thrown away). Merging without narrowing is incomplete (you need narrowing to make unions tractable). Cross-file without annotations is blind (you get Dynamic everywhere). The features only work as a system.

Let’s see that system in action.

The Program

The capstone code in chapters/ch17-capstone/ is a single main.rs that combines everything from Chapters 1–16. There’s no new logic — every function and type is one you’ve seen before. What’s new is that they’re all present at once, and they call each other.

Here’s the dependency graph of the major components:

SourceFile (input)
  ├─→ parse (tracked) → LuaAst
  └─→ extract_annotations (tracked) → Vec<Annotation>
        └─→ type_check (tracked) → Vec<Diagnostic>
              │     depends on both parse and extract_annotations
              ├─→ check_stmt → TypeEnv
              │     ├─→ infer_type → Type
              │     ├─→ extract_narrowings → (then, else)
              │     └─ TypeEnv::merge
              └─→ module_exports (tracked) → Type
                    └─→ resolve_require → SourceFile

Every arrow is a Salsa-tracked query or a function called from one. The data flows down; the invalidation flows up. When you change a SourceFile’s text, Salsa re-runs parse, then extract_annotations, then everything that depends on them — but only if the outputs actually changed.

Demo 1: Full Type Checking

Here’s a Lua file that uses classes, union types, and narrowing in the same program:

---@class Point
---@field x number
---@field y number

---@param a Point
---@param b Point
---@return Point
function add_points(a, b)
    return a
end

---@type number|string
local x = 42

if type(x) == "number" then
    local y = x + 1       -- OK: x is narrowed to Number
else
    local z = x .. "!"    -- OK: x is narrowed to String
end

---@type number|nil
local maybe_num = 42

if maybe_num ~= nil then
    local safe = maybe_num + 1  -- OK: nil excluded
end

Zero diagnostics. Every feature is doing its job:

  • ---@class Point registers a table type with x: Number and y: Number (Ch11)
  • ---@param a Point annotates the function’s parameter types (Ch10)
  • ---@type number|string declares a union type (Ch11)
  • type(x) == "number" narrows x to Number in the then-block (Ch15)
  • After the if, the narrowing reverts — x goes back to Number | String (Ch16)
  • maybe_num ~= nil excludes Nil from the union (Ch15)

None of these features work in isolation. The narrowing is only useful because the union type exists. The union type is only useful because is_compatible_with handles it. The class annotation is only useful because check_stmt looks up parameter types. The features are layers, and each layer depends on the ones below.

Demo 2: Cross-File Type Checking

Two files: a utility module and a main program that requires it.

utils.lua:

---@param x number
---@return number
function double(x)
    return x
end

return double

main.lua:

local double = require("utils")
local result = double(42)

When we type-check main.lua, the checker calls require("utils"), which triggers module_exports on utils.lua. That query parses utils.lua, infers that double has type Function(Number) -> Number, and returns it as the module’s export type. Back in main.lua, double(42) is a function call with a Number argument against a Function(Number) -> Number — it type-checks cleanly.

The cross-file dependency is tracked by Salsa. If you edit utils.lua and change double to return a string, module_exports re-runs, type_check on main.lua re-runs, and you get a diagnostic: “cannot use String in arithmetic.” Salsa figured out that main.lua depends on utils.lua because resolve_require called module_exports — the dependency is implicit in the query graph, not something you have to declare.

Demo 3: Language Server with Timing

The language server from Chapter 7, now with std::time::Instant measurements. The demo generates a ~1200-line Lua file (200 typed functions plus a narrowing section) to make the timing visible:

#![allow(unused)]
fn main() {
use salsa::Setter;
use std::path::PathBuf;
use std::time::{Duration, Instant};

struct LanguageServer {
    db: Database,
    files: Vec<(PathBuf, SourceFile)>,  // path → SourceFile for this server's db
}

impl LanguageServer {
    fn open_file(&mut self, path: &str, text: &str) -> (Vec<Diagnostic>, Duration) {
        let start = Instant::now();
        let source = SourceFile::new(&self.db, PathBuf::from(path), text.to_string());
        self.files.push((PathBuf::from(path), source));
        let diagnostics = type_check(&self.db, source);
        (diagnostics, start.elapsed())
    }

    fn edit_file(&mut self, path: &str, new_text: &str) -> (Vec<Diagnostic>, Duration) {
        if let Some((_, source)) = self.files.iter().find(|(p, _)| p == path) {
            let start = Instant::now();
            source.set_text(&mut self.db).to(new_text.to_string());
            let diagnostics = type_check(&self.db, *source);
            (diagnostics, start.elapsed())
        } else {
            self.open_file(path, new_text)
        }
    }
}
}

Three runs on the same 1200-line file:

  1. First open (cold cache) — full parse + type check: ~22ms
  2. Edit: change a value (local result = 42local result = 99) — re-parse + re-check: ~22ms. The source text changed, so parse re-runs. The AST changed, so type_check re-runs too.
  3. Edit: add a comment (---@class Item--- A data item\n---@class Item) — re-parse only: ~1.5ms. The source text changed, so parse re-runs. But the AST is identical — comments aren’t part of the AST. Salsa’s value-based comparison detects this and skips type_check entirely.

That’s the 14x speedup (timings vary by machine; the key point is the ratio, not the absolute numbers). The comment-only edit triggers a re-parse but doesn’t propagate to type checking because Salsa compares the output, not only the revision. In a real codebase with cross-file dependencies, the difference is even more dramatic: editing file A doesn’t invalidate file B’s cached type_check.

Demo 4: Generics + Narrowing + Merging

This is where the features really start interacting. Here’s a Lua program that uses generics, narrowing, and environment merging in sequence:

---@param x T
---@return T
function identity(x)
    return x
end

---@type number|string
local val = 42

if type(val) == "number" then
    local narrowed = identity(val)
else
    local also = val .. "!"
end

Trace what happens:

  1. identity is declared with ---@param x T and ---@return T. The T becomes Type::Var("T") (Ch12).
  2. val is Number | String (Ch11).
  3. type(val) == "number" narrows val to Number in the then-block (Ch15).
  4. identity(val)val is Number, so T = Number, return type is Number. The generic substitution works on the narrowed type (Ch12).
  5. After the if, the environment merges: val goes back to Number | String (Ch16).

The generic substitution works on the narrowed type without any special handling. This isn’t an accident — it’s a consequence of the design. Narrowing produces a new TypeEnv. infer_type reads from that environment. Substitution applies to whatever type it finds. The features compose because they all operate on the same data structures, and none of them make assumptions about where those data structures came from.

Demo 5: Recursive Types + Narrowing

Recursive types (Ch14) and narrowing (Ch15) interact in a common Lua pattern — a linked list node that might be nil:

---@class Node
---@field value number
---@field next Node|nil

---@type Node|nil
local head = nil

if head ~= nil then
    local v = head
end

Node|nil is a union of Ref("Node") and Nil. The head ~= nil check removes Nil from the union, narrowing head to Ref("Node") inside the then-block. The Ref type isn’t expanded — it stays as a named reference. This is correct: Ref is a final value, not a placeholder (Ch14). The type checker doesn’t need to know what’s inside the Node to know that head isn’t nil.

Demo 6: Environment Merging

The most recent feature, and the one that makes narrowing stick. Without merging, any assignment inside an if was lost after the block ended. With merging, the post-if type is the union of all possible types across branches:

---@type number|string
local x = 42
if type(x) == "number" then
    x = "hello"
else
    x = 99
end

After the if:

  • pre_env has x: Number | String
  • then_env has x: String
  • else_env has x: Number
  • Merge: Type::union(String, Number)Number | String

The assignment changed x in each branch, but the merged type is the same as the original — because the union of the branch types equals the pre-if type. Narrowing reverts via the same mechanism: Type::union(NarrowedType, OriginalType) absorbs the narrowed variant back into the original.

What We Built

Here’s every feature, the chapter that introduced it, and what it contributes to the whole:

FeatureChapterWhy It Matters
Salsa inputs1Source of truth — everything derives from SourceFile
Tracked functions1–2Automatic caching and invalidation
Interned symbols3Cheap identity comparison for names
Tracked structs4Entity identity — FuncDef is a database-resident object
Type inference5The core query — “what type does this expression have?”
Diagnostics6Error reporting without polluting return types
Language server7The payoff — a usable tool for programmers
Cycle detection8Safety net — recursive queries can’t loop forever
Cross-file9require() resolves types across modules
Annotations10The programmer teaches the checker what they know
Union types11`number
Generics12identity(x: T): T — type-preserving abstractions
Function types13fun(number): string — higher-order function types
Recursive types14`Node
Type narrowing15type(x) == "number" — making unions tractable
Environment merging16Assignments inside branches survive the if

Seventeen chapters. Sixteen features. One system.

What’s Still Missing

This tutorial builds a teaching type checker, not a production one. A real Lua type checker (like LuaLS or Teal) has plenty that we don’t.

Type narrowing in loops — we return the post-loop-body type, which is overly optimistic. The correct post-loop type is the intersection of the pre-loop and post-loop-body types, because the loop might not have run at all.

Full method desugaring — method calls (a:f()) are silently dropped. They’d need to desugar to a.f(a, ...) with the subject as an implicit first argument.

Table expression types — we have Type::Table for class instances but no way to construct a table literal. A real checker would infer { x = 1, y = 2 } as Table { x: Number, y: Number }.

Multiple return values — Lua functions can return multiple values and we only track the first.

Variadic arguments — Lua functions can take ... arguments and we don’t model variadic generics.

Live registry updates — our OnceLock registry is write-once. A real language server would watch the filesystem and update the registry on file changes, through the database, not a side channel.

Bidirectional type checking — we only check top-down (from annotations to expressions). A production checker also works bottom-up, inferring types from usage when annotations are absent.

Type aliasing---@alias Vec2 {x: number, y: number} style named shorthands for complex types aren’t supported.

Each of these is a real feature, not a hypothetical. If you’re building a type checker for production use, you’ll need most of them. The good news: the architecture you’ve learned — Salsa inputs, tracked queries, derived types, accumulators, narrowing, merging — scales to all of them. The hard part isn’t the Salsa plumbing. It’s the type-system semantics.