Disp

1.  Motivation

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 and can be stated as a single equation:

T (v) = true   ⟺   v : T

In words: the type T applied to the value v reduces to the canonical Boolean true if and only if v inhabits T. (Following standard type-theory notation, we write v : T to mean “v has type T”, i.e. “v inhabits T”.)

In traditional type theory the relation "v has type T" is a separate kind of statement, written Γ ⊢ v : T (read: "in context Γ, the term v has type T") and derived by inference rules. Disp has no such separate machinery. Types are themselves tree-calculus programs: predicates that, run against a candidate tree, return a Boolean. Type-checking is, then, just function application on those predicates.

1.2  Why does this design exist?

The long-term aspiration, stated in GOALS.md, 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 itself over time. For that, every relevant component (the specification, the type-checker, the scoring function, the candidate programs) needs to live inside a single self-inspecting computational universe.

The mainstream proof assistants Lean [Lean], Rocq/Coq [Rocq], and Agda [Agda] have not bootstrapped their checkers into themselves, in part because those checkers accumulated dependencies on features of their implementation language (mutable hash tables, exceptions, pattern-match compilation, tactic DSLs) which have no counterpart in the language being implemented. Disp's development philosophy, in the spirit of the LCF tradition [Gordon, Milner & Wadsworth 1979] — a small, trusted kernel with everything else built on top in the language being implemented — aims to avoid that drift from the start.

"The object language is the specification. Host implementations are optimizations. Every component that participates in deciding well-typedness — the type checker, the elaborator's semantics, conversion, the data structures those components read — must have a declared encoding as a tree-calculus program. The TypeScript implementation exists to make iteration fast. It is never the ground truth." — DEVELOPMENT_PHILOSOPHY.md:11–13

Reach that point and the type checker becomes synthesizable by the same machinery that uses it. The architectural commitments it forces — small kernel, predicates as types, metacircular checker — shape the rest of the document.

2.  From λ-calculus to Trees

We start with the untyped λ-calculus — the minimal language of functions. Its terms are

M, N  ::=  x  |  λx. M  |  M N

and the single computation rule is β-reduction, (λx. M) N →_β M[x ≔ N]. This is Turing complete, but it has a property that becomes inconvenient when building a fully reflective language: λ-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 [Schönfinkel 1924][Curry & Feys 1958] observed that one can dispense with bound variables entirely using three combinators:

SKI is combinatorially complete: every λ-term has an equivalent SKI translation (the algorithm is called bracket abstraction). 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 [Jay 2021], is an alternative combinatory calculus in which every value is a tree built from three node shapes, and one of the reduction rules pattern-matches on those shapes. There is exactly one base piece — call it △, a triangle, the "leaf" — and trees are assembled by writing pieces next to each other (juxtaposition). Every tree is therefore one of:

△       (leaf, arity 0)
△ u      (stem, arity 1, holds one child)
△ u v     (fork, arity 2, holds two children)

Application is not a syntactic constructor; it's an external operation apply : Tree × Tree → Tree. Trees by themselves are already in normal form; reduction only happens through apply.

2.3  The reduction rules

The five rules of apply(f, x) partition by the shape of f (and, in the F-rule, also by the shape of x). Read each row as: if f matches the pattern in the left column, then apply(f, x) reduces to the result column.

The first two rules (L and s) are passive: they just build larger trees when no reduction can fire. K and S match their SKI counterparts. The fifth rule — F — is the new ingredient: it's the only rule whose behavior depends on the shape of the argument. A program of shape △ (△ c d) b is, operationally, a case analysis on the structure of its argument. Reduction itself can inspect tree shape. (The widget below labels each firing with its rule letter: K, S, F, L, or s.)

To get a better sense of the tree calculus in action, the widget below evaluates any expression you type — press Step to fire the next reduction, and watch the rule letter (K, S, F, L, or s) appear on each redex as it becomes ready.

2.4  Bracket abstraction: compiling λ to trees

