disp, from first principles

Section 1Motivation

1.1 · What is disp?

Disp is a dependently typed programming language based on the computational model of the tree calculus, rather than the λ-calculus, where the type system is a first-class object. Type-checking is one equation:

T (v) = Ok true  ⟺  v : T

In words: the type T, applied to the value v, reduces to the verdict Ok true if and only if v inhabits T. Traditional type theory maintains a separate judgment Γ ⊢ v : T, derived by inference rules that live outside the language. Disp has no such separate machinery. Types are themselves tree-calculus programs: predicates that, run against a candidate tree, return a verdict. Type-checking is, then, just function application on those predicates. (The verdict is a CheckerResult — Ok or Err — so failure is an ordinary value too, not an exception in some meta-language.)

1.2 · Why does this design exist?

The long-term aspiration is a self-improving optimizer: a program that, given a specification of "good program" (encoded as a type — which is just a predicate), searches for programs satisfying it and improves the search program itself over time. For that loop to close, every component — the specification, the checker, the scoring function, the candidate programs — must live inside a single self-inspecting computational universe.

Compare the mainstream proof assistants. Lean, Rocq, and Agda all descend from the LCF traditionEdinburgh LCF (Gordon, Milner & Wadsworth, 1979) established the 'small trusted kernel + everything else as a library' architecture: only the kernel can mint theorems, so soundness reduces to auditing it, yet each still ships a trusted kernel written in its implementation language — Lean 4 self-hosts its elaborator, but the trusted kernel is C++; Rocq's and Agda's checkers remain in OCaml and Haskell. Those kernels accumulate host-language machinery — mutable hash tables, exceptions, pattern-match compilation — with no counterpart in the language being implemented. Disp applies the LCF discipline from the start, and more literally: the checker is a tree program checking tree programs.

The operating principle, and this walkthrough's spine: the object language is the specification; host implementations are optimizations. The TypeScript runtime (src/core/tree.ts) and the Rust evaluators accelerate the in-language definitions, and must produce identical decisions — they are validated against the in-language reference, byte for byte.

Section 2From λ-calculus to trees

The untyped λ-calculus has terms M, N ::= x | λx. M | M N and one rule, β-reduction: (λx. M) N →_β M[x ≔ N]. Its key limitation, for our purposes: λ-terms cannot inspect their own structure by reduction. Given a λ-term f, there is no β-reducible context in which we can ask "is f a function or an atom?". Everything is a function.

2.1 · The SKI detour

Curry and Schönfinkel showed bound variables are dispensable: three combinators suffice.

SKI is combinatorially complete — every closed λ-term compiles to it. But SKI inherits the same limitation from λ-calculus: there is no reducible operation that asks "is this an S or a K?"

2.2 · Tree calculus

Tree calculus, due to Barry Jay, keeps combinatorial completeness and adds exactly the missing power. There is one base piece: t (written △ in the literature — the "leaf"). Trees are assembled by application, and every tree in normal formin tree calculus, every tree is already in normal form — reduction only happens through apply is one of:

t (leaf)  ·  t u (stem)  ·  t u v (fork)

Application is not a syntactic constructor; it's an external operation apply : Tree × Tree → Tree. Trees by themselves don't reduce; reduction happens only through apply.

2.3 · The five rules

apply(f, x) is defined by five rules that partition on the shape of f — and, for the last, on the shape of x:

The first two rules are passive — they just grow trees. K and S match their SKI counterparts. The fifth rule — F, the triagethe third reduction rule: a function of shape t (t c d) b dispatches on the shape of its argument (leaf, stem, or fork) — the primitive reflection mechanism — is the new ingredient: it is the only rule whose behavior depends on the shape of the argument. Reduction itself can inspect tree shape.

The lab below evaluates any expression you type. Press Step to fire the next reduction and watch which rule carries it: the amber letter marks the next redexa reducible expression: an application whose function (and, for triage, argument) is in the right shape for a rule to fire, and pruned leaves fall where all pruned leaves go. The toggles are worth a poke: parallel fires every ready redex per round, which is legal because tree calculus is confluent, and nature off turns the grove back into a plain diagram.

