The Warp Book

Preface

How to read this book

This book teaches Warp: a small dependently typed language whose entire purpose is to enumerate or sample the inhabitants of any type, in order of simplicity. It assumes you are a programmer. It does not assume you know what a dependent type, an eliminator, a universe, or a motive is — every one of those words gets built up from things you already know, and every concept is demonstrated with a real run of the actual tool. No output in this book is invented; everything after a $ was produced by generate.py from the Warp repository.

Warp is implemented in about two thousand lines of dependency-free Python across four files: kernel.py (the type theory), prelude.py (the standard library — which, as you'll see, is shockingly small because almost nothing is built in), generate.py (the enumerator and sampler), and tests.py. Where a concept lives in the code, the book says so in a note like this: kernel.py · check(). You are encouraged to read along in the source; none of it is long.

The name. On a loom, the warp is the set of threads held in tension, through which the weft is woven. Warp is the successor to a language called Weft, and the metaphor is honest: the type system holds the space of programs in tension, and the generator passes through it, row by row, weaving out every cloth the threads permit. That image — every possible cloth, in order of simplicity — is the whole book in one sentence.

Interludes marked Try it are commands to run yourself. Quizzes are answered by clicking; predictions made before revealing are worth ten explanations. Exercises come with hidden solutions. Part I says why the language exists. Part II builds the type theory from simply typed functions upward. Part III explains the simplicity prior. Part IV is the payoff: the enumerator, the proof search, the sampler, the trick that turns the entire language into a single enumerable dataset — and the loom run in reverse, where programs are built first and their types read off.

Part I · The Idea · Chapter 1

Every type is a dataset

A type is a description of data. If the description is precise enough, you can turn the crank and generate the data.

Suppose you want a stream of small, total, correct programs — say, to train a model, to test a compiler, to seed a search. You could scrape them, but scraped programs come without guarantees and without labels. Or you could generate them: write down a description of the programs you want and enumerate everything that matches, simplest first.

Every programmer already owns a language of such descriptions: types. The type Nat -> Nat describes "functions from naturals to naturals". In most languages that description is loose — a Java Function<Integer,Integer> might loop forever, throw, or read the disk. But in a total language, where every program terminates and has no effects, the type describes exactly a set of mathematical functions, and each program of that type is a certified, labeled data point.

Warp is a language built so that this works for every type, with three commitments:

1. Types can say anything worth saying. "A function from naturals to naturals" is a type. So is "a pair of a number and a proof that it equals 2". So is "for all a and b, if a = b then b = a" — and a program of that type is a proof of the theorem. So is "a type, together with a value of it". The richer the type language, the richer the datasets you can order up. Warp's type language is dependent type theory, the same family as Agda, Coq, and Lean — Part II builds it up piece by piece.

2. Every well-typed program is meaningful. Every Warp program terminates (Chapter 6 shows why this is guaranteed by construction rather than checked by an analyzer), so enumeration never wedges on an infinite loop, and every generated point can be labeled by actually running it.

3. Simplicity is measured, and generation respects it. Every term has a description length (DL): one node per syntactic construct. Enumeration is exhaustive in DL order; sampling draws from a distribution that prefers short programs — a simplicity prior in the spirit of minimum description length. Chapter 10 is about why this particular ruler, and what it takes to keep it honest (spoiler: the number 7 costs 8 nodes, on purpose).

The one-liner

Here is the entire product, in one command. Give it a type; it gives you the inhabitants, simplest first, and for observable goals it tabulates them on small inputs:

Identity and the zero function are the two 2-node programs; successor and the constant 1 are the 3-node programs; and so on, forever, without repetition or omission. Now the same machine, pointed at a theorem — "for all a, b : if a = b then b = a" — with no hints, no tactics, nothing exposed from the library:

That is the textbook proof of symmetry of equality (you will be able to read it by the end of Chapter 9), discovered by enumeration. Nothing special happened: proof search is what enumeration is called when the goal happens to be a theorem. It is slower there — which is exactly what theorem proving deserves — and fast where the goal is ordinary data. One machine, one prior, every type a dataset.

Where this is going

The deep reason Warp repays study is a single design decision applied everywhere: things you'd expect to be built in are instead data. Booleans, numbers, lists, pairs — library declarations. Equality — a library declaration (Chapter 9). Even types themselves are first-class terms, so a type is one more thing the generator can generate (Chapters 4 and 13). Push that to its limit and you get the closing act: a single goal type whose inhabitants are all well-typed programs of all types, so "enumerate the whole language, simplest first" is not a special mode but one more dataset (Chapter 14). The loom at the top of this page is that goal running.

Part I · The Idea · Chapter 2

A ten-minute tour

Run the tool, poke six goals, and collect the vocabulary the rest of the book will define properly.

Warp needs nothing but Python 3. From the repository:

python3 tests.py                    # kernel + prelude tests
python3 generate.py --goal 'Nat' --enumerate 3 --use ''

The interface is one script with two verbs. --enumerate N lists the first N inhabitants of the goal type in description-length order, exhaustively. --samples N draws N random inhabitants under the simplicity prior. The goal is written in a small s-expression surface syntax (Appendix A has the full grammar), and --use controls which library names the generator may build with — --use '' means "from scratch", and the default exposes add, mul, Nat, Bool.

Six goals, six ideas

Data. A list of booleans is a goal. The least inhabitant is the empty list; DL order then walks up by length and content:

Functions. You saw (-> Nat Nat) in Chapter 1. Functions on finite types close out quickly — here is every simplest spelling of the four functions on booleans; note the machine finds the "if" at #003 (the strange elim syntax becomes friendly in Chapter 6):

Search. A Sig goal (a dependent pair — Chapter 11's favorite) asks for a value and evidence about it. "A number n together with a proof that n = 2" has exactly one sensible least inhabitant, and the tool solves for it:

Your own types, inline. Type declarations are ordinary expressions, so a goal can introduce a datatype that never existed before and ask for functions out of it:

Types as data. The goal can be U0 — "the type of (small) types" — and then the things being generated are types themselves. Sampling mode will even invent fresh datatypes and inhabit them in the same breath:

Theorems. And the goal can be a proposition, in which case inhabitants are proofs and enumeration is proof search — including proofs that genuinely require induction (Chapter 12 walks through this output):

The vocabulary you just collected

Six words appeared that the next chapters will define with care. Goal: the type whose inhabitants you asked for. DL: description length, the node count that orders everything. lam / pi: functions and their (possibly dependent) types — Chapter 3. U0: the type of types — Chapter 4. data / con: datatype declarations and constructors — Chapter 5. elim: the single, universal case-analysis-plus-recursion construct — Chapter 6. And two you met in passing: Id, equality-as-a-type (Chapter 9), and Sig, the dependent pair (Chapters 8 and 14).

Part II · The Language · Chapter 3

Functions, from the ground up

Warp's function layer is the typed lambda calculus you already half-know, with one syntactic surprise waiting at the type of a function.

Strip Warp of datatypes and universes and what remains is the simply typed lambda calculus: the minimal language of functions. There are variables, there are anonymous functions, and there is application:

(lam (x) x)          ; the identity function
(lam (x y) x)        ; curried: a function returning a function
(f a b)              ; application, left-nested: ((f a) b)

Two conventions to absorb. First, everything is curried. A "two-argument function" is a function that returns a function; (lam (x y) e) is sugar for (lam (x) (lam (y) e)), and (f a b) applies one argument at a time. Second, lambdas carry no type annotations. You write (lam (x) x), never (lam (x : Nat) x). How the checker copes without annotations is the subject of Chapter 7; for now, note that a bare lambda doesn't have a type by itself — it is checked against one.

The type of a function is called Pi

The type of functions from A to B is written the way you'd hope:

(-> A B)         ; functions from A to B
(-> A B C)       ; sugar for (-> A (-> B C)) — curried again

But -> is itself sugar. The real construct is:

(pi (x A) B)     ; the type of functions taking x : A and returning B
                 ; — where B may mention x

Read (pi (x A) B) as "for each x of type A, a B". The novelty — the thing that makes this a dependent function type, and the hinge of the whole book — is that clause at the end: the return type may mention the argument. (-> A B) is just (pi (x A) B) where B doesn't bother to use x.

Why would a return type mention an argument's value? Here is the example from the tour, now legible: (pi (n Nat) (Fin (suc n))) is the type of functions that take a number n and return an element of Fin (suc n) — the type of numbers strictly below n + 1. The return type is computed from the argument. No simply-typed language can say this; a dependently-typed one says it with the same arrow it uses for everything else. Chapter 8 does dependency properly; until then every Pi you meet will be an honest arrow.

What the generator does at a function goal

When the goal is a Pi, the generator has exactly one move: emit a lambda and continue inside with the argument in scope. generate.py · _enum_at, 'VPi' case. This means every generated function is eta-long — fully spelled out as (lam (x) …) rather than passed point-free — and it means function goals are cheap: the interesting choices all happen at the result type. You can see the discipline in any enumeration from Chapter 2: every inhabitant of (-> Nat Nat) starts with (lam (x0) …), and the variety lives in the body.

Variables, for the record, are the other primitive production: at any goal, any in-scope variable whose type matches is a 1-node inhabitant. That's why (lam (x0) x0) is a 2-node program — one lam, one variable — and why it is always the first inhabitant of (-> A A) for any A.

python3 generate.py --goal '(-> Nat (-> Bool Nat))' --enumerate 2 --use ''

Part II · The Language · Chapter 4

Types are programs: universes

In Warp there is no separate language of types. A type is an expression you can pass around, compute, and — crucially for a data engine — generate.

In most languages the type layer and the term layer are different languages with different grammars, one erased before run time. Warp collapses the distinction: types are terms. Nat is an expression. (-> Nat Bool) is an expression. You can bind a type with a let, take one as a function argument, return one from a function.

Expressions have types — so what is the type of Nat? The answer is U0, pronounced "universe zero": the type of ordinary, small types. And because U0 is itself an expression, it too has a type: U1. Which has type U2, and so on up a ladder that never ends and never cycles:

Nat : U0        (-> Nat Bool) : U0        U0 : U1        U1 : U2 …

Why a ladder and not a loop?

The tempting shortcut is one universe with Type : Type. Warp refuses it, and the reason is not aesthetic. With Type : Type the type system becomes inconsistent: by a construction known as Girard's paradox, every type — including absurd ones — acquires an inhabitant. For a proof assistant that's embarrassing; for a data engine it is fatal in a specific, practical way. Warp's promise is that enumerating a theorem-type yields proofs, and that an empty type stays visibly empty:

Under Type : Type, that search would eventually "succeed", and every proof dataset the engine ever produced would be mislabeled. The universe ladder is what makes "this goal has no inhabitants" a meaningful, trustworthy output. The discipline is called predicativity: each universe's types are built only from universes strictly below it, with two concrete rules — U l : U (l+1), and a Pi type lives in the maximum of its domain's and codomain's universes. There is deliberately no "cumulativity" (a U0 type is not automatically a U1 type); keeping levels exact keeps the checker simple and the semantics honest. kernel.py · infer(), 'pi' case

The payoff: type goals

Because types are terms, U0 is a legitimate goal, and "generate me some types" is not a special feature — it's the same enumerator pointed one level up:

And U1 enumerates large types — note the least inhabitant:

The simplest large type is U0 itself — the ladder made visible. Hold this thought for Chapter 13, where sampling at U0 starts inventing datatypes, and Chapter 14, where a goal that pairs "a type" with "a value of it" makes the entire language one dataset.

Part II · The Language · Chapter 5

Data from one mechanism: mu

Warp has no built-in booleans, numbers, lists, or pairs. It has one construct for declaring datatypes — and a standard library that uses it nine times.

Here is a Warp datatype declaration, in the surface syntax you feed to --goal:

(data Color (red) (green) (blue))

A declaration lists constructors; each constructor lists typed fields. That's a sum of products — the enum/variant/case-class you already know. The kernel calls the underlying construct mu (the traditional letter for least fixed points), and a declaration is an ordinary term: it can appear anywhere an expression can, including inline in a goal. Its type is a universe — a declaration is a type.

Recursion is where mu earns its keep. A field can be marked rec, meaning "another value of the type being declared". With that one marker, the naturals and lists stop being primitives:

; from prelude.py — the entire definition of Nat
(data Nat (zero)
          (suc (n rec)))

; lists of A (A bound outside): nil, or cons of a head and a rec tail
(data List (nil)
           (cons (x A) (xs rec)))

A natural number is zero or the successor of a natural number. The numeral 3 that the tool prints is pure notation for (suc (suc (suc zero))) — a constructor tree, with a cost the prior will take seriously in Chapter 10. Constructing values uses con (with sugar for the common ones): (con cons true nil), or just (cons true nil) in goal syntax.

Two properties you get without asking

Strict positivity, by unwritability. Languages with expressive datatypes must ban "negative" recursion — types like data Bad = MkBad (Bad -> Bool) whose constructor stores a function out of the type being defined. Such types let you write non-terminating programs (and, in a proof language, prove false things) without any visible loop. Most kernels ban them with a positivity checker — a program that inspects declarations, and whose bugs have historically been soundness bugs. Warp bans them structurally: a recursive position is written with the atomic marker rec, which is not a type expression and cannot sit under an arrow. Bad is not rejected; it is unwritable. The grammar is the checker.

Generativity. Two textually identical declarations are different types — a datatype's identity is its declaration, not its spelling. kernel.py · conv(), VMu case. Nominal typing, in other words, which is what mainstream languages ship anyway. For a data engine it's a feature twice over: when the sampler invents datatypes (Chapter 13), each invention is a genuinely fresh goal even if it happens to be isomorphic to an old one. The one practical consequence: if a goal needs the same inline type twice, declare it once and name it with let —

(let (C (data Color (red) (green) (blue)))
  (-> C C))            ; NOT (-> (data Color …) (data Color …)):
                       ; those would be two distinct Colors

The whole standard library

Because mu plus rec is the entire data mechanism, prelude.py is a catalogue, not a compiler: Unit (one constructor, no fields), Empty (no constructors at all — the type with no values you met in Chapter 4), Bool, Nat, Sig (pairs — Chapter 8), Id (equality! — Chapter 9), List, Vec, Fin (Chapter 8 again). Nine declarations. Everything else is functions defined over them. Appendix D lists them all.

python3 generate.py --goal '(let (D (data Dir (north) (south) (east))) (-> D Bool))' --enumerate 5 --use 'Bool'

Part II · The Language · Chapter 6

One eliminator: elim

Pattern matching, folds, and recursion are one construct — and because it is the only way to consume data, every Warp program terminates by construction.

Declaring data is half the story; the other half is using it. Warp has exactly one construct for consuming a datatype value, the eliminator:

(elim scrutinee motive (case₁) (case₂) …)

Squint and it's a match/switch: inspect the scrutinee, run the case for whichever constructor built it, with the constructor's fields in scope. Two upgrades distinguish it from the match you know, one small and one enormous.

Upgrade 1 — recursion is included. For each rec field, the case additionally receives the result of recursively eliminating that field — an "induction hypothesis", delivered like an accumulator in a fold. Here is addition, the actual prelude definition, translated to surface syntax:

(lam (m n)
  (elim m (lam (_) Nat)          ; eliminate m; result type: Nat
    (zero => n)                  ; m = zero:  return n
    (suc  => (lam (k ih)         ; m = suc k: get k AND ih = k + n,
                (suc ih)))))     ;            return suc (k + n)

The suc case never calls anything: the recursive result ih arrives as an argument. elim at Nat is primitive recursion; at List it is fold; at Bool (no rec fields anywhere) it degenerates to if. Watch it compute — step through add 2 3:

Upgrade 2 — the motive. That second argument, (lam (_) Nat), is the motive: a function computing the result type of the elimination, as a function of the value being inspected. For add it's constant — the answer is Nat whatever m is — and reads as noise. It stops being noise the moment types depend on values: eliminating a length-indexed vector can return a type that depends on the length; eliminating an equality proof (Chapter 9) must return a type that depends on the endpoints, and the motive is where that dependency is spelled. It also quietly explains the mystery syntax from Chapter 2's negation-that-wasn't: (elim x0 (lam (x1.s) Bool) …) — scrutinee, motive, cases. The l you'll see in kernel-level elim terms is just the universe the motive lands in. kernel.py · infer_elim(), velim()

Termination, by construction

Now the payoff promised in Chapter 1. In Warp, there is no other recursion. No general fix, no named self-reference — the only way a computation revisits itself is the induction hypothesis of an elim, and that hypothesis is always computed on a structurally smaller value (a field of the scrutinee). Every chain of recursive calls descends a finite constructor tree, so every program halts. There is no termination checker to trust, appease, or find bugs in — non-termination is unwritable in exactly the way negative datatypes were unwritable in Chapter 5. What survives is everything expressible as structural recursion, which is more than it sounds: add and mul above; and the prelude builds comparison, Vec append, and all of Chapter 12's proofs from the same construct.

Zero cases, and honest emptiness

The degenerate cases are instructive. elim on Empty has no cases to provide — from a value of the empty type, you may conclude anything, vacuously. The enumerator discovers this "ex falso" principle by itself; here it finds the two lazy constant functions first, then the honest one that never needs an answer at all:

Note what it means that #002 typechecks with an empty case list, while the goal Empty itself came back no inhabitants found in Chapter 4: the machine can prove things from absurdity but cannot manufacture absurdity. That asymmetry is consistency, observed experimentally.

python3 generate.py --goal '(-> Bool Bool)' --enumerate 12 --use ''

Part II · The Language · Chapter 7

The judge: checking and evaluation

The typechecker is an interpreter with opinions. Two hundred lines of it decide everything the generator will ever be allowed to emit.

Every term the generator dreams up faces the kernel, and the kernel's verdict is the only ground truth in the system. This chapter is how the verdict is reached. It's also where dependent types stop being philosophy and become engineering: because types can contain programs, the checker must run programs to compare types.

Two modes: infer and check

Chapter 3 flagged that lambdas carry no annotations. The trick that makes this work is bidirectional typechecking: two mutually recursive judgments instead of one.

Infer (given a term, compute its type) handles terms whose type is self-evident: variables (look them up), universes (U l : U (l+1)), Pi types, applications (infer the function, check the argument against its domain), let, the (an ascription carries its type on its sleeve), declarations, elim. Check (given a term and a candidate type, validate) handles the two constructs whose type is not self-evident: lam — which could inhabit many Pis — and con — since many datatypes may share a constructor name. Checking a lam against a Pi pushes the bound variable into scope and checks the body; checking anything inferable just infers and compares. kernel.py · infer(), check()

This division is why Warp terms are annotation-free without any Hindley–Milner-style unification: information flows from the goal. And it is exactly the shape of the generator: --goal is a checking judgment run in reverse. The bidirectional split even dictates a rule you'll meet twice more (Chapters 10 and 11): a let-bound value must be inferable, because let has no annotation slot to check a bare lambda against.

Conversion: when are two types "the same"?

The application rule says: check the argument against the function's domain. But suppose the domain is (Vec Nat (add 1 1)) and the argument has type (Vec Nat 2). Are those the same type? They are — if you run the addition. Dependent typechecking constantly faces such questions, and the relation that answers them is called definitional equality (or conversion): two types are interchangeable when they compute to the same shape. Remember this term; when Chapter 9 introduces its counterpart, propositional equality, the contrast between "the checker can see it by running" and "you must prove it" becomes the most important distinction in the book.

How does the kernel run things? A technique with an intimidating name and a friendly nature: normalization by evaluation (NbE). Instead of rewriting syntax step by step, the kernel evaluates terms into Python values — closures for functions, constructor trees for data — using an ordinary environment-passing interpreter. kernel.py · eval_(), vapp(), velim(). The one twist: an unknown, like a lambda's bound variable, evaluates to a neutral value — a frozen "I don't know yet" that accumulates whatever applications and eliminations pile onto it. Conversion then compares values structurally, applying both sides to fresh unknowns to peer under lambdas (with eta: a function equals anything that behaves like it pointwise). kernel.py · conv(). When output is needed, values are read back into syntax — quote(). Evaluate, compare, read back: the interpreter is the type theory's engine.

let is transparent

One construct got only a nod so far. (let (x e₁) e₂) binds x to the value of e₁ — not to a frozen unknown. The body's type may mention x, and conversion sees straight through it, because the environment literally maps x to the evaluated value. Definitional transparency costs nothing; there's no delta-unfolding machinery because there's nothing to unfold — evaluation already substituted. The consequences for the prior (sharing!) are Chapter 10's climax.

And one construct exists precisely because of the infer/check split. (the T e) is a type ascription: check that T is a type, check e against it, and the whole term infers at T. It is the standard bidirectional mode-shift — the escape hatch that puts a checking-only spelling (a bare lam, a bare constructor) anywhere inference is demanded: a let value, an elim scrutinee, the head of an application. Evaluation erases it, so no ascription value exists and none ever appears in readback; it costs 1 + |T| + |e| nodes — exactly the joint price of stating a type and a term, which Chapters 14 and 15 will meet again from the outside.

Part II · The Language · Chapter 8

Dependency arrives: indexed types

A type with a value-shaped hole in it. This is the chapter where the language starts saying things no simply-typed system can.

Everything so far — functions, universes, datatypes, the eliminator — has a counterpart in ordinary typed programming. Now the counterparts run out. A datatype declaration may take an index telescope: value parameters that vary from constructor to constructor. The classic first example is length-indexed vectors. In goal syntax (from the README, naming it with let per Chapter 5's generativity rule):

(data VN ((n Nat))                          ; indexed by a Nat
  (nil                        -> 0)          ; nil    : VN 0
  (cons (k Nat) (x Nat) (xs rec k) -> (suc k)))  ; cons … : VN (suc k)

Read the arrows as "lands at": each constructor declares which VN n it builds. nil is a vector of length 0 and nothing else; cons takes a length k, a head, a tail of length exactly k (recursive fields specify their indices too — (xs rec k)), and lands at length k+1. The type system now tracks lengths: (-> (VN 3) (VN 3)) is the type of length-preserving functions on 3-vectors, and heads of non-empty vectors never need a "what if it's empty" case.

How checking an indexed constructor works

The kernel rule is disarmingly direct. To check (con c args…) against a fully applied datatype D i₁ … iₖ: check the fields left to right — each field's type may depend on the fields before it — then evaluate the constructor's declared result indices and compare them, definitionally (Chapter 7's relation, so computation is free), with the goal's indices. kernel.py · check(), 'con' case. Match: accepted. Mismatch: rejected. That's the entire theory of indexed families in Warp — no unification, no equality constraints compiled behind your back.

Watch it select inhabitants. Fin n, from the prelude, is the type of numbers strictly below n — fz lands at any suc k (zero is below any positive bound) and fs bumps both the number and the evidence:

Exactly three inhabitants — 0, 1, 2 — and a fourth will never be found, because no assignment of fields makes the result index equal 3… er, makes it equal the goal's index. The generator produces candidates and lets the index check veto them; Chapter 11 names this generate-and-check and prices it.

Dependent functions, for real this time

Chapter 3 promised a Pi whose codomain uses its argument. With indexed types in hand, they're everywhere. "For every n, a number below n+1":

The returned value (fz x0) mentions the argument because the returned type (Fin (suc x0)) does. The tabulation shows the family: at each input, an inhabitant of a different type. This is the general pattern that makes Part IV interesting — a dependent goal is a whole indexed family of search problems wearing one Pi.

And dependent pairs

Pi's mirror image: Sig, the dependent pair — a value a : A together with a value of B a, a type computed from the first component. It's not a primitive; it's a two-field declaration where the second field's type mentions the first field prelude.py · define('Sig', …). Read (Sig A B) as "an A such that B" — an existential. Chapter 2's search goal was exactly this: (Sig Nat (lam (n) (Id Nat n 2))), "a number such that it equals 2", solved by (pair 2 refl). When Chapter 14 needs "a type, together with a value of it", it will reach for the same shape one universe up.

Part II · The Language · Chapter 9

Equality is a datatype: Id and J

The most audacious move in type theory: "a = b" is just another indexed type, "it's true" is just another constructor, and proving is just another kind of programming.

You have now seen every kernel construct. So here is a question with no new machinery available to answer it: what is a proof that two things are equal?

Warp's answer — Martin-Löf's answer — is a three-line library declaration. For a type A and a fixed element a, declare an indexed family Id A a : A → U0 with exactly one constructor: prelude.py · define('Id', …)

(data Id ((b A))          ; indexed by the "other side"
  (refl -> a))            ; one constructor, landing ONLY at index a

Id A a b is a type — read "a equals b (in A)". Its only constructor, refl, lands at index a itself. So when does refl check against Id A a b? Apply Chapter 8's rule mechanically: evaluate the result index (a), compare definitionally with the goal's index (b). The consequence is wonderful: refl proves every equation the evaluator can see, and nothing else.

One node. The checker evaluated add 2 2, got 4, matched the index. This is the promised payoff of Chapter 7's distinction: definitional equality is what computation settles silently, and Id — propositional equality — is how the language talks about equality as a fact worth proving. The two meet at exactly one point: refl, the bridge that turns "the evaluator can see it" into "it is on the record".

Using an equation: J is just elim

Producing equalities is refl; consuming them is — of course — elim. What does case analysis on a proof p : Id A a b look like? There is one case, refl, and that case only ever arises when b is a. So the eliminator says: to prove something about a, b, and p, it suffices to prove it when b is literally a and p is literally refl. In type-theory books this principle is called J. In Warp it is not a rule — it's what the generic eliminator happens to say when pointed at this declaration. The motive (Chapter 6's "result type as a function of the scrutinee") is essential now: it abstracts over the index b and the proof, which is how the conclusion gets to mention both.

Watch it in a real proof — symmetry, as the enumerator discovered it in Chapter 1, now fully legible:

(lam (x0 x1 x2)                          ; a, b, p : Id Nat a b
  (elim x2                               ; eliminate the PROOF
    (lam (i3.0 x3.s) (Id Nat i3.0 x0))   ; motive: for any endpoint i and proof,
                                         ;   "i equals a"
    (refl => refl)))                     ; when b is a: a = a, by refl

The motive instantiated at the actual endpoint b gives the goal Id Nat b a; the single case owes it only at i = a, where it collapses to Id Nat a a — one refl. That's the entire proof, and the eliminator's computation rule (the same velim that ran add) makes it compute: applied to an actual refl, the proof returns refl. Transitivity is the same trick — eliminate the second proof, motive "a equals the moving endpoint", and the case hands back the first proof unchanged:

python3 generate.py --goal '(pi (f (-> Nat Nat)) (pi (a Nat) (pi (b Nat) (-> (Id Nat a b) (Id Nat (f a) (f b))))))' --enumerate 1 --use '' --max-size 14

Part III · The Ruler · Chapter 10

Description length

Every ordering needs a ruler. Warp's is brutally simple — one node per construct — and its integrity is defended in two places you might not expect.

"Simplest first" only means something once simple is a number. Warp's measure is description length (DL): count one for every syntactic construct in the term — every lam, pi, application, variable, universe, constructor, let, the, elim, and every piece of a data declaration. kernel.py · count_nodes(). That last clause matters: declarations are terms (Chapter 5), so a sampled datatype is priced by the same ruler as everything else — a type definition is not free context, it's part of the description.

Why care so much about a node count? Because in a generator, the measure is the prior. Enumeration presents candidates in DL order; sampling (Chapter 13) draws with probability decaying geometrically in DL. Whatever the ruler undercounts becomes free and floods the output; whatever it overcounts vanishes. A simplicity prior is a claim about what "typical" data looks like, and Warp's claim is the minimum-description-length one: a program's weight should track the cost of writing it down.

Two places the ruler is defended

No literal loophole. In most languages, 7 and 7000000 cost the same to write. Under a DL prior that's a subsidy: huge constants would be as "simple" as small ones. Warp refuses: a numeral is its constructor tree, so 7 costs 8 nodes and 7000000 costs 7,000,001. Expensive big numbers aren't a bug — they're the claim that magnitude is complexity, under the unary representation. And representation is a modelling choice, not a stipulation: declare a binary-digits datatype and its numerals cost O(log n); the prior prices whichever representation you actually use. Warp's predecessor (Weft) needed a special per-digit literal rule in the kernel to get this effect; in Warp it's a theorem about a library choice.

Sharing is real, so the prior must see it. Consider a term that uses the same expensive subterm three times. As a tree it pays three times; as a program with a local name it pays once plus three cheap references. Which is the "true" complexity? Program-length complexity — the Kolmogorov-flavored notion MDL descends from — says the shared spelling: descriptions may name and reuse. let is how Warp's prior agrees. Binding a subterm once and referencing it by a 1-node variable moves the measure from tree size toward DAG size. A striking corollary, embraced deliberately: iterated-doubling terms describe values of size 2ⁿ in O(n) nodes — so evaluation is guarded by fuel, not by any pretense that term size bounds work.

Here is sharing surfacing in the wild — a sampler run over an uninterpreted signature (Chapter 14 explains --postulate); note k1.0, bound once and used three times:

The generator's let discipline keeps the ruler unambiguous. It emits let only in maximal-sharing form: the bound value must be a non-variable inferable term (an application spine — Chapter 7 said why nothing else can be inferred), and the body must use the name at least twice. An unused let is dead code; a single-use let always loses to inlining by exactly one node. Ruling both out means no term ever has two competing generated spellings of trivially equal cost — let appears precisely where sharing genuinely pays. generate.py · enum_lets(), count_uses()

One special price remains — motives are charged 1 node when mechanically derived from the goal — but it belongs to the proof-search story, so it waits for Chapter 12.

Part IV · The Loom · Chapter 11

Enumeration

At every goal, only a handful of moves are even grammatical. The enumerator's whole art is reading them off the goal's head — and never trying anything else.

You've now watched a dozen enumerations. This chapter is how they work — and the answer is smaller than you'd guess. The enumerator asks one question of the goal: what is your head? Each head licenses a short, fixed menu of productions: generate.py · _enum_at()

That's the entire grammar of the search space. Enumeration then runs sizes 1, 2, 3, … and at each size generates every production whose parts can be budgeted to fit — so output is exhaustive in DL order by construction. Three refinements do the heavy lifting:

Generate-and-check at indexed goals. For a constructor of an indexed family (Chapter 8), candidate fields are enumerated first, then the result indices are evaluated and compared with the goal's — mismatches discarded. No unification machinery; the checker's own veto is the filter. This is the deliberate tractability trade: where the goal is plain data the veto never fires and enumeration is cheap; where the goal is a theorem (Id's index check is maximally picky) the same veto makes the search honest. The cost lands exactly where the difficulty is.

Spines, pruned. Application spines — (add x0 1), (mul (add x0 x0) 2) — are enumerated head-first: pick an in-scope function, enumerate arguments recursively, accept when the final type converts to the goal. One cheap test avoids most dead ends: saturate the head's type with dummies and compare heads — a spine ending in Nat can never meet a Bool goal, so no argument enumeration is even attempted. generate.py · head_compatible()

Memoization by scope, not just by goal. Results are cached per (goal, size, scope signature) — the signature includes the types of everything in scope and the definitions of let-bound values, since a transparent definition (Chapter 7) can change what typechecks. Sub-searches repeat massively across sizes; the cache is what makes exhaustive search practical. generate.py · enum_at(), Scope.sig

Part IV · The Loom · Chapter 12

Proof search for free

Nothing in the enumerator knows what a theorem is. Add one pricing rule for motives, and the same machine that lists functions starts discovering induction proofs.

Chapter 9 left a cliffhanger: add 0 k = k is free (computation sees it), but add k 0 = k is stuck — true, yet invisible to the evaluator, because add recurses on the unknown k. Every proof of it must do induction: eliminate k, prove the base, prove the step given the induction hypothesis. Chapter 6's elim has everything needed… except one awkward piece of pricing.

The motive problem

To eliminate k when the goal is (Id Nat (add k 0) k), the motive must be "the goal, with k abstracted out": (lam (m) (Id Nat (add m 0) m)). That's a large term — and enumerated from scratch it would cost its full size, pushing routine induction proofs absurdly deep into the search order. But notice what the motive actually is: the goal you already wrote down, with some occurrences of the scrutinee replaced by a hole. The information content isn't the term — it's which occurrences to abstract.

So the generator synthesizes motive candidates by goal abstraction: take the goal, take the set of occurrences of the scrutinee (and, for indexed scrutinees, its index values), and for every subset of those occurrence-slots, abstract that subset into motive variables. The empty subset is the constant motive (Chapter 6's boring case); the full subset is complete generalization; the subsets in between are the classic "generalize before you induct" moves, including the partial ones proof texts teach as an art. Unsound choices are cheap to reject — the candidate simply fails to typecheck against the motive type. Each surviving candidate is charged one node, because one abstraction choice is one decision, the goal itself having already been paid for. Free-form motives — enumerated at the motive type like any other term — remain available at full price, so nothing is lost, and at larger budgets the enumerator really does propose motives no abstraction of the goal could produce. generate.py · abstraction_motives(), enum_elims()

Watching it work

With motives priced, "proof search" is nothing at all: enumerate the theorem type. You have already read the discovered sym (Chapter 9) — goal abstraction produced its motive by abstracting the index b. The induction showcase, found in well under a second:

Read the skeleton, not the noise: induction on x0 (the outer elim); a motive that is the goal with k abstracted — the inlined add is why it looks bulky; base case refl (at zero, computation takes over — Chapter 9's checkpoint); and a step case that rewrites by the induction hypothesis using a J-elimination (the inner elim x4 … (refl => refl)), a move nobody taught it. The tabulation row at the bottom is the proof running: at every input it computes to refl, as a proof-by-induction must. This proof's tree size is far above 17 — the DL discount is the motive rule making induction affordable, which is the entire point.

Note also what an honest engine does when a goal is false or out of reach: Chapter 4's Empty search returned no inhabitants of size ≤ 9. There is no "failed" state distinct from "not found at this budget" — semidecidability worn openly. Chapter 16 turns even that into a dataset feature (hard-negative mining by budget).

Part IV · The Loom · Chapter 13

Sampling under the prior

Enumeration walks the space; sampling throws darts weighted by simplicity. And at a universe goal, the darts start inventing types.

Exhaustive DL order is perfect for search and for small spaces, but a dataset usually wants draws from a distribution — diverse, sized-varied, duplicable-on-purpose. That's --samples. The mechanism: generate.py · sample_at(), sample_goal()

Draw a budget, then descend. Each sample first draws a size budget from a geometric-flavored distribution (an exponential over --tau, offset by --min-budget, capped by --max-budget), then walks the same production menu as Chapter 11 — weighted coin-flips choosing among variables, constructors, spines, eliminations, lets — spending budget as it goes. Bigger budget, deeper terms; the budget distribution is the prior.

Reject and retry. The descent can die: an indexed constructor's result indices may miss the goal (Chapter 11's generate-and-check veto), evaluation may exhaust fuel, a branch may dead-end. Failures are simply rejected and redrawn. The distribution you end up sampling is therefore not the raw prior but the prior conditioned on typeability and feasibility — which is exactly the honest thing: the weight a term deserves, given that it exists. Duplicates are expected and labeled ((dup) in the output) — a short program being drawn often is the prior working, not a bug:

Sampling types — and inventing them

Point the sampler at U0 and the productions shift to the universe menu (Chapter 11's table)… plus one production the enumerator doesn't have: fresh data declarations. generate.py · sample_desc(). The sampler assembles a never-before-seen datatype — one to three constructors, fields drawn from in-scope base types, recursive fields sprinkled in — and, because declarations are terms priced by the same ruler (Chapter 10), the invention pays for every node of itself. Generativity (Chapter 5) makes each invention a genuinely new type; --inhabit K then turns around and samples K values of each:

Read #000 slowly, because it's the thesis of the language in one line: the sampler invented a recursive datatype, then a function type out of it, and then two functions of that type — types, programs, and data drawn from one distribution. This is what "the prior extends to types" means, and no stage of it was a special case.

Part IV · The Loom · Chapter 14

Enumerating everything

"List every well-typed program, simplest first" sounds like it needs a new mode. It needs a goal — because in a dependent language, "any program, whatever its type" is itself a type.

Everything so far enumerated inhabitants of a fixed goal. The natural next want — this book's reason for existing, if you build training data — is the unconstrained version: every well-typed program, of every type, in one simplicity-ordered stream, each labeled with its type.

Try to say that in a simply-typed language and you're stuck: "a value of some type" isn't a type there. In Warp it is. What's being asked for is a pair: a type A, and a value whose type is A — the second component's type depending on the first component's value. That's Chapter 8's dependent pair, with its first coordinate ranging over U0. The prelude's Sig can't host it (its parameters live in U0, and U0 : U1 — predicativity, Chapter 4, doing its job), but Chapter 5 gave us declarations anywhere, and a two-field declaration with a universe field lands in U1 without complaint:

(data W (mk (A U0) (a A)))     ; a small type, and a value of it

Why does this work with no new machinery? Chapter 11's constructor production enumerates fields left to right, dependently: the first field's goal is U0 — the universe menu, so types come out — and the second field's goal is whatever type the first field just produced. The type flows from the first coordinate into the second coordinate's search, inside one enumeration. "Unconstrained" was never the right word; the type isn't dropped, it's bound — moved from the query into the data. The loom on this book's cover is this goal running.

Reading the fine print

The DL is joint. (mk Nat 0) costs 3: the pair node, the type, the value. Ordering is by simplicity of the (type, program) pair — arguably the right MDL reading, since a program's description isn't complete without its type, but know that it's not "simplest term, annotation free": a cheap term of an expensive type sorts late.

It ranges over U0. Programs whose types live higher (type operators, the polymorphic identity) aren't in this stream. Nothing deep — a second field at U1, or a nested pair one level up, extends it.

No invented types. Chapter 13's asymmetry bites here: enumeration's universe menu never mints fresh declarations, so the A coordinate ranges over what's in scope — the --use vocabulary and its Pi-closure. The sampling version of this same goal does invent (that's Chapter 13's --inhabit output, repackaged); the exhaustive version inherits the enumerator's conservatism.

The other "everything"s

Two more enumerations deserve the name, each a different answer to what counts as one datum?

Behaviors, not spellings: --dedup. Chapter 2's checkpoint found the identity function wearing an elim costume. For observable goals (Nats in, data out), --dedup keys enumeration on the observed input/output table, discarding every later spelling of an already-seen behavior — enumerate the functions themselves, not their syntax. Boolean-valued tables render as #/. grids, which for two-argument predicates are literally pictures — the weave the loom was making all along:

The first six behaviors of (-> Nat Nat Bool) under --dedup (8×8 window, row = first argument): the two constants, then x0 = 0?, x0 > 0?, x1 = 0?, x1 > 0? — each grid the actual tabulated output of the first program found with that behavior.

Free algebras: --postulate. An axiom is a constant with a type and no computation rule. Postulating a signature — 'F=U0', 'fadd=(-> F F F)', 'e=F' — turns the generator into an enumerator of uninterpreted syntax trees over that signature (Chapter 10's sharing example was one). Term-algebra datasets, rewriting corpora, "here is an expression, simplify it" pairs: all downstream of three flags. The warning label: a postulated equality is an Id with no refl behind it, so proofs that use it no longer compute to canonical forms — fine for syntax datasets, poisonous for anything that must run. Axioms are a per-dataset knob, deliberately not a kernel feature.

Part IV · The Loom · Chapter 15

The loom in reverse

Chapter 14 asked one type for every program. This chapter never asks: it builds programs out of programs and reads each type off the construction — and every equality it lands on is a theorem, arriving with its proof.

Every mode so far ran in one direction: a goal in hand, a search for inhabitants. The search is generate-and-check — most of what Chapter 11's productions propose at an Id goal dies on the index comparison, and a false equation consumes a full search at every size while yielding nothing. That cost is not waste, exactly; it's the price of conditioning. You chose the type, so the engine must pay to find out what lives there — or that nothing does.

Now recall Chapter 7's economics from the other side. Checking a finished term is cheap; only the search was expensive. So run construction in the direction where nothing can fail: start from the --use vocabulary as a table of (term, type) pairs, and grow the table by moves that only ever combine entries already known well-typed. Apply a table function to a table argument whose type matches its domain. Build a constructor from table fields. Eliminate a table scrutinee under a table motive. Each move computes its result type instead of requesting one, and the kernel re-checks every admitted pair, so work is proportional to pairs produced — there is no failed search to pay for. generate.py · FTable

One obstacle stands in the way, and it is a familiar one. Chapter 7 put lam and con in checking mode: a bare lambda inhabits every (-> A A), so "build terms, infer their types" is undefined for half the grammar. The fix is not annotations at every binder — Chapter 10 would bill you for restating the type inside the term — it's the hypothesis mechanism: pick a domain A from the table's type entries, saturate a sub-table under a hypothesis x : A, and discharge each of its entries b : B to the pair (lam (x) b) : (pi (x A) B). The chosen A lands in the pair — exactly where Chapter 14 kept it, outside the term. (When a single term does need its type inline, Chapter 7's the is the same annotation internalized, at the same price.) Motives for the elimination move arrive the same way: a discharged lambda into a universe is a motive-shaped entry, and the table doesn't know the difference.

The ordering is joint DL — 1 + |type| + |term|, Chapter 14's everything-pair measure to the node. That identity is the point: forward and backward are two ways of walking one priced space. The everything-pair walks it by querying (type first, term searched); the table walks it by construction (term first, type computed); the ruler is indifferent.

Theorems from proofs

Here is what the direction buys. Every table entry whose type is an Id is a theorem, and its term is the proof — not found, caused. --theorems filters the stream to exactly those:

Read #002 the way the table made it. Nobody asked whether add 0 0 equals 0. An application chain minted the type (Id Nat (add 0 0) 0) as an ordinary table entry — Id applied to Nat, then to a spine, then to a numeral, each step a move — and the constructor move then noticed that refl's index check passes there, because the evaluator computes add 0 0 to 0 on the spot. The statement and its proof condensed out of the same saturation. Compare Chapter 12, where add k 0 = k was found by paying seventeen nodes of search at a goal someone chose: different economics in kind, not degree. The trade is symmetric and honest — forward cannot be pointed at a question. The types fall out; --goal and --theorems are filters on the stream, not questions put to it.

Sampling the moves

Chapter 13's sampler rejects and retries; a forward random walk barely knows how to fail. Pick a move, pick table entries for its slots, land a pair — the only "rejections" are duplicates and the DL cap, so nearly every step of work emits a new labeled datum, which is exactly the shape a dataset pipeline wants:

#003 is the polymorphic-flavored identity at U0, discharged from a sub-table under a type hypothesis; #004 dropped a library function under a binder. The walk visits indexed families more often than their numbers warrant (their constructors are the index-checked, theorem-bearing ones), and one distribution caveat is worth writing on the box: the walk samples constructions, not the DL prior — a pair reachable by many move sequences is drawn more often than Chapter 13's budget draw would give it. Filter, reweight, or use the exhaustive stream when the prior itself is the spec.

Part IV · The Loom · Chapter 16

Recipes for datasets

The engine assembled, cookbook-style: seven patterns for ordering up synthetic data, each a goal plus a handful of flags.

1 · Function corpora with ground-truth behavior. Goal an arrow into observable data; the tool tabulates every emission on small inputs — program and behavior arrive together, already paired for training:

python3 generate.py --goal '(-> Nat Nat)' --samples 500 --seed 1 --use 'add,mul,Nat'

Knobs that matter: --use is the vocabulary (Exercise 11.1 — the library is part of the prior); --min-budget/--tau shape size; --window widens the behavior table.

2 · Behavioral coverage, not syntactic coverage. When diversity means "different functions", not "different spellings": --enumerate --dedup. Each emission is the cheapest program yet found for a new behavior — a canonical-implementation dataset by construction (and, read the other way, a natural "many programs, same behavior" equivalence corpus if you diff against the non-deduped stream).

3 · Domain types without writing a compiler. Inline data forms give every dataset its own vocabulary of shapes — enums, records, trees — declared in the goal string, priced by the prior, generative so each is fresh. Remember the two rules of goal-local types: let-bind a declaration used twice (Chapter 5), and don't expect generated eliminations into a goal-local type (Chapter 11's fine print).

4 · Theorem/proof pairs, difficulty-graded. Enumerate at a proposition; the DL of the least proof is a difficulty score the engine computes for you. Chapter 12's asymmetry is the design tool: add 0 k = k costs 2, add k 0 = k costs 17 — same surface shape, an order of magnitude apart in search depth. Families of goals (vary the equation, vary the direction) yield curricula; goals that time out at budget B are hard negatives at that budget, honestly labeled semidecidable.

5 · Witness-finding (search) data. Sig goals are constraint problems with certified solutions: (Sig Nat (lam (n) (Id Nat (mul n n) 9))) enumerates to (pair 3 refl) — puzzle in the goal, answer plus proof in the output. Compose Sigs for multi-part records (Exercise 14.2).

6 · Uninterpreted syntax at scale. Postulate a signature, sample the free algebra (Chapter 14). Because postulated constants never compute, every sample is pure structure — ideal for expression corpora, and let-sharing emerges naturally in samples (Chapter 10's 32-node specimen). Keep postulated equalities away from anything that must evaluate.

7 · Types-then-terms, hierarchically. The two-stage draw — --goal U0 --samples N --inhabit K — is a topic model: each sampled type is a "topic", its inhabitants the documents (Chapter 13). The exhaustive counterpart is Chapter 14's everything-pair when you need coverage guarantees instead of diversity. Between them: sample types, then enumerate each one's inhabitants by re-invoking with the sampled declaration pasted into --goal.

8 · Theorem mining, forward. When the dataset is "true statements with certified proofs" and you don't care which truths, run the loom in reverse (Chapter 15): --forward N --theorems streams Id-typed pairs at cost proportional to output — no goal chosen, no empty types paid for. --forward-samples is the random-walk version for volume; --goal turns either into a conditioned filter. Pair it with recipe 4: backward search grades the difficulty of the statements forward mining discovered.

And that is the book's arc in reverse: recipes stand on the generator (Part IV), the generator on the ruler (Part III), the ruler on a language where types, data, proofs, and declarations are all terms of one small calculus (Part II), which exists because someone asked a plain question (Part I): if a type is a description of data, how much data can one description language order up? The appendices that follow are the reference card; the loom is yours now.

Appendix A

Syntax reference

Core terms (kernel.py)

e ::= x                          variable
    | U l                        universe, l = 0, 1, …    (U l : U (l+1))
    | (pi (x A) B)               dependent function type
    | (lam (x) e)                unannotated; checked against a Pi
    | (e1 e2)                    application
    | (let (x e1) e2)            transparent definition; e1 inferred,
                                 x bound to e1's VALUE
    | (the T e)                  type ascription: e checked at T,
                                 inferable; erased at evaluation
    | (mu D)                     a datatype — a first-class term
    | (con c e …)                constructor application
    | (elim e P cases)           the generic eliminator; the
                                 motive's universe is derived from P

D     ::= name [x : A, …] { c fields -> i … ; … }
field ::= (x : A)                ordinary field (A any type term)
        | (x : rec i …)          recursive field at the given indices

Field types may depend on earlier fields; result indices are arbitrary terms over the fields. There is no separate type grammar — types are terms.

Goal language (generate.py --goal)

goal ::= x                       prelude or bound name (Nat, add, …)
       | U0 | U1                 universes
       | 3                       integer literals elaborate to Nat
       | true | false | tt
       | zero | refl | nil       constructor sugar
       | (suc e)
       | (-> A B … R)            right-nested non-dependent arrows
       | (pi (x A) B)            dependent function type
       | (lam (x y …) e)         curried lambda
       | (let (x e1) e2)         transparent definition
       | (the T e)               type ascription
       | (con c e …)             constructor of any type in scope
       | (f a b …)               application
       | (data Name [((i T) …)] (c field … [-> idx …]) …)

field ::= (x T)                  ordinary field
        | (x rec idx …)          recursive field at the given indices

In a data form the optional first group is the index telescope; terms after -> in a constructor are its result indices. Declarations are generative — bind with let to reuse one (Chapter 5).

Appendix B

The typing rules, in prose

Stated informally but completely; the code is the formal version. Inferable: variables (from context), U l : U (l+1), Pi (both parts must be types; result universe is the max of theirs — predicative, no cumulativity), application (infer the function to a Pi, check the argument against the domain, substitute into the codomain), let (infer the bound term, bind its value, continue), the (check T to be a type, check e against it, synthesize T — the mode-shift from checking to inference, erased at evaluation), mu (see below), elim (see below). Checkable only: lam against a Pi (bind, check body against instantiated codomain) and con against a fully applied datatype — (the T (lam …)) promotes either into inference position where one is needed (a let value, an elim scrutinee, the head of a spine). Any inferable term checks by inferring and comparing with conversion — untyped NbE value comparison with eta for functions; datatypes compare by declaration identity plus closed-over values (generative).

Declarations. (mu D) : A₁ → … → Aₖ → U l where A₁…Aₖ is the index telescope and l the maximum universe of index and field types. Each constructor's fields are a telescope (later types may use earlier fields); rec fields carry index terms; result indices are terms over the fields.

Constructors. To check (con c e…) against D i₁ … iₖ: find c in D, check fields left to right against their (dependently instantiated) types — rec fields against D at their declared indices — then evaluate the declared result indices and require each definitionally equal to the goal's. This one rule is why refl proves computations (Chapter 9) and why Fin 3 has three elements (Chapter 8).

Eliminations. For (elim s P cases): infer s to a fully applied datatype D ī. The motive P must check against (pi (indices…) (pi (x (D indices…)) (U l))) — a function from the indices and the scrutinee to a type in some universe U l, where l is derived from P itself (peel its lambdas through the telescope, infer what remains), never written in the term. Each constructor needs one case, checked against: fields, each rec field followed by an induction hypothesis (the motive at that field), concluding in the motive at the constructor's result indices and the rebuilt constructor. The whole elim has type P ī s. Computation: on (con c args…), apply c's case to the fields, interleaving recursive eliminations after each rec field; on an unknown, freeze as neutral.

Guarantees by construction: strict positivity (no type expression can sit at a recursive position — rec is a marker, not a type), termination (recursion only via elim, always structurally smaller), consistency discipline (predicative universes; an inhabitant of Empty or a false Id would need a constructor that doesn't exist).

Appendix C

CLI reference

Appendix D

Prelude catalogue

Everything below is a library definition in prelude.py — none of it is kernel. Names in the left column are what --use accepts.

Appendix E

Kernel map

Where each concept in this book lives, for reading along. Line numbers drift; names don't.

Appendix F

Glossary