Tree calculus, like SKI, admits a translation that eliminates binders. Given a λ-term M and a variable x, the operation [x].M ("abstract x out of M") produces a closed expression built only from I, K, S, and application, such that applying the result to any tree v behaves like M with v substituted for x. Three base rules suffice:

This is just structural recursion on M. For nested binders λx.λy.M, peel them off inside-out: first compute [y].M, then abstract x from the result.

A small example

Take the term λx. λy. y (a constant function that always returns its second argument):

[x]. [y]. y  =  [x]. I  =  K I

The first step uses the variable rule ([y].y = I). The second step uses the constant rule (x doesn't appear in I, so we get K I). The output K I is a closed tree — substituting the tree representations of K and I gives a specific tree shape, and applying that tree to any two arguments recovers the second.

The three combinators as trees

The combinators I, K, S are themselves particular trees:

I  =  △ (△ △ △) △     K  =  △ △     S  =  △ (△ (△ △ △)) △

You can check, from the reduction rules of §2.3, that these tree shapes do what the names say: I v reduces to v (because the leaf/stem rules construct a stem, and the fork shape of I hits the F-rule whose leaf-branch is the identity), and similarly for K, S.

Two practical optimizations

Applied naively, the three rules above produce huge terms. S appears at every application node, even when one or both subterms don't mention x. Disp's compiler (src/compile.ts:77–102) recognizes two redex shapes that arise from the naive rules and rewrites them at compile time:

• η-reductionthe identity λx.(f x) = f when x is not free in f; the application and the bound variable cancel.. If M = N x and x is not free in N, then [x].(N x) = N. The naive rule would give S (K N) I, but that reduces to N for every argument, so we may as well emit N directly.
• K-composition. If both subterms of an application abstracted to K p and K q respectively — i.e., neither used x — then S (K p) (K q) reduces (for every argument) to K (p q). The compiler collapses it eagerly.

Both rules preserve semantics and substantially shrink the output. So every λ-term in Disp's surface syntax becomes, after bracket abstraction, a closed tree. The runtime has no free variables; binders are compiled away. This is what makes the equation "types are tree programs" coherent: the surface notation {x} -> body is sugar that compilation eliminates; once compilation finishes there is nothing in the runtime that is not a tree.

2.5  Hash-consing and O(1) equality

One implementation detail is essential for what follows. Disp's tree runtime stores every distinct tree exactly once: when fork(l, r) is invoked twice with the same children (as identified by their integer ids), the second call returns the same node as the first (src/tree.ts:26–48). This is hash-consingstructural sharing: identical subtrees share one heap cell, so structural equality collapses to integer-identity comparison.. The consequence is that structural equality reduces to identity:

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. Making conversion O(1) keeps type-checking cheap. It also makes the kernel's H-rule (introduced in §5.3) tractable: the H-rule decides "the stored type of this hypothesis equals the type reconstructed from these parameters" by hashed identity, given that deterministic elaboration produces identical trees for identical types.

3.  A first look at Disp source

Before turning to the type system, a short tour of the surface syntax. The notation is small, and from §4 onward we will read it constantly, so it pays to nail down what the symbols mean. The grammar is fully specified in SYNTAX.typ; what follows is the part you need for the rest of the document.

3.1  Binders, application, and the leaf

Lambda abstraction uses braces, not λ:

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

Annotations are informational; the compiler does not check them against an inferred type. The elaborator just lowers {x} -> body by running the bracket abstraction of §2.4. By the time anything reaches the runtime, the binder is gone and you have a closed combinator tree.

Application is juxtaposition, left-associative as in λ-calculus: f g x means ((f g) x). Parentheses regroup.

The literal t denotes the leaf △. So t is the leaf, (t t) is the stem △ △, (t t t) is the fork △ △ △, and arbitrary trees nest from there. This is the only "literal" the language has — everything else is built by application.

Other files come in with open use "path/to/file.disp" at the top of a source file; we'll see this from §6 onward when library types start importing each other.

3.2  Definitions and tests

A top-level definition uses :=. The left side is a name; the right side is any expression. With an optional :-annotation:

// untyped
I := {x} -> x
K := {x, y} -> x

// typed (the type is itself an expression — typically a Pi, i.e. a
// dependent function type; introduced properly in §5.1)
id : {A : Type} -> A -> A
   := {A} -> {x} -> x

The id example reads: "for any type A, a function from A to A." The {A : Type} on the left of the := is a type-level binder (Pi); the {A} on the right is the matching term-level binder. Type, the universe, is defined in §6.4.

A test is a compile-time obligation: parse both sides, reduce, demand structural equality.

test I t = t
test ({x, y} -> x) t (t t) = t

If the equation does not hold, compilation fails. Tests are how the library asserts properties of definitions; they are also how the type-checking itself is exercised at compile time. A test like

test (Nat) t = true

asserts that Nat applied to t (the leaf, which encodes zero) reduces to true — i.e., that t inhabits Nat. This is the central equation of §4 in executable form. (We define Nat in §6.1; the example anticipates it.)

3.3  Pattern matching

The match form dispatches on a value via its own eliminator (Scott-encoded; see §4.2):

not := {b} -> match b {
  true  => false
  false => true
}

The arms desugar to applications of the matched value as its own eliminator — a function that takes one branch per shape the value can have, and returns the chosen branch. §4.2 makes this precise for Booleans. For non-Boolean datatypes the same mechanism works: each arm corresponds to one constructor of the type, and the elaborator threads the binders through.

4.  Types as Predicates

4.1  Propositions, predicates, and Curry–Howard [Howard 1980]

Four traditions each give a different reading of what "T" and "v : T" mean. The structural shape is the same; what differs is which objects are primitive and what the relation is:

Disp's row is the closest to the predicate-logic row — the structural shape is identical, with function application playing the role of evaluating a formula at an assignment. The Curry–Howard correspondence (the MLTT row) is the observation that propositions correspond to types and proofs correspond to inhabitants; we'll borrow its vocabulary informally throughout, but Disp's machinery is closer to "decidable predicate evaluation" than to "proof derivation in a deductive system."

The load-bearing difference between Disp and the other three rows is that 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 the kernel's apply. That is what makes the type-checker writable as a tree program rather than as an external interpreter.

T : Tree → Bool,   v : T  ⟺  T(v) reduces to true

4.2  Booleans as functions: the Scott encoding

To make T(v) = true a literal equation, Disp encodes Booleans not as opaque values but as their own eliminators. The encoding is Scott-style [Scott 1976]: a Boolean is a function that takes two branches and returns the appropriate one (lib/prelude.disp:19–20):

// doc convention; the codebase spells these TT/FF and includes a motive parameter
true  := {then_branch, else_branch} -> then_branch
false := {then_branch, else_branch} -> else_branch

After bracket abstraction these compile to specific trees: true = K K and false = K (K I). A conditional is then just an application:

select := {cond, then_branch, else_branch} -> cond then_branch else_branch

If cond is true, it selects then_branch; if false, else_branch. There is no if-keyword and no opcode; conditional dispatch is just Scott dispatch.

4.3  The central equation, in code

Suppose Nat is some tree (a predicate on trees). To check that 0 has type Nat, we apply:

Nat 0   ⇝   evaluates to true or false

That's it: no typing context to maintain, no judgement to derive; the type checker is just reduction.

To make it concrete: ask "does the leaf t inhabit Nat?" — i.e., does Nat t reduce to true? Anticipating §6.1's definition, Nat's recognizer says: a tree is a Nat if it is the leaf, or a fork whose left child is a leaf and whose right child is itself a Nat. Apply it:

Nat t
⇝  (predicate-framed nat_recognizer) t
⇝  nat_recognizer (t t t) t            // frame routes through to the recognizer
⇝  match (is_leaf t) { true => true; … }
⇝  true

That is the entire type-check for t : Nat. No context, no judgement; an apply and four reductions. The §6 widget will do this at scale, with hypothesis handling layered on. First, though, one real complication: what happens when v is not a closed value like t but a variable bound by some surrounding lambda?

5.  The Seven Kernel Primitives

5.1  The hypothesis problem

Consider f := {x} -> x, the identity function, and ask: does f have type Pi Nat ({n} -> Nat)Pi A B is the dependent function type: a value f inhabits it when f(x) inhabits B(x) for every x : A. Defined as library code in §6.2.? Following the central equation, this becomes: evaluate (Pi Nat ({n} -> Nat)) f and check the result is true. To verify that f produces a Nat for every input, we need some way to range over all possible inputs.

The usual approach in dependent type theory is to introduce a variable x : Nat in the typing context (the Γ that §1.1 was contrasting against) and check f x : Nat under that hypothesis. Disp doesn't have a typing context as a separate object, but it has to solve the same problem operationally.

Operationally we want a single placeholder we can pass to f that behaves like an unknown Nat. Three properties are needed: (i) it carries its declared type, so later checks can look that up; (ii) it has a fresh identity, so we can tell two distinct placeholders apart; (iii) user code, running against it, cannot peek at any of this. Build such a thing and feed it to f, and "does f always return a Nat?" becomes a single concrete reduction.

The kernel mints this placeholder — called a neutral or hypothesis — as a specific tree shape:

Hyp Nat id  =  wait(kernel.hyp_reduce)(neutral_meta)

Read it piece by piece. kernel.hyp_reduce is the kernel handler that fires when something tries to use this placeholder by applying it to an argument (§5.3 ②). waitwait f x y reduces to f x y, but wait f x by itself does not evaluate f x. It lets us write a tree whose head is kernel.hyp_reduce without that head firing until a third argument arrives. defers that firing until the hypothesis is actually applied — without it, the handler would fire on neutral_meta immediately and there would be no placeholder to pass around. The neutral_meta is the payload: it packages the stored type (here Nat), a unique identifier, and a spinea record of how the hypothesis has been applied so far: when h is applied to arg, the new hypothesis remembers the chain h · arg. Spines are how neutrals stay neutral under further application. (a running log of how the hypothesis has been applied so far; explained in §5.4). The whole tree's signature — kernel-speak for "what function sits at the head" — is kernel.hyp_reduce. Signatures are the routing keys the kernel uses below.

5.2  The parametric walker

The kernel handles the soundness threat by partitioning all apply calls into two modes:

• Raw mode. The five reduction rules as written above. Used inside the kernel, where full visibility into hypothesis structure is needed.
• Parametric mode, also called the walker. The same five rules, but with two restrictions. (i) The F-rule (triage) refuses to fire when its argument is rooted at a kernel-minted hypothesis — concretely, the triage returns false, as if the recognizer had said "no". (ii) The stem-rule (rule 2 in §2.3), which normally builds a fork by snapping a stem onto an argument, is blocked when the resulting fork would have the head signature of a kernel-minted neutral. This prevents user code from forging fake hypotheses.

The walker enforces operational parametricity: user code, running under the walker, cannot examine the structure of a hypothesis and cannot forge new ones. From the user's perspective, a hypothesis behaves like an opaque universally quantified value. The mode-switching is invisible to the user, and it's what makes "f(h) type-checks for a fresh h" mean the same thing as "f is correct on all inputs."

5.3  The seven primitives

The seven handlers fall into three families. Dispatch routes every application either to a kernel handler (raw mode) or to the walker (parametric mode). Frames wrap a user-supplied recognizer or eliminator with the kernel's hypothesis-handling rule. Boundary mediates the public/internal seam.

Why seven? Four are forced by the type-checker shape (checked_apply, hyp_reduce, predicate_frame, eliminator_frame); two by the boundary discipline (guard, unguard); the seventh, bind_hyp, is privileged for the escape-check's reliance on raw reduction and could in principle become library code. The count is engineering, not numerology.

Dispatch

① checked_apply: the dispatcher. Every application apply(f, x) in user code goes through checked_apply. It inspects the signature of f's head; if the signature matches one of the seven handlers, the handler runs in raw mode; otherwise the walker takes over. This is the privilege boundary: kernel handlers are raw-privileged, user code is parametric.

② hyp_reduce: applying a hypothesis. If h is a hypothesis of stored type T, what does h(arg) mean? The kernel consults T's metadata for a codomain function, which returns an Action: conceptually the sum type

Action  ::=  Extend(T)  |  Return(v)

where Extend(T) means "the result is a new hypothesis of type T" and Return(v) means "the result is the concrete value v." For example, the codomain function inside Pi (lib/types/pi.disp:34–40) extracts the body B from Pi's metadata and returns Extend(B arg): when the kernel evaluates h(arg) for h : Pi Nat ({n} -> Nat), hyp_reduce calls Pi's codomain_fn, gets back Extend(Nat), and constructs a new hypothesis with stored type Nat and spine extended by arg. Spines (§5.4) are how the kernel grows neutrals without hard-coding a notion of "function application."

Frames

③ predicate_frame: the H-rule. This is the engine of type-checking for inductive and predicate types. It wraps a user-supplied recognizer with a special case for hypothesis inputs: if the candidate v is a hypothesis, don't run the recognizer; instead, compare v's stored type against the type reconstructed from this predicate's metadata. The reconstruction is mechanical: from the predicate's stored parameters and a reference to itself, it rebuilds the same tree the type-former would have produced. This is the H-rule (hypothesis rule). It is sound because hash-consing makes "reconstructed type" and "stored type" comparable via O(1) identity, so the comparison is exact and total.

④ eliminator_frame: induction on hypotheses. The dual of predicate_frame. Recognizers check membership; eliminators destruct. If the target of an eliminator is a hypothesis, we can't pattern-match on it: we don't know which constructor it is. Instead, eliminator_frame mints a stuck neutral — structurally identical to an ordinary hypothesis (same kernel.hyp_reduce signature), with stored type motive target and identity target. The stuck mint is one of two branches the handler picks between: if the target is a hypothesis, mint the stuck; if the target is concrete, the dispatcher fires and reduces to a value. The stuck branch does not get "unstuck" later — it persists for the rest of the checking pass that minted it, carrying the derived type motive target so further checks have something to reason against. Different invocations of the same eliminator against concrete targets independently run the dispatcher.

⑤ bind_hyp: binders that mint hypotheses. The mechanism by which dependent types like Pi A B verify "for all x : A, the body holds." bind_hyp mints a fresh hypothesis of domain type A, runs the body with it, then performs an escape check: if the body's result contains the minted hypothesis via any non-neutral path, bind_hyp rejects (handlers.disp:188–214). The escape check is what prevents the bound variable from leaking into a closed proof.

Boundary

⑥ guard: the public boundary. Every published type-former wraps its predicate in guard. When a user invokes the predicate at the boundary (i.e., writes T v at top level), guard first scans the candidate v for pre-existing kernel-minted neutrals. If v contains a stray hypothesis, guard rejects with false before evaluating the predicate. This closes the smuggling attack: hypotheses cannot leak across the public boundary into closed proofs.

⑦ unguard: the trusted peel. Library code sometimes needs to unwrap a guarded type to access its inner predicate (for example, to compose a new type-former from existing ones). Doing this naively would re-trigger the walker's restrictions. unguard performs the peel in raw mode, recognized by signature and dispatched safely.

5.4  Spines

A hypothesis's spine is the running log of how it has been applied so far. When the kernel evaluates h(arg) and h's codomain function returns Extend(B) (§5.3 ②), the result is a new hypothesis whose stored type is B and whose spine is h's spine extended by arg. Spines let the kernel grow neutrals indefinitely without ever evaluating them: a hypothesis can be applied to a thousand arguments, and the result is still just a placeholder — only with a longer history. They are also what makes the walker's "no triage on a hypothesis" rule total: every spine-extended tree still has signature kernel.hyp_reduce, so the walker still recognizes it.

5.5  Three layers of soundness

The kernel's soundness theorem, informally: if T(v) = true evaluates at the public boundary, then v inhabits T per T's predicate. The two attacks anticipated in §5.1's warn-box are blocked by three runtime mechanisms; the mapping is:

One soundness carve-out: the polymorphic identity I reduces against any argument, including hypotheses. This is necessary because the identity-function type Pi Type ({A} -> Pi A ({x} -> A)) needs to be inhabited.

What the kernel deliberately does not guarantee: termination of user predicates, semantic correctness of user-supplied recognizers, detection of paradoxical type definitions. Those responsibilities sit with the library author. Russell-style paradoxes are well-formed syntactically but diverge under evaluation; the apply budget catches divergence as failure rather than synthesizing a proof of False. We return to a concrete example (R := {T} -> not (T T); R R) when discussing the universe in §6.4.

6.  Library Types

Pi, Bool, Nat, Eq, Type, Ord, Sigma: none of these are kernel primitives. They are library definitions built from predicate_frame and eliminator_frame with type-specific recognizers and codomain functions. Adding a new library type does not grow the kernel.

6.1  Bool and Nat

The recognizer for Bool is one line: a tree is a Bool if it equals true or false.

let bool_recognizer = {_, v} -> or (tree_eq v true) (tree_eq v false)
Bool := guard (predicate_frame_form (bool_recognizer, /* metadata */))

(predicate_frame_form is the constructor that builds a tree routed through handler ⑤ — its head signature is kernel.predicate_frame, so any application to it dispatches there. The "metadata" slot — (t t t) in the codebase — is a fork-shaped placeholder; for primitive recognizers without parameters it carries no information.) When applied to a hypothesis h, the H-rule inside predicate_frame bypasses the recognizer and structurally compares stored type against reconstructed type. Bool is library code; the kernel has never heard of it.

Natural numbers (lib/types/nat.disp:14–26) use a recursive predicate. We show this one in full because the recursion is the interesting part — the self-call goes through predicate_frame_form, so when it encounters a sub-hypothesis the H-rule fires:

let nat_recognizer = fix ({self_recog, params, v} -> {
  let nat_inner = predicate_frame_form (t self_recog (t t t))
  match (is_leaf v) {
    true => true                                   // zero is △
    false => match (is_fork v) {
      true => and (is_leaf (fst v))
                (nat_inner (snd v))           // succ n = fork(△, n)
      false => false
    }
  }
})
Nat := guard (predicate_frame_form (t nat_recognizer (t t t)))

Reading the body: nat_recognizer is a fixed point (the outer fix). Inside, nat_inner is the recognizer's self-reference wrapped back into a predicate_frame_form tree — that's the recursive call. The two matches decide: leaf → zero, fork-with-leaf-left → successor (recurse on the right child), anything else → not a Nat. So a Nat is either a leaf (zero) or a fork whose left is a leaf and whose right is a Nat.

6.2  Dependent functions

The Pi type-former is library code that uses bind_hyp to mint a hypothesis and run the body. The recognizer alone tells the story:

let pi_recognizer = {(A, B), v} ->
  bind_hyp A ({hyp} -> B hyp (v hyp))

Reading: to check that v : Pi A B, mint a fresh hypothesis hyp : A, apply v to it, then check the result against the codomain B(hyp). This is the standard rule for dependent function types, but here it is library code rather than kernel code. The full definition wraps the recognizer in predicate_frame_form with metadata (A, B, pi_codomain_fn) and then guard.

6.3  Propositional equality

A proof of Eq A x y is the leaf △ (canonical reflexivity), and it is only valid when x and y are identical trees — the O(1) hash-consed equality check:

refl := t        // the leaf △ is the canonical proof of reflexivity

let eq_recognizer = {(A, x, y), proof} ->
  and (tree_eq proof refl) (tree_eq x y)

Eq := {A, x, y} -> guard (predicate_frame_form (eq_recognizer, (A, x, y)))

The eliminator eq_J follows the standard Martin-Löf pattern, implemented via eliminator_frame.

6.4  The universe

There is a single universe Type; Disp does not stratify universes. This is unusual — Lean, Coq, and Agda all use a hierarchy Type 0 : Type 1 : Type 2 : … to block Girard's paradox: the type-theoretic version of "the set of all sets that don't contain themselves", which derives a contradiction from unrestricted self-reference at the type level. Disp instead accepts that such paradoxical definitions are syntactically legal and relies on a runtime budget to catch them as divergence.

A value inhabits Type iff it is structurally a published type-former, i.e., a guard-wrapped predicate_frame with well-formed metadata (lib/types/type.disp:71–96):

let type_recognizer = {_, v} ->
  match (has_sig kernel_ref.guard v) {
    true => match (has_sig kernel_ref.predicate_frame (type_meta v)) {
      true => type_metadata_well_formed (type_meta (type_meta v))
      false => false
    }
    false => false
  }

Without stratification, paradoxical definitions exist as syntactic objects but diverge under evaluation. The Russell-style culprit from §5.5 — R := {T} -> not (T T); R R — simply loops, and the runtime's apply-budget catches the loop as failure. Soundness is achieved by divergence-as-failure rather than by Tarski-style hierarchy. The tradeoff is that one cannot decide ahead of time whether a given program will be caught by the budget. Strengthening the Type recognizer to validate type metadata more aggressively is still pending.

7.  Future Directions

7.1  Categorical foundations

CATEGORY_THEORY_FOUNDATIONS_PROPOSAL.typ argues that the existing seven-primitive design is already a faithful implementation of standard categorical machinery; the proposal is to make this implicit structure explicit by giving types to the type-former metadata. A type's three metadata slots correspond to:

• Recognizer  ↔  a characteristic morphism χ_T : Tree → Ω into the subobject classifier (with Ω = Bool).
• Codomain_fn  ↔  the evaluation morphism of a locally cartesian closed categorya category with a terminal object, pullbacks, and right adjoints to pullback functors; the natural categorical home of dependent type theory. [Lambek & Scott 1986] (LCCC), or the membership relation of a topos.
• Comp_fn (proposed, cubical)  ↔  the morphism action of a functor between ∞-groupoids.

The proposal refactors the opaque 3-tuple into a typed record TypeFormer with named fields, so that library authors must construct identity and composition laws as propositional proofs. Functoriality would then be enforced by the kernel rather than left as an informal commitment.

7.2  Cubical type theory and univalence

The two cubical proposals (CUBICAL_PROPOSAL.typ and the introductory CUBICAL_TYPE_THEORY_FOR_DUMMIES.typ) argue that the move from MLTT-style propositional equality to path-based equality [Cohen et al. 2018] (the source of computational univalence [Univalent Foundations Program 2013]) can be implemented as library code over the existing seven primitives. No new kernel work appears to be required.

The interval and paths

I is a library type whose values form the free De Morgan algebra on two constants I_zero and I_one with operations I_and, I_or, I_inv. It is not Boolean: i I_or (I_inv i) ≠ I_one in general, which preserves the continuous interpretation. Disp's walker already enforces the parametricity discipline that paths require: one cannot triage on an abstract i : I.

Paths are then just dependent functions from the interval (the {_} is an unused binder; the codomain doesn't depend on which point of the interval we picked):

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

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

Function extensionality, which requires an axiom in intensional MLTT, drops out as a one-line definition. The endpoints x, y in Path A x y are documentation only; they are recovered by applying the path to I_zero and I_one.

Transport, composition, and Glue

Transport, transp P x : P I_one given x : P I_zero, is implemented by dispatch: each type-former supplies a transp_fn slot. Discrete types (Bool, Nat) use identity; pairs recurse; Pis use the standard contravariant/covariant scheme.

The Glue type-former is the construction that makes univalence compute. Glue B φ T e is "almost B, but with faces specified by φ replaced by T via the equivalence e." Its transp_fn recognizes ua-shaped paths and applies the stored equivalence directly:

ua : (A ≈ B) -> Path Type A B
ua := {A, B, e, i} -> Glue B (i I_or (I_inv i)) A e

So transp (ua not_equiv) true evaluates to not_equiv.forward true = not true = false. Univalence is a definable operation in this design, not an axiom: equivalent types compute as equal.

7.3  The long arc: synthesis and bootstrap

The final motivation, from GOALS.md:

"I want to synthesize the best possible programs given a specification... Turn 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:5–6

Once the kernel is small enough to live inside its own object language, and once enough mathematical structure (categorical, cubical) has been defined in library code, the prerequisites for neural-guided synthesis are in place: an external optimizer generates candidate trees, the type-checker (itself a tree) scores them, and the loop refines itself. The path, as currently sketched:

1. Tree calculus (done) provides a Turing-complete, reflective substrate.
2. Seven-primitive kernel (done) lifts dependent types into library code.
3. Categorical typing (proposed) makes library structure mathematically legible.
4. Cubical extensions (proposed) give univalence and HITs (higher inductive types) without axioms.
5. Self-hosting checker (in progress) closes the metacircular loop.
6. Optimizer-as-tree-program (future) enables self-improving synthesis.

8.  References

External works referenced in the text, with direct links where the canonical source is freely available. Where no open PDF is available, the entry lists the publisher of record. Each entry ends with a ↩ arrow that jumps back to the citation point in the body.

9.  Glossary

Tree calculus.

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

Triage.

The third reduction rule of tree calculus: a function of shape △ (△ c d) b dispatches on the shape of its argument (leaf, stem, or fork). Triage is the primitive reflection mechanism.

Hash-consing.

The implementation technique of storing each distinct tree exactly once and identifying trees by integer ID. Makes structural equality an O(1) identity check.

Bracket abstraction.

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

Types-as-predicates.

Disp's design principle: a type is a tree-program T : Tree → Bool, and v : T iff T(v) = true.

Scott encoding.

Encoding a data type as its own eliminator: a Boolean is a 3-argument function that selects one of its branches. Removes the need for primitive case opcodes.

Neutral / hypothesis.

A kernel-minted tree of shape wait(kernel.hyp_reduce)(meta) standing for "an unknown value of stored type T." Used to type-check under binders.

Parametric walker.

The user-mode reduction discipline. The five reduction rules with two restrictions: no triage on a hypothesis, and no stem-rule fabrication of a fork whose head matches a kernel-minted neutral signature.

Raw mode.

The five reduction rules without restrictions. Privileged: kernel handlers run in raw mode.

Action protocol.

Tagged return values Extend(B) / Return(v) from a type's codomain function. Let the kernel evaluate hypothesis applications without knowing the type's internal structure.

H-rule (hypothesis rule).

The rule inside predicate_frame: if the candidate is a hypothesis, compare reconstructed type against stored type rather than running the recognizer. Sound because hash-consing makes reconstruction-equal-stored an O(1) identity check.

Stuck neutral.

A neutral produced by eliminator_frame when an eliminator's target is a hypothesis. Stored type is the motive applied to the target; payload is the original target.

Escape check.

The check performed by bind_hyp on its body's result: if the minted hypothesis is reachable via any non-neutral path, the binder rejects. Prevents hypothesis leakage from closed proofs.

Guard scan.

The public-boundary check inside guard: rejects candidates containing pre-existing kernel-minted neutrals. Closes the "smuggle a hypothesis" soundness attack.

Path.

(Cubical, proposed.) A dependent function Pi I ({_} -> A) from the interval into a type. Endpoints recovered by applying the path to I_zero and I_one.

Glue.

(Cubical, proposed.) A type former whose values encode equivalences directly. Its transport rule applies the stored equivalence, giving univalence computational content.

Univalence.

The principle that equivalent types are equal. In Disp's cubical extension this becomes a theorem, not an axiom, because the ua path is constructed using Glue with computational transport behavior.