2.4 · Bracket abstraction: compiling λ to trees

Surface disp has binders; trees don't. The bridge is bracket abstraction: [x].M ("abstract x out of M") produces a closed expression in I, K, S and application:

Nested binders peel inside-out: [x].[y].y = [x].I = K I. The compiler adds two semantics-preserving optimizations — η-reductionthe identity λx.(f x) = f when x is not free in f; the application and the bound variable cancel ([x].(N x) = N when x ∉ N) and K-composition (S (K p) (K q) → K (p q)) — which substantially shrink the output. These live in src/elab/cir.ts and are part of definitional equality: once compilation finishes, there is nothing in the runtime that is not a tree.

2.5 · Hash-consing and O(1) equality

The runtime stores every distinct tree exactly once (hash-consingstructural sharing: identical subtrees share one heap cell, so structural equality collapses to integer-identity comparison), so structural equality reduces to an identity check:

export function treeEqual(a, b) {
  return a.id === b.id   // O(1) — no traversal
}

Why does this matter so much? Because conversion checking in a dependent type system is structural equality of normal forms — the hot loop of every proof assistant. Making conversion O(1) keeps type-checking cheap. It also makes the kernel's H-rule (§5) tractable: "the stored type of this hypothesis equals the required type" is decided by hashed identity, because deterministic elaboration produces identical trees for identical types.

Section 3A first look at disp

The notation is small, and from Section 4 onward we will read it constantly, so it pays to nail down what the symbols mean. The grammar's authoritative source is SYNTAX.typ.

3.1 · Binders and application

{x} -> body                // λx. body
{x, y} -> body             // λx. λy. body  (curried)
{x : A, y : B} -> body     // annotated binders

The elaborator lowers binders via bracket abstraction (§2.4). Application is juxtaposition and associates left. The literal t denotes the leaf — the only "literal" the language truly has; numbers and strings are sugar for particular trees built by application.

3.2 · Declarations and tests

// untyped definitions — plain combinators
i := {x} -> x
k := {x, y} -> x

// a test is a compile-time obligation: reduce both sides,
// demand the identical tree
test i t = t
test k t (t t) = t

A test is a compile-time obligation: parse both sides, reduce, demand the identical tree. If the equation does not hold, the file fails to load. Tests are how the library asserts properties of definitions — and how the type checker itself is exercised on every load.

A typed definition carries its type before :=. The annotation is an ordinary expression (typically a Pi), and it is enforced: when a module loads, every typed export is verified through the kernel. An annotation the value doesn't satisfy is a compile error, not a comment.

// a typed definition: the annotation is an expression too, and the
// compiler VERIFIES it through the kernel when the module loads
quadruple : Nat -> Nat := {n} -> double (double n)
test quadruple 3 = 12

Sum types have a literal form that auto-binds constructors, and match eliminates them by tag. Booleans are not a tagged sum (§4.2), so they eliminate with if:

// a sum-type literal auto-binds its constructors…
Wrap : Type := < box : Nat, empty >
test param_apply Wrap (box 4) = Ok true

// …and match eliminates by tag, binding payloads
test (match (box 4) { box n => double n; empty => 0 }) = 8

// booleans eliminate with if (they are shapes, not tagged sums)
test (if true then 1 else 2) = 1

3.3 · Modules

open use "path/to/file.disp" loads a module and splices its exports into scope. Modules are hermetic: a used file sees only its own definitions, its own opens, and its declared givens — never the user's scope. A module that needs something from outside declares it explicitly (given X : T) and callers fill it (use "f.disp" { X := v }) — which makes every module a checkable functor from its givens to its exports. The kernel bootstraps itself through exactly this mechanism.

Section 4Types as predicates

4.1 · Four traditions

Disp's row is closest to the predicate-logic row, and we'll borrow Curry–Howard vocabulary informally throughout. The load-bearing difference from all three other rows: T and v live in the same universe. In predicate logic, formulas are syntactic objects and values are model-theoretic; you can't apply a formula to a value without an interpretation step. In disp both are trees, and applying one to the other is just apply. That is what makes the type-checker writable as a tree program rather than as an external interpreter.

4.2 · Booleans are shapes

For T v = Ok true to be a literal equation, the language needs booleans that are trees. Disp's are the two smallest distinguishable ones:

true = t  ·  false = t t

A boolean carries no eliminator of its own — it is raw data, and consuming it is a triage: the F rule reads the argument's shape (leaf or stem) and picks a branch. if c then a else b is sugar for exactly such a dispatch. Here is a hand-built not, one F-rule firing per call:

// the two booleans are the two smallest distinguishable trees
test tree_eq true t = true
test tree_eq false (t t) = true

// elimination is a triage: the F rule reads the shape
shape_not := t (t false (t t true)) (t t (t t true))
test shape_not true = false
test shape_not false = true

4.3 · The central equation, running

// the central equation, executable: apply the type, read the verdict
test Nat 3 = Ok true
test Nat (t (t t)) = Ok false

// the verdict is a value (a CheckerResult), so failure is data too —
// no exceptions, no judgment layer

That is the entire type-check for a concrete value: an apply and a handful of reductions. No context, no judgment. Which sets up the real question — the one the kernel exists to answer. What happens when v is not a closed value but a variable bound by some surrounding lambda?

Section 5The two-operation kernel

Everything else about the type system — Pi, records, Bool, Nat, Eq, the universe Type — is library code you can read in lib/kernel/. The kernel proper is two operations and a dispatcher. This section is about why those two, and why they must be trusted.

5.1 · The hypothesis problem

Does quadruple := {n} -> double (double n) have type Nat -> Nat? The annotation claims something about infinitely many inputs. No amount of running visits them all. Martin-Löf type theory answers with a context variable — "assume n : Nat" — managed by judgment rules outside the language. Disp has no context object, but it must solve the same problem operationally.

The answer is a placeholder with three properties: (i) it carries its declared type, so later checks can look that up; (ii) it has a fresh identity, so distinct placeholders are distinguishable; (iii) user code, running against it, cannot peek at any of this. Such a placeholder is called a hypothesis (or neutral), and this walkthrough will also call it a promise: a promise that a Nat will be here.

The kernel mints one as a specific tree shape:

hyp T id  =  wait (hyp_reduce) (meta)

where waitwait f x y reduces to f x y, but wait f x by itself does NOT evaluate f x — it lets a tree carry a handler at its head without that handler firing until another argument arrives defers the handler and meta packages the stored type, the fresh identifier, and the spinethe running log of how the hypothesis has been applied so far — how neutrals stay neutral under further application. The tree's signature — kernel-speak for "what function sits at the head", read by the sanctioned pair_fst projection — is hyp_reduce. Signatures are the kernel's routing keys.

// mint a promise by hand: an opaque tree carrying a type and nothing else
let hN := make_hyp Nat 0

// a promise of a Nat counts as a Nat (the H-rule: stored type vs
// required type, compared by hash-cons identity)
test param_apply Nat hN = Ok true

// it is a neutral — recognizable, not inspectable
test is_neutral hN = true

5.2 · The dispatcher and the walker

Both attacks are blocked by one mechanism: param_apply, the kernel's two-argument dispatcher. Every checked application routes through it, and it runs in one of two regimes:

The walker enforces operational parametricityhypotheses are opaque tokens for universal quantification: user code cannot inspect their structure or synthesize new ones: under it, a hypothesis behaves like an opaque universally-quantified value. That is exactly what makes "f h checks for a fresh h" mean the same thing as "f is correct on all inputs". A type that tries the illegal question doesn't crash the checker — the question itself is refused:

// under the dispatcher, a type that peeks at its argument's raw shape
// is refused — either answer would leak what the promise doesn't contain
test param_apply (Pi Nat ({_} -> Bool)) ({x} -> is_fork x) = Err

5.3 · The two operations

