sail-judge · GAT spike · 2026-07-13 · a discussion opener for Aaron Steven White, companion to Bandits, Recapped and The Full Map
Role choice and arm choice look like two mechanisms bolted together. Written down as a Generalized Algebraic Theory, they aren't two mechanisms at all — and the way they aren't is precise enough to hand to someone who actually does this for a living.
The spike question, verbatim
Short answer first, because it isn't the tidy one either side of that question expects: the duality doesn't dissolve into an unstructured single thing, because it was never a free product of two independent factors to begin with. Once sail-judge's actual running code is written down as a Generalized Algebraic Theory (Cartmell, 1986), role and arm turn out to already be a dependent pair — a discrete fibration, arm indexed by role — and that fibration is the one natural entity. "Role, then arm" is how a term of that one sort gets built, in two stages, not two mechanisms glued together after the fact.
The mechanism, as actually coded
Traced directly from ~/haiku.garden/scripts/chatto-realtime-demo/sail-judge.mjs, not from memory. Role is a deterministic guard cascade — no bandit involved — over two live counters on the conversation:
if (msgsSinceQuestion ≥ ASK_AFTER_NO_QUESTION) role = asker else if (msgsSinceReply ≥ SPEAK_EVERY) role = discourseDriver else (no role fires this turn)
Only once a role fires does a bandit choose among that role's own arm vocabulary — Thompson sampling over an independent Beta-Bernoulli posterior:
| Role | Arm vocabulary |
|---|---|
| asker | generation-effect, retrieval-practice, metacognitive-calibration bandit-competitive + desirable-difficulty fixed schedule, every 4th fire, unscored |
| discourseDriver | marking-critical-features, reduction-in-degrees-of-freedom, direction-maintenance |
Easy to miss without reading the code: these two arm sets are disjoint. Two separate object literals, two separately-seeded posteriors, persisted as two top-level keys. There is no arm value that is even well-formed for both roles — writing arm = retrieval-practice already means role = asker. Arm was never a free-standing second choice sitting beside role in a product space; it is already role-indexed in the code as it stands today, just not written down that way.
The GAT
A Generalized Algebraic Theory is a signature — some of its sorts dependent, meaning a sort can be indexed by a prior term of another sort. B(x) for x : A is exactly a family of sorts over A; in categorical semantics this is a fibration, p : (Σa:A B(a)) → A, whose fiber over each a is B(a).
The piece left in prose above — what decides which Role term fires — becomes two priority-ordered introduction rules over a sort RoomState with operations msgsSinceQuestion, msgsSinceReply : RoomState → Nat and constants ASK_AFTER_NO_QUESTION, SPEAK_EVERY : Nat:
Γ ⊢ s : RoomState msgsSinceQuestion(s) ≥ ASK_AFTER_NO_QUESTION ————————————————————————————————————————————— (asker-intro) Γ ⊢ fires(s) : Role [fires(s) ≡ asker] Γ ⊢ s : RoomState msgsSinceQuestion(s) < ASK_AFTER_NO_QUESTION msgsSinceReply(s) ≥ SPEAK_EVERY ————————————————————————————————————————————— (driver-intro) Γ ⊢ fires(s) : Role [fires(s) ≡ discourseDriver]
driver-intro's guard carries asker-intro's guard negated, verbatim, as part of its own side-condition — not a tie-break bolted on after the fact. That inclusion is what makes "asker wins ties" a derived fact about the theory rather than a prose note about if/else if ordering. And if neither guard holds, fires(s) is simply undefined at s: the silent no-op branch sits outside the sort, not as a third term with an empty fiber.
The dependent sort Arm(r : Role) then reproduces the table above exactly: Arm(asker) has four terms, Arm(discourseDriver) has three, and Arm(asker) ∩ Arm(discourseDriver) = ∅ — a discrete fibration, no term of the total Arm sort living in two fibers at once. One level further down, inside the Arm(asker) fiber alone, the scheduled desirable-difficulty override is two more term-forming rules targeting that same dependent sort — one deterministic-scheduled, one stochastic — and both still respect the fibration exactly, since neither conclusion can land in Arm(discourseDriver):
Γ ⊢ fires(s) ≡ asker askerFireCount(s) mod DESIRABLE_DIFFICULTY_EVERY = 0 —————————————————————————————————————————————————— (scheduled-override) Γ ⊢ arm(s) : Arm(asker) [arm(s) ≡ desirable-difficulty] Γ ⊢ fires(s) ≡ asker askerFireCount(s) mod DESIRABLE_DIFFICULTY_EVERY ≠ 0 —————————————————————————————————————————————————— (bandit-draw) Γ ⊢ arm(s) : Arm(asker) [arm(s) ≡ bandits.asker.choose()]
That a scheduled override and a stochastic bandit draw both stay confined to one fiber, never spilling into the other, is itself evidence the fibration carries real structural weight — not just a description of the top-level role split.
Move := Σr : Role Arm(r). A term of Move is a pair (r, a) with a : Arm(r): you cannot construct one without committing to r first, and committing to r immediately restricts which a are even typeable.
That is the fusion the intuition behind the spike question was reaching for. Under the correct type discipline, "role choice" and "arm choice" were never two independent mechanisms composed afterward — they are the base-projection and fiber-selection of constructing one term of one sort, in two stages. The two-bandit-objects, two-if-branch shape of the actual JS is a presentation choice, not a semantic claim that two separate mechanisms exist.
projection p : Move → Role. Each fiber is reachable only through its own base point — the two clusters never touch.
What a morphism is forced to preserve
A morphism between GATs — equivalently, a Cartesian/fibered functor over the base — has to send Role to a target base sort, and the whole dependent family Arm(-), not its flattened union, to a target family, respecting fibers: for each r, it restricts to a map Arm(r) → Arm′(F(r)). It can rename roles, relabel or even merge/split fibers — but it cannot flatten Role × Arm into an unstructured product and permute freely across that flattening, because that is a map of a strictly weaker theory: a plain product, which is what "role and arm are two separate mechanisms" secretly assumes.
So the natural properties of the fused entity — what any legitimate morphism out of this theory has to respect — are:
(|Arm(asker)| = 3+1, |Arm(discourseDriver)| = 3).Move factors as P(a | r)·P(r) with zero cross-terms. A direct consequence of discreteness, not a separate design decision — and falsifiable: if discourseDriver's arm draws ever turn out to statistically depend on asker's recent arm history, that's the fibration leaking, worth one real pass over sail-judge-events.jsonl before assuming it holds.One more thread, briefly
sail-i9j3 already settled the practical direction for roles themselves — mine them from real behavioral data (tab's firehose records on trullala, the haiku-community Bluesky scan) rather than hand-invent them, distilled offline into a fast runtime classifier. That distillation step needs two signatures and one morphism between them, not one: a slow, human-curated SlowTheory (a Card sort, a dependent Connection(c₁ c₂ : Card) sort — exactly Semble's own Connection object, typed and directional between two actual cards), and the live FastTheory already described above (Role, Arm(r), Move), extended with one new dependent sort, PersonaHint(m : Move) — indexed by Move for the same reason Arm is indexed by Role.
Distill : SlowTheory → FastTheory is the morphism connecting them, computed offline once; what it adds over treating this as a bare ML pipeline is that "is the distillation still faithful to the real data" becomes a checkable morphism law — does Distill commute with Connection's own dependency on two distinct cards — rather than only an eval metric with no structural guarantee. Full account in 2026-07-13-persona-role-arm-gat-spike.md §4; not repeated here since the point of this page is the fibration above, and this is only the pointer to where it leads next.
Where this is actually headed
a first pass, not a finished account reacting to it is the ask
sail-oj4n named the real prerequisite for lens-mapped reward-proxy observability as GAT expertise, not an improvised reading of the GATlab paper — and named Aaron Steven White (factslab.io, GAT schema lead on AIDLE) as the person who actually has it. This page is that spike's first real pass at making the practical question — is PersonaHint the right dependent sort, does Distill even typecheck the way sketched — something to argue with, rather than a paragraph asking whether panproto has anything to offer.
the fibration above is the whole content of this page; everything past §4's pointer is still open, on purpose, for whoever reads it next.