① bind_hyp — mint a promise. The mechanism by which Pi A B verifies "for all x : A, the body holds". bind_hyp mints a fresh hypothesis of type A, runs the body under the walker (so the body cannot reflect on the mint), and finally performs an escape check: if the minted hypothesis is reachable in the result via any extractable path, the binder rejects. A promise may appear inside other neutrals — that's how spines accumulate — but never as a directly extractable value; otherwise a proof of False could leak out of its own hypothetical.

② hyp_reduce — observe through a promise. The only legal move on a hypothesis is an observation: apply it, project a field from it, eliminate it. Every observation routes here. hyp_reduce reads the promise's stored type and forwards the observation to that type's respond — a metadata field every type carries. A respond has exactly two moves, the ActionAction ::= Extend type | Reduce value — a neutral elimination either stays stuck at a type or computes to a value; the canonical normalization-by-evaluation dichotomy dichotomy: Extend T ("stuck — but I know the result's type is T") or Reduce v ("this actually computes — here's the value").

// neutral evaluation: an eliminator reaching a promise parks as a
// stuck elimination, TYPED by its motive
let hN := make_hyp Nat 0
test is_neutral (nat_rec ({_} -> Bool) true ({n, rec} -> false) hN) = true

// observations route through the stored type's respond: apply a
// function-promise and the result is stuck AT THE CODOMAIN TYPE
let hPi := make_hyp (Pi Nat ({_} -> Bool)) 0
test neutral_type (param_apply hPi zero) = Bool

Both Action arms, on one record type:

// respond has exactly two moves. Extend: stay stuck at a type.
// Reduce: compute through. A record with a derived field shows both:
let Pt := { a : Nat, b := succ a }
let hPt := make_hyp Pt 0
test neutral_type (param_apply hPt (acc "a")) = Nat
test tree_eq (param_apply hPt (acc "b")) (succ (param_apply hPt (acc "a"))) = true

This is neutral evaluation, and it is how the opening question resolves: quadruple's body runs on a promise, double's recursor reaches it and parks as a stuck elimination typed by its motive, the body finishes as a stuck tree of type Nat, the codomain matches, and the definition is accepted.

5.4 · Spines

A hypothesis's spine is the running log of how it has been observed so far. When hyp_reduce answers Extend T, the result is a new neutral whose stored type is T and whose payload records "the parent neutral, extended by this observation" — the typed shape Spine ::= Mint id | Ext parent frame. Spines let neutrals grow indefinitely without ever evaluating: apply a promise to a thousand arguments and the result is still a placeholder, just with a longer history. And since every spine-extended tree still carries the hyp_reduce signature, the walker's protections follow it everywhere.

5.5 · Three layers of soundness

The informal theorem: if param_apply T v = Ok true, then v inhabits T per T's predicate.

These carve-outs are pinned: lib/tests/soundness.test.disp asserts both what must pass and what must be refused, so a kernel change that widens the walker fails the suite.

What the kernel deliberately does not guarantee: termination of user predicates, semantic correctness of user-supplied responds (§6.4 tackles that behaviorally), or ahead-of-time detection of paradoxes. Russell-style definitions are syntactically legal and diverge under evaluation; the reduction budget catches divergence as failure, never as a proof.

Section 6Library types

Pi, Sigma, records, Bool, Nat, Eq, Type: none of these are kernel primitives. Each is a wait-forma type is wait(checker)(metadata): a deferred application whose head identifies the former and whose metadata record carries recognizer_params, respond, functor, behavioral_specs built from cells, a metadata record, and a respond — and adding a new type former is library work, not kernel surgery. Two constructions cover nearly everything.

6.1 · The telescope: the one negative former

A telescope is a dependent chain of cellsa cell is itself a wait-form `wait op meta` — inspectable (its signature says which observation) and runnable; the op is the cell's observation: mint a binder, project a field, check an application, pin a derived value, each binding a value the later cells can mention. It is the single former behind functions, pairs, records, and the trivial type:

// the surface record literal IS the library telescope former
let Point := { x : Nat, y : Nat }
let PointCells := Telescope (t (proj_cell "x" Nat) ({_x} -> t (proj_cell "y" Nat) ({_y} -> t)))
test tree_eq Point PointCells = true

// and Pi is a two-cell telescope: mint the domain, check the codomain
test param_apply (Pi Nat ({_} -> Nat)) ({n} -> n) = Ok true

One walker serves every telescope, in two modes: recognition (walk the cells, check a candidate satisfies each observation) and response (drive a stuck elimination — this is what a telescope type's respond does when hyp_reduce forwards an observation). Because both faces read the same cells, the recognizer and the respond cannot disagree about what a field is. Derived fields show the payoff — the recipe is data, so checking runs it:

// a derived field's recipe runs during the check
let TDs := { a : Nat, b := double a }
test TDs { a := 2; b := 4 } = Ok true
test TDs { a := 2; b := 5 } = Ok false

6.2 · Sums and recursion

The telescope's dual is Coproduct — a sum of per-variant telescopes, each tagged. Recursion is not a special former: a recursive constructor argument is one more cell kind (Rec), and the coproduct ties its own knot. From the cells alone, the library derives the recursor, the fold, and the functorial map — one implementation for every inductive, read off the type's structure.

// a home-made Nat: two variants, one recursive position
let MyNat := Coproduct [pair "z" [], pair "s" [Rec]]
test param_apply Type MyNat = Ok true

// its values are tagged injections
let my_zero := inj "z" []
test param_apply MyNat my_zero = Ok true

6.3 · Propositional equality

An equality type has exactly one proof value, and it is the leaf itself. Whether refl proves an equation is decided by running both sides — conversion is hash-cons identity (§2.5), so the check is cheap:

// one proof value, and it is the leaf itself
test refl = t
test (Eq Nat (double 2) 4) refl = Ok true
test (Eq Nat 3 4) refl = Ok false

// a theorem about every Nat: a Pi into a proposition
n_eq_n : {n : Nat} -> Eq Nat n n := {n} -> refl
test param_apply (Pi Nat ({n} -> Eq Nat n n)) n_eq_n = Ok true
test param_apply (Pi Nat ({n} -> Eq Nat n (succ n))) ({n} -> refl) = Ok false

6.4 · The universe checks itself

There is a single universe, and no stratification — no Type 0 : Type 1 : Type 2 tower. Membership in Type is a predicate like membership anywhere else, in two layers. The structural layer recognizes a well-formed wait-form type carrying MetaShape-conforming metadata. The behavioral layer aims the §5 promise machinery at the type itself: probes mint hypotheses and fire observations through hyp_reduce at the candidate's respond, comparing answers against the type's own constructors. A respond can lie in two directions — wave junk through, or refuse everything — and both are caught:

test param_apply Type Nat = Ok true
test param_apply Type zero = Ok false
test param_apply Type Type = Ok true

// the behavioral check: aim the promise machinery at a type's own
// respond, and catch lies in both directions
let MyNat := Coproduct [pair "z" [], pair "s" [Rec]]
let resp_of := {T} -> (type_meta T).respond (type_meta T).recognizer_params
test verify_good MyNat (resp_of MyNat) = Ok true
test verify_good MyNat (inductive_respond unit_witness) = Ok false
test verify_good MyNat (inert_respond unit_witness) = Ok false

So the checker checks the checkers, with the same two kernel operations it uses on everything else — the "self-verified" in disp's first sentence. As for Girard-style paradoxes: a Russell definition like R := {T} -> not (T T) is syntactically legal and simply diverges when run; the reduction budget reports failure, and failure proves nothing. Soundness by divergence-as-failure, not by hierarchy.

Section 7Future directions

7.1 · What has landed

The original version of this walkthrough (mid-2026) closed with a roadmap; an unusual amount of it has since shipped. The seven-primitive kernel became the two-operation kernel of §5. Telescopes and cells unified the negative formers; the coproduct + coherence-gate story covered the positives. The universe grew its behavioral layer (Type := BehavioralType) — the §6.4 self-check is landed code, not a plan. Modules became hermetic functors with explicit givens; declarations became guard-mediated requests (a name can be owned by a policy, and rebinding it demands a machine-checked license — the seed of verified optimization). Five evaluator backends sit behind one session ABI and must agree byte-for-byte, including the Rust engine this website runs in your tab. And the first end-to-end optimizer slice exists: equality witnesses licensing real rewrites (map fusion among them) past syntactic equality, with zero kernel changes.

Still design-stage: effects as a free-monad library with one impure driver at the program boundary (TYPE_THEORY.typ §15), cost as a typing-level resource, and the items below.

7.2 · Cubical type theory

Path-based equality — the source of computational univalence — appears implementable as library code over the existing kernel (TYPE_THEORY.typ §13). The interval I is a library type; a path is a function from it; and the walker's parametricity is exactly the discipline paths require (one cannot triage on an abstract i : I):

Path A x y  :=  Pi I ({_} -> A)

refl   := {A, x, i} -> x
sym    := {A, p, i} -> p (I_inv i)
funext := {A, B, h, i, a} -> h a i

Function extensionality, an axiom in intensional MLTT, drops out as a one-line definition. Transport dispatches through each type's functor metadata field — the same dispatch pattern the kernel already uses everywhere — and Glue would make univalence a theorem: equivalent types compute as equal.

7.3 · The long arc

I want to synthesize the best possible programs given a specification… turn the type checker into a function that takes a program and returns 1 or 0, combine that with functions that measure performance or program size, and somehow turn all that into a function represented purely in some low-level deterministic Turing-complete calculus. — GOALS.md

The pieces now in place: a reflective substrate (§2), a kernel small enough to trust (§5), a universe that can check its own citizens (§6.4), and licensing machinery that can say "these two programs are interchangeable, and here is the certificate". What remains is the optimizer itself — OPTIMIZER.typ designs it as verified gradient descent on a graded cost over a materialized reduction net — and the neural proposer that searches where brute force cannot. An external generator proposes candidate trees; the type checker, itself a tree, scores them; and the loop refines itself.

Section 8References

1. Schönfinkel, M. (1924). Über die Bausteine der mathematischen Logik Mathematische Annalen 92, 305–316; English translation in van Heijenoort, From Frege to Gödel, Harvard UP 1967.
2. Curry, H. B., & Feys, R. (1958). Combinatory Logic, Vol. I North-Holland. The classical reference for the combinatory calculus and bracket abstraction.
3. Howard, W. A. (1980). The formulae-as-types notion of construction In Seldin & Hindley (eds.), To H. B. Curry, 479–490, Academic Press; circulated 1969.
4. Martin-Löf, P. (1984). Intuitionistic Type Theory Sambin notes, Padua lectures 1980. Bibliopolis.
5. Scott, D. S. (1976). Data types as lattices SIAM J. Computing 5(3):522–587. The lattice-theoretic origin of the encoding now called "Scott encoding".
6. Reynolds, J. C. (1983). Types, abstraction and parametric polymorphism Information Processing 83, 513–523. The foundational paper on relational parametricity.
7. Jay, B. (2021). Reflective Programs in Tree Calculus Self-published; sources and PDFs on GitHub.
8. Cohen, C., Coquand, T., Huber, S., & Mörtberg, A. (2018). Cubical Type Theory: a constructive interpretation of the univalence axiom TYPES 2015, LIPIcs 69.
9. The Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics IAS Princeton.
10. Gordon, M., Milner, R., & Wadsworth, C. P. (1979). Edinburgh LCF: A Mechanised Logic of Computation LNCS 78, Springer. The progenitor of the small-trusted-kernel tradition that informs disp’s discipline.
11. Mac Lane, S., & Moerdijk, I. (1994). Sheaves in Geometry and Logic Springer. Standard reference for elementary topos theory and the subobject classifier.
12. Lambek, J., & Scott, P. J. (1986). Introduction to Higher Order Categorical Logic Cambridge University Press.
13. de Moura, L., et al. The Lean theorem prover & programming language
14. The Rocq Development Team The Rocq Prover (formerly Coq)
15. The Agda Team Agda — dependently typed functional programming language

Section 9Glossary

Tree calculus

An abstract rewriting system on values built from one nullary constructor (the leaf t), with binary application. The K, S, and triage rules make it Turing complete and structurally complete: every program can decide the shape of every value by reduction alone.

Triage

The F rule: a function of shape t (t c d) b dispatches on the shape of its argument (leaf, stem, or fork). The primitive reflection mechanism.

Hash-consing

Storing each distinct tree exactly once and identifying trees by integer ID. Makes structural equality — and therefore conversion checking — an O(1) identity check.

Bracket abstraction

The algorithm [x].M that removes a free variable, leaving a closed combinator expression in I, K, S. Bridges the surface λ-syntax to tree calculus.

Types-as-predicates

The design principle: a type is a tree program, and v : T iff T v = Ok true.

CheckerResult

The verdict coproduct Ok | Err. Failure is a value, not an exception in a meta-language.

Hypothesis / neutral

A kernel-minted tree of shape wait (hyp_reduce) (meta), standing for "an unknown value of stored type T". How disp checks under binders. Unforgeable and uninspectable by construction.

Signature

The identity of the function at a tree’s head, read by the sanctioned pair_fst projection. The kernel’s routing key.

Σ (the routing table)

The fixed map from pinned signatures to registered handlers. param_apply routes a pinned signature to the REGISTERED handler, ignoring anything embedded in the value — so carrying a kernel signature grants no privilege.

param_apply / the walker

The dispatcher and its policed reduction mode: the five rules minus reflective moves on hypotheses (no triage on a neutral, no forging kernel-signed forks), with reader carve-outs pair_fst, neutral_type, I, tree_eq.

bind_hyp

Kernel operation #1: mint a fresh hypothesis, run the body under the walker, then escape-check that the hypothesis does not leak out of the result.

hyp_reduce

Kernel operation #2: the single gateway for observing a hypothesis — reads the stored type and forwards the observation to that type’s respond.

respond

The metadata field through which a type answers observations on its hypotheses. Constitutive: every type carries one, and the universe checks it behaviorally.

Action

The two-armed answer of a respond: Extend type (stuck, at that type) or Reduce value (computes through). The canonical normalization-by-evaluation dichotomy.

Spine

A neutral’s payload: Mint id, or Ext parent frame — the log of observations so far. Typed, so the kernel can reason about it; still unreadable by user code.

H-rule

If the candidate is a hypothesis, compare its stored type against the required type by hash-cons identity instead of running the recognizer.

Escape check

bind_hyp’s final gate: if the minted hypothesis is reachable in the result via an extractable path, the binder rejects. Prevents hypothetical values from leaking into closed proofs.

Telescope

The one negative former: a dependent chain of cells. Pi, Sigma, records, and the trivial type are instances differing only in cell kind.

Cell

One obligation in a telescope — itself a wait-form (inspectable AND runnable). Kinds include mint (bind a ∀-hypothesis), proj (a named field), apply (a codomain check), derive (a computed field), and Rec (a recursive position).

Coproduct

The positive former: a tagged sum of per-variant telescopes. Bool, Nat, and Ord are instances (over raw shape encodings, via a view isomorphism).

Coherence gate

The η-readback check (coh_check) every inductive respond runs on its case record before issuing a stuck elimination — the respond cannot wave junk through.

Neutral evaluation

Running a program on a promise: eliminators park as stuck eliminations typed by their motives, and checking proceeds on the types of stuck things.

Path (cubical, proposed)

A function from the interval into a type; equality with computational content. Univalence becomes a theorem via Glue.

Verdict / verify_good

The behavioral universe check: probe a type’s respond with minted hypotheses and compare answers against its constructors. Catches responds that lie in either direction.

This walkthrough is pedagogical commentary. The repository's TYPE_THEORY.typ, SYNTAX.typ, and the lib/kernel/*.disp sources are the ground truth — and unlike most language documentation, the kernel sources are the theory.