BANG — language reference

Derived from the code through the schema-validated docfacts/language.json bundle; every example is a #guard gated by lake build, so nothing here can drift from what the language actually does.

Surface syntax

Types

Grammar

GENERATED from the reified parser tables in Bang/Frontend/Surface.lean (ADR-0071): operator precedence from opInfo, keyword-led constructs from keywordRule. The parser consults these same tables, so this grammar cannot drift from what BANG actually parses.

Operator precedence

Binding powers from opInfo, loosest first (higher BP binds tighter). Associativity is read off the powers: left-assoc ⟺ leftBP < rightBP, right-assoc ⟺ leftBP > rightBP. Application (juxtaposition) binds tighter than every operator below; .-method-perform tighter still.

Keyword-led constructs

Each is a reified Rule (keywordRule): a linear sequence of keyword literals and sub-parses — <expr> a full expression, <atom> an atom, <ident> a bound name. Surface constructs not (yet) reified as rules are parsed by bespoke arms; the complete construct list is the Surface syntax table above.

let is NOT in the table above (issue #68): its multi-binding sugar needs a repeated-group grammar the fixed linear Rule/Choice shape can't express, so — like let (a,b) = …, let rec, match, do — it is a bespoke pExpr arm instead. let x = e1; y = e2; … in body binds SEQUENTIALLY (a later binding sees every earlier one; an earlier binding can never see a later one). Contrast with Haskell's let-block, which is mutually recursive: bang's plain let stays non-recursive by convention (let rec is the only recursion marker; its … and … chain is the ONE mutually-recursive multi-binding form — see below), so sequential-not-recursive is the reading consistent with the rest of the surface. Semantically it ELABORATES to the IDENTICAL nested chain a hand-written let x = e1 in let y = e2 in … in body already produces (a thin .lettMulti SUGAR MARKER, erased before typing/lowering ever run — zero new semantics).

bang fmt's CANONICAL FORM is a single multi-binding block (issue #71, operator ruling 2026-07-10): every MAXIMAL RUN of sequential let-bindings prints as ONE let x = e1; y = e2; … in body — a hand-written nested chain COLLAPSES into this form exactly like a sugar-parsed one does (a single binding still prints plain let x = e in body, no trailing ;). The collapse is exactly semantics-preserving, including when a later binding SHADOWS an earlier one's name (let x = 1 in let x = x + 1 in x collapses to let x = 1; x = x + 1 in x — verified, not assumed: the grammar imposes no duplicate-name restriction, and sequential scoping through the ;-chain matches the nested chain's binder-shadowing exactly).

Mutual recursion — let rec … and … (ADR-0102, issue #97)

let rec grows a MUTUALLY-RECURSIVE multi-binding form by chaining siblings with and: let rec f : T1 = e1 and g : T2 = e2 … in body. Every sibling is in scope in every sibling's RHS (so f may call g and g may call f) — the one place bang's surface is mutually recursive. A single-binding let rec (no and) keeps its original non-mutual shape unchanged; ≥ 1 and desugars to the .letRecMultiS group form.

Each sibling carries its OWN mandatory : T ! {row} ascription (the same rule a non-structural single let rec already needs, ADR-0073): a mutual group's siblings hand off to each OTHER, not to a strict subterm of their own argument, so neither structurally certifies on its own — both need the explicit ! {Div}.

let rec even : Int -> Int ! {Div} = fun n =>
      if n == 0 then 1 else ($odd) (n - 1)
    and odd : Int -> Int ! {Div} = fun n =>
      if n == 0 then 0 else ($even) (n - 1)
in ($even) 10
-- ⟹ 1

See examples/mutual-parity for the N-way cycle (a three-sibling and group).

Binding a function (issue #121)

let f = e in body binds a VALUE — e must be a value, not a bare computation. fun x => … is a COMPUTATION (a "returner") in bang's CBPV core (ADR-0007), so binding one directly — let f = fun x => … in body, the single most natural thing a functional programmer reaches for — is a type error (B015): a bare function is a computation, not a value. Suspend it in a thunk to bind it: let f = {fun x => …} in body; force it to call it: ($f) arg. This applies at every let, not only top-level ones. examples/caesar follows this idiom throughout (encode/decode).

Lexical notes

Line comments: -- runs to end-of-line (or end-of-input) and is dropped by the lexer — no token, no source span (issue #62). -- wins maximal munch over the single-char - and the -> arrow, so a comment can follow either without escaping. Comments are stripped before parsing, so they carry no meaning to check/run and are not preserved by bang fmt — a formatted file drops any comments in its input. There is no block-comment form.

Unary minus: -e desugars to 0 - e (the same binary-- AST node — no new surface constructor), binding to ONE atom — tighter than every binary operator, so -x + 1 reads as (-x) + 1 and -x * y as (-x) * y, matching mainstream convention. A bare (unparenthesized) application argument goes to the BINARY reading instead: f -1 parses as f - 1, not f applied to -1 — parenthesize for the unary reading (f (-1)) the same disambiguation every language with juxtaposition-application + infix - makes. Interacts with line comments: -- wins maximal munch over two - tokens, so 3--10 is 3 followed by a DROPPED line comment (--10), not 3 - (-10) — write 3 - -10 or 3-(-10) (a space or parens before the second -) to get subtraction of a negative.

Modules (ADR-0093)

A module is a file — import Foo resolves Foo.bang (same directory, then the project root; a miss is a loud error naming both probed paths). No module header, no module { … } block — the module's name IS its filename stem.

The header comes first. import/use lines form the file's HEADER and must appear before any let/data/trait/fn decl — a use/import after the first decl is a parse error (unexpected 'use'/'import' where an atom was expected). Any number of import/use lines compose, in any order, within the header.

Qualified access — the $(mod.op) arg convention. A qualified reference to an imported (not used) function must be FORCED as a PARENTHESIZED group, not a bare dotted atom: $(Foo.op) arg, never $Foo.op arg — $ forces exactly one ATOM, and Foo.op is not itself an atom, so $Foo.op arg parses as ($Foo).op (forcing Foo alone, then projecting .op off the result) — almost never what's intended. The same rule applies to any qualified call, including inside let/match; a use-hoisted name needs no such wrapping (use Foo (op) then a bare $op arg, exactly like a local binding).

The Mod_Type hand-qualification convention. A qualified TYPE name has no dot syntax (pTy parses no Foo.T) — an imported data type must be spelled by hand as Foo_T (the module resolver's own qualification scheme, Mod _ Name) wherever a bare type name is needed, e.g. a match (v : Foo_T) { … } ascription or a function's declared parameter type. use Foo (T) avoids this — it hoists T (and its constructors) fully unqualified, so the plain name T is written and matched on directly.

Known v1 limitation (visibility enforcement, tracked as issue #73): pub/private-by- default is the DESIGNED semantics above (ADR-0093 D3), but enforcement is not yet wired — today a non-pub decl is still importable. Treat pub as the interface you are declaring, not (yet) a gate the checker enforces.

See examples/json/ for a worked four-file module program (Json.bang/Parse.bang/ Print.bang/main.bang) exercising import, qualified access, and Mod_Type ascriptions end-to-end, gated by check-examples.

Traits & Laws (ADR-0040 §5, ADR-0068)

A trait declares a Self-typed interface: zero or more operation SIGNATURES (fn) and zero or more LAWS (law) the implementations are expected to satisfy. An impl provides the operation bodies for one STRUCTURAL target type. Member separators (; or ,) are optional — the leading keyword (fn/law/}) alone delimits each member.

trait Add { fn add(a, b) -> Int ; law comm(a, b): add a b == add b a }
impl Add for Int { fn add(p, q) = p }

A law body calls a trait op in PAREN-CALL form (add a b == add b a, note the add a b, ordinary curried application) — this is consistent with the rest of the surface's curried convention (f x y, not f(x, y)). An impl's operation DEFINITION, however, uses a TUPLE-STYLE parameter list at both the trait declaration site (fn add(a, b) -> Int) and the impl site (fn add(p, q) = p) — the parenthesized, comma-separated form, not curried fn add a b. This is a deliberate but visible asymmetry: trait/impl SIGNATURES use the paren-list form, law BODIES and ordinary function calls elsewhere use curried application.

bang test [<file.bang>] (issue #60) discovers every trait-law instance in a decls-only program and sample-checks it (30 Int-tuple samples, a fixed seed for CI-reproducible runs), reporting PASS/FAIL/ERROR/STUCK per law — end-to-end law EXECUTION through the CLI works (issue #74, closed): a law body written in the SUPPORTED shape (its trait ops reached only through the overloaded operator — add a b == add b a, not add(a, b) by name) samples and PASSes/FAILs for real.

A law body may not call its trait op BY NAME (eq(x, x) or curried add a b where add/eq name a trait op directly): ADR-0068 wires trait-op resolution EXCLUSIVELY through the overloaded operator (==/</+/…), never a direct call — even a sibling op of the SAME impl cannot call another op of that impl by name. bang test diagnoses this UP FRONT with a specific, fixable message (law 'Trait.law' calls trait op 'op' directly — trait ops are invoked ONLY through their overloaded operator in v1 (ADR-0068; …)) rather than the opaque runtime crash (app: callee is not a function) an earlier version gave.

Deriving (ADR-0097, issue #109)

A data decl's trailing deriving (Eq, Ord) clause generates the trait/impl pair a hand-written Eq/Ord implementation would otherwise need — same-tag structural fold for Eq (AND over every payload slot; different tag ⇒ false), decl-order tag comparison + lexicographic payload for Ord:

data Point = Pt(Int, Int) deriving (Eq, Ord)
let p1 = Pt(3, 4) in
let p2 = Pt(3, 4) in
if p1 == p2 then 1 else 0   -- 1: equal, via the derived impl (no hand-written one)
-- ⟹ 1

The generated impl is indistinguishable from a hand-written one — ==/< dispatch through it exactly like any other trait op, usable directly in a match. A SELF-RECURSIVE carrier (data IntList = Nil | Cons(Int, IntList) deriving (Eq)) is supported: the fold recurses through the SAME knot-based let rec dispatch (#112) a hand-written recursive impl rides. The GENERATED impl always uses the carrier's OWN type-qualified ctor names internally (IntList_Nil/IntList_Cons, ADR-0099's Type_Ctor form) — so if your carrier's bare ctor names collide with another co-present type's (e.g. the prelude's built-in List a = Nil | Cons(a, List a), ADR-0103 Amendment ①), you construct/match VALUES of your own carrier with the SAME qualified spelling (IntList_Cons(1, IntList_Nil), not bare Cons(1, Nil)) — B012 catches the ambiguity loud, naming the fix.

Only Eq/Ord derive today (tier 1 — their ops are binop-dispatched, so a derived impl is usable the moment it exists, no separate name-callability wiring). A GENERIC carrier cannot derive (data Box a = Mk(a) deriving (Eq) is refused LOUD at the decl site, naming the limitation): deriving emits ONE impl at decl time, targeting the carrier's own (necessarily monomorphic) type — a generic data has no single monomorphic type to target, and unlike a let rec's call-site-driven monomorphization (ADR-0103), a deriving clause has no call site to discover an instantiation set from. Work around it with a monomorphic alias data decl (data BoxI = Mk(Int) deriving (Eq)) or a hand-written impl for the specific instantiation needed. See examples/derive-eq-ord/, examples/trait-recursive-eq/, examples/trait-recursive-ord/.

User-defined effects (ADR-0095, issue #44 Stage 7)

A user declares a NAMED effect interface (effect Name { op : ArgTy -> ResTy, … }), installs a HANDLER for it at a use site (handle e with Name as h { … }), and PERFORMS through the handler's own capability value (h.op(arg)) — the SAME "runtime is a handler installed at the use site" thesis the built-in effects (state/atomically) already use, now user-spellable. The kernel is untouched: this surface lowers to the already-landed Handler.custom constructor (ADR-0085) — a fourth handler shape, not a sixth primitive.

effect Net { fetch : Int -> Int }             -- the interface: one op, Int -> Int
 
handle
  (net.fetch(1)) + (net.fetch(2))              -- performs through the `as`-bound `net`
with Net as net {
  fetch(n) => n * 10                           -- bare body = the resume value (implicit tail-resume)
}
-- ⟹ 30   (examples/handle-custom-tracer)

Clause bodies are CURRIED, matching the perform site (op(x, y) => body desugars to a curried clause, mirroring h.op(x)(y)'s own curried call shape) — a deliberate divergence from today's trait-op convention (trait ops stay tuple-style, fn add(a, b); effects are a new construct born curried rather than inheriting the trait-op inconsistency).

A bare clause body IS the resume value — v1 has no resume keyword. op(x) => x * 10 resumes the captured continuation with x * 10 directly (one-shot, tail-resumptive); there is no explicit resume(…) form to write in v1 (a future multi-shot upgrade grows the surface additively, it does not change this form).

The carried param is CLAUSE-NAMEABLE via the reserved identifier param (issue #87, ADR-0095 D1's own worked example). A (Name init) as h clause body reads the init value through the bare word param — READ-ONLY in v1 (no param-UPDATE surface, ADR-0092 D5 deferred):

effect Reader { fetch : Int -> Int }
handle net.fetch(5) with (Reader 100) as net { fetch(x) => x + param }
-- net.fetch(5) resumes with 5 + 100
-- ⟹ 105

param is RESERVED at every BINDER position (a clause-arg name, the as h capability binder, a let/fun name, …) — the same discipline with/resume already use — so no user binding can ever shadow it; it stays freely usable as an ordinary expression (param, param + x, …) everywhere else, exactly like get. A param-less Name (no (Name init)) still elaborates fine; its clauses simply have no reason to reference param.

The v1 RET-SHAPE restriction — a clause body may not itself perform an effect before resuming. A clause whose body computes-then-effects (e.g. performs another op, or raises) is rejected with a named diagnostic, not a bare type error:

error: handle: clause 'fetch' body must be a `ret`-shape value in v1 (no effects
       before resuming) — a compute-then-return body needs binop typing (ADR-0065)
       + resumption-grade surfacing (Q27), tracked as the general-body entry gate
       (ADR-0095 D4)

A clause body that only computes arithmetically over its argument and returns (no nested effect performed) is fine (fetch(n) => n * 10, fetch(n) => n + 1); a clause performing raise/another op/etc. before its final value hits this wall.

Effect op names may not collide with a built-in effect's own operations (get/put/ new/read/write/raise/handle are reserved at the op-name position) — a collision is a loud parse/elaboration error naming the conflict, not a silent shadow.

Passing a capability to a helper function (issue #90/#123). The net/h bound by as is an ordinary VALUE once bound — it can be passed to a helper like any other argument, typed Cap Name (Cap Net, naming the effect). The catch: a bare inline ascription on the PARAMETER (fun e => (e : Cap Fail).fail(9)) does not parse as a cap type there — Cap Name must be spelled inside the enclosing THUNK's own arrow-and-row annotation, cap position included, exactly like every other parameter type:

effect Fail { fail : Int -> Int }
let apply = ( {fun cap => fun x => cap.fail(x)} : Thunk (Cap Fail -> Int -> Int ! {Fail}) )
handle (($apply) net) 9 with Fail as net { fail(n) => n }
-- ⟹ 9 — `net`, threaded as an ordinary Cap-typed argument, still dispatches by identity

Every effect row a threaded cap's own ops perform must appear in the THUNK's row (! {Fail} above) — the same row-composition rule an inline handle needs, just spelled once on the helper instead of at the call site.

An effect or op name that collides with a prelude Result/Option constructor name (Err/Ok/Some/None) is read as that CONSTRUCTOR at an ascription site, not the effect — (e : Cap Err) parses Err as the Result constructor, not an effect name, and fails with the unrelated-looking constructor 'Err' expects 1 argument(s). Name a custom effect something that does not collide with a prelude constructor (e.g. Fail, not Err) until effect/op names get their own namespace (tracked, issue #123).

See examples/handle-custom-tracer/, examples/handle-custom-resume/ (now reading its carried param through param for real, issue #87), and examples/handle-custom-abort-coexist/ (a raise inside a nested handle still aborts PAST a custom handler that is still installed — the two effect systems coexist) for worked, check-examples-gated single-op programs.

Effect channels

The surface's effect labels (the frozen v1 set). A handler on a label discharges its row; an undischarged label surfaces in the inferred effect (see Examples → type display).

Kernel primitives (the IR the surface lowers to)

The graded-CBPV kernel — Val (values), Comp (computations), Handler (effect handlers). The surface is sugar over these; Source.eval (Bang/Core/IR.lean) is the reference semantics.

Values (Val)

Computations (Comp)

Handlers (Handler)

Standard library

Library functions available FREE in every program that mentions them — Prelude.bang (repo root), auto-used (ADR-0098): no import/use line needed. They are let rec bindings, so call them with the force convention: ($concat) "ab" "cd", not bare concat …. A user binding of the same name shadows the injected one (lexical scope, per-name — not an all-or-nothing bucket); this also covers a project that names its OWN module Prelude.bang — an explicit use Prelude (name)/import Prelude resolves to the USER's file (the ordinary same-dir-then-root search, ADR-0093 D1) and its own binding of name wins, exactly like any other user-vs-prelude shadow; with no explicit use/import naming Prelude, a same-named file just sits there unreferenced (no silent pickup).

Curried (multi-arg) let recs type … ! {Div} — the #47 multi-arg gap (ADR-0073), a sound over-approximation: they terminate but the certifier can't prove it, so they run correctly.

Generic prelude functions

Also FREE in every program that mentions them — Prelude.bang's remaining entries: the ⊥-row (non-recursive) companions to the tagged-sum types (Option/Result/the built-in sum Either) plus the type-agnostic first-slice prelude (issue #105). Auto-used ONLY for the names a program actually mentions (a syntactic scan, ADR-0098 — this is a FUEL discipline, not just a scope-pollution one: Prelude.bang is a real module merged in via mergeModules, and an unconditional merge would tax every program one evaluation step per unused entry). A user binding of the same name shadows the injected one.

Bound-free generics (take/drop/length/append/zip/range/replicate — no trait bound, a free element-type variable) need their instantiation ANCHORED at each call site by an explicit annotation on the argument that DIRECTLY carries the free variable (ADR-0103 — a monomorphization pre-pass, never a guess, R6's finiteness discipline): a List a-typed argument needs (xs : List Int), a bare a-typed argument (replicate's element) needs (x : Int) directly, not an annotation on the CALL'S result. An un-annotated call that leaves a free variable unresolved is a loud, self-teaching error naming the fix, never a silent guess.

Examples

Every example below is a build-verified #guard. ⟹ is evaluation; : is the inferred type.

A. Surface-string programs (run via runYieldsInt)

• let x = 3 in x ⟹ 3 — A1. PURE LET: a binding sequences; the body reads it. let x = 3 in x ⟶ 3.
• let x = 1 in (let x = 2 in x) ⟹ 2 — A2. LEXICAL SHADOWING: the inner binding of x wins; the outer 1 is hidden.
• let c = {7} in $c ⟹ 7 — value. Nothing runs until forced (ADR-0007). let c = {7} in $c ⟶ 7.
• (fun x => x) 5 ⟹ 5 — A4. LAMBDA β: applying the identity function to 5 reduces to 5.
• handle (raise 7) ⟹ 7 — yields the payload. handle (raise 7) ⟶ 7.
• handle (let z = raise 7 in 99) ⟹ 7 — let … in 99 frame; the 99 continuation is dropped (zero-shot). ⟶ 7.
• state 5 in get ⟹ 5 — A7. STATE — GET DEFAULT: with no write, get reads the initial cell. ⟶ 5.
• state 0 in (let z = put 7 in get) ⟹ 7 — (unlike raise), threading the new cell; the following get reads it. ⟶ 7.
• state 0 in (let c = {get} in (let a = put 5 in (let b = put 9 in $c))) ⟹ 9 — LATEST write (9) — pull-based reactivity, no sig, no kernel change. ⟶ 9.
• state 1 in (let c = {get} in (state 2 in $c)) ⟹ 1 — realizing lexical scope, the heart of the inc-5/6 soundness story, made observable.
• atomically (let r = new 100 in (let z = write r 70 in read r)) ⟹ 70 — 70, read it back — the heap is threaded, the write is visible. ⟶ 70.
• handle (atomically (let r = new 100 in (let z = write r 70 in raise 100))) ⟹ 100 — never commits. The abort payload is the ORIGINAL 100: the rollback witness.
• match Right(7) { Left(a) -> 0 , Right(x) -> x } ⟹ 7 — Right(7) is the right injection; the Right arm fires, binding x = 7. ⟶ 7.
• let (a, b) = (3, 4) in (let (c, d) = (b, a) in c) ⟹ 4 — b = snd. Re-pairing swapped (b, a) and reading the first proves the binding order. ⟶ 4.

A14–A16: ARITHMETIC COMPOSES with the other features (issue #4 × #1/#3/rung-4).

• let x = 3 in let y = 4 in x * x + y * y ⟹ 25 — A14. PURE arithmetic composition: x² + y² over two bindings. ⟶ 9 + 16 = 25.
• atomically (let a = new 100 in (let bal = read a in (let bal2 = bal - 30 in (let z = write a bal2 in read a)))) ⟹ 70 — COMPUTES the new balance (100 - 30), not a literal post-balance. read → subtract → write → read. ⟶ 70.
• state 4 in (let c = {get * get} in (let z = put 9 in $c)) ⟹ 81 — reads 9 and squares it. ⟶ 81. Derived reactivity falls straight out of thunks + the δ-rule.

A17–A19: arithmetic AS an effect-op argument (issue #26 part-1 — A-normalized lowering).

• state 0 in (let z = put (get + 1) in get) ⟹ 1 — canonical mutable counter, finally one line: read, add one, store. state N in (put (get+1); get) ⟶ N+1.
• state 41 in (let z = put (get + 1) in get) ⟹ 42
• state 100 in (let bal = get in (if bal < 30 then bal else (let z = put (bal - 30) in get))) ⟹ 70 — no let-binding needed for the arithmetic. balance 100 ≥ 30 ⟹ withdraw ⟹ 70.
• handle (let x = 7 in (if x < 10 then raise (x * 6) else x)) ⟹ 42 — the deep handle catches it. x = 7 < 10 ⟹ raise 42 ⟹ caught ⟹ 42.

A20–A21: an effect op FEEDS the operator chain (issue #26 part-2 — parser precedence).

• atomically (let a = new 100 in read a - 30) ⟹ 70 — precedence fix this was "expected ')', got '-'". atomically ⟹ 100 - 30 ⟹ 70.
• atomically (let a = new 5 in read a + 1) ⟹ 6
• atomically (let a = new 100 in (let z = write a (read a - 30) in read a)) ⟹ 70 — computed balance, read it back: 100 - 30 ⟹ 70. (Also the effect-op-arith example project.)

A22–A25: do-notation (issue #27) — sequential effectful statements, desugaring to nested letC.

• do { x = 3; y = 4; x + y } ⟹ 7 — A22. PURE do: binds then a result expression. ⟶ 3 + 4 = 7.
• state 5 in (do { x = get; put (x + 1); get }) ⟹ 6 — return the cell. Reads like x = get(); set(x+1); return get(). ⟶ 6.
• state 0 in (do { put 5; put 9; get }) ⟹ 9 — A24. SEQUENCED bare statements: two puts in a row (values discarded), then get. ⟶ 9.
• atomically (do { a = new 100; bal = read a; z = write a (bal - 30); read a }) ⟹ 70 — CBPV kernel underneath; this is what "surface the verified kernel" looks like end-to-end.

A24–A25: arithmetic/computations in ADT INTRO args & ELIMINATOR scrutinees (issue #29).

• let x = 20 in (let y = 4 in (match (if y == 0 then Left(0) else Right(x / y)) { Left(e) -> 0 , Right(q) -> q })) ⟹ 5 — Result recovers it. y = 4 ≠ 0 ⟹ Right(20/4) ⟹ matched ⟹ 5. (The if scrutinee + Right arg both A-norm.)
• let (a, b) = (if 1 < 2 then (3, 4) else (5, 6)) in a + b ⟹ 7 — a computation (the split scrutinee is A-normalized). 1 < 2 ⟹ (3,4) ⟹ a + b = 7.

Stage ② foundation — type ascription (e : T) parses into annotS (ADR-0066 ②).

• ( fun x => x : Int -> Int ) 5 ⟹ 5 — ascription erases at lowering: the annotated identity still runs as the bare identity.

Stage ④b — type DISPLAY (#5's "type display": effect rows made visible).

• ( fun x => x : Int -> Int ) : Int -> Int — pure types show with no effect suffix; effectful ones surface their row.
• ( fun x => raise x : Int -> Int ) : Int -> Int ! {throws}
• raise 7 : Int ! {throws}
• handle (raise 7) : Int
• state 0 in get : Int
• (get) : Int ! {state}
• let x = 2 in x + 3 : Int

Stage ④b (writing) — effect SIGNATURES: declare ! {ρ}, the checker enforces it (#5).

• ( fun x => raise x : Int -> Int ! {throws} ) : Int -> Int ! {throws} — a declared row that COVERS the inferred effect passes (and the inferred effect is what displays).
• ( fun x => x : Int -> Int ! {throws} ) : Int -> Int — a PURE function satisfies a may-throw signature (⊥ ⊆ {throws}).
• ( fun x => raise x : Int -> Int ) : Int -> Int ! {throws} — un-annotated arrow stays unconstrained: a throwing fn is fine, effect inferred + shown.

Exceptional / error terminals — the typed Outcome layer's NEW capability (issue #54).

• 1 + Left(0) ⟹ 0 — helper says only false, the Outcome names the actual terminal (here: a type error).

#118 — the bare-fun-param hole gap: fun p => … p == derivedCarrierValue …. elabS's

• effect Two { a : Int -> Int } handle (two.a(3) + 1) + 1 with Two as two { a(n) => n * 10 } ⟹ 32
• effect KV { set : Int -> Int } handle kv.set(7) with KV as kv { set(n) => n } ⟹ 7 — fixed parse) still runs end to end — confirms pOpName didn't just silently swallow real errors.

Validation ⑨b — HIGHER-ORDER constructor payloads (#45): a Thunk (Int -> Int) field.

• let f = ( {fun x => x + 1} : Thunk (Int -> Int) ) in ($f) 41 ⟹ 42 — the checkSC thunk arm (thunk in COMPUTATION position): an annotated thunk at top level, forced+applied.

Validation ⑨e — let rec SURFACE SUGAR (ADR-0073 §1): recursion, user-spellable.

• let rec sum : Int -> Int = fun n => if n == 0 then 0 else n + ($sum)(n - 1) in ($sum) 5 ⟹ 15 — countdown-sum 5+4+3+2+1+0 = 15, the recursive call written ($sum)(n - 1) (computation arg).
• let rec fac : Int -> Int = fun n => if n == 0 then 1 else n * ($fac)(n - 1) in ($fac) 5 ⟹ 120 — factorial 5! = 120 (multiplicative recursion).
• let rec sum : Int -> Int = fun n => if n == 0 then 0 else (let m = n - 1 in n + ($sum) m) in ($sum) 3 ⟹ 6 — a let-BOUND recursive-call arg is equivalent (the pre-#41 spelling still works).
• let rec loop : Int -> Int = fun n => ($loop)(n + 1) in ($loop) 0 ⟹ 0

Validation ⑨i — EFFECTFUL recursion via a DECLARED row (ADR-0088, #48).

• handle (let rec f : Int -> Int ! {throws} = fun n => if n == 0 then raise 99 else ($f)(n - 1) in ($f) 3) ⟹ 99 — is scoped where installed, not where called — the state/8/design-doc convention).
• state 0 in (let rec loop : Int -> Int ! {state} = fun n => if n == 0 then get else (let z = put (get + 1) in ($loop)(n - 1)) in ($loop) 3) ⟹ 3 — the ambient state handler across recursive calls.

Validation ⑨h — STRINGS: String = List Char (ADR-0074, #49).

• match 'a' { Char(n) -> n } ⟹ 97 — a char literal 'a' is Char 97; destructuring recovers the code point.
• match '\\n' { Char(n) -> n } ⟹ 10

Validation ⑨h′ — the STRING STDLIB: concat/reverse/eq injected FREE (#49 stage 3, #50).

• match (($reverse) \"abc\") { SNil -> 0, SCons(c, t) -> match c { Char(n) -> n } } ⟹ 99
• if (($eq) \"ab\" \"ab\") then 1 else 0 ⟹ 1 — eq char-by-char: equal strings → true (then-branch), unequal (content OR length) → false.
• if (($eq) \"ab\" \"ba\") then 1 else 0 ⟹ 0
• if (($eq) \"a\" \"ab\") then 1 else 0 ⟹ 0
• if (($eq) \"\" \"\") then 1 else 0 ⟹ 1
• ($strLength) \"abc\" ⟹ 3 — name, strLength, #144). Same structural-fold shape as lengthDef, now shipped for real.
• ($strLength) \"\" ⟹ 0
• ($strLength) (($concat) \"ab\" \"cd\") ⟹ 4
• 3 ⟹ 3

Strings & Characters (issue #65: the stranger-test's documented blind spot).

• match \"ab\" { SNil -> 0, SCons(c, t) -> match c { Char(n) -> n } } ⟹ 97 — IDIOM 1 (match a string): destructure SNil/SCons(Char(n), rest) to read its first code point.
• match \"\" { SNil -> 0, SCons(c, t) -> match c { Char(n) -> n } } ⟹ 0 — IDIOM 1, the empty string: SNil (no SCons to destructure).
• match (Char 97) { Char(n) -> n } ⟹ 97 — IDIOM 2 (build a char from a code point): Char <n> introduces; round-tripping recovers n.
• match ' ' { Char(n) -> n } ⟹ 32 — IDIOM 3 (common code point constants, all ASCII per the codepoint-encoding note above): space.
• match '0' { Char(n) -> n } ⟹ 48 — IDIOM 3: the digit range '0'-'9'.
• match '9' { Char(n) -> n } ⟹ 57
• match 'a' { Char(n) -> n } ⟹ 97 — IDIOM 3: the lowercase letter range 'a'-'z'.
• match 'z' { Char(n) -> n } ⟹ 122
• match 'A' { Char(n) -> n } ⟹ 65 — IDIOM 3: the uppercase letter range 'A'-'Z'.
• match 'Z' { Char(n) -> n } ⟹ 90
• match (($concat) \"foo\" \"bar\") { SNil -> 0, SCons(c, t) -> match c { Char(n) -> n } } ⟹ 102 — the auto-used STDLIB (free in every program, no import needed — Prelude.bang, ADR-0098): concat.
• if (($eq) \"cat\" \"cat\") then 1 else 0 ⟹ 1 — the injected STDLIB: eq, structural string equality.
• if (($eq) \"cat\" \"dog\") then 1 else 0 ⟹ 0

Validation ⑨d — VALUE-POSITION A-normalization (#41): computations spelled NATURALLY.

• let (x, y) = (1 + 0, 2 + 0) in x + y ⟹ 3 — (1 + 0, 2 + 0) is a bare computation-product destructured directly (was "not a value").

Validation ⑩ — named capabilities are TYPED (#3, ADR-0070).

• state 5 as h in h.get : Int
• state 1 as a in (state 2 as b in (let x = a.get in (let y = b.get in x + y))) ⟹ 3 — the TWO-CELL demo type-checks AND runs to 3 (typed path) — ambient can't express it.
• state 5 as h in (let z = h.put(7) in h.get) ⟹ 7 — put on a named cap, then get, still discharged.

Validation ⑦b — HM polymorphism RUNS end-to-end (ADR-0075 bite-0, the real pipeline).

• let id = {fun x => x} in (let a = ($id) 5 in (let u = ($id) () in a)) ⟹ 5 — id at Int and Unit (independent instantiations): 5.

#119 — the row-subsumption asymmetry (fork-1): checkSC's .annotS arm ALREADY used

• match Right(7) { Left(a) -> 0, Right(x) -> x } ⟹ 7 — #53 — bare anonymous injections RUN end-to-end through the typed default path (CHECK precedes eval).
• let x = Right(7) in match x { Left(a) -> 0, Right(x) -> x } ⟹ 7
• match Left(3) { Left(a) -> a, Right(x) -> x } ⟹ 3

GENERIC data types (ADR-0069 bite-1) — data List a monomorphized per concrete instantiation.

• data List a = Nil | Cons(a, List a) match (Cons(7, Nil)) { Nil -> 0, Cons(h, t) -> h } ⟹ 7 — solved μ). No : List Int annotation. Consumed by a match to yield an Int the run-oracle can check.
• data Option a = None | Some(a) match (Some(5)) { None -> 0, Some(v) -> v } ⟹ 5 — Some(x) where x : Int ⟹ Option Int, no annotation; destructured to its payload.
• data List a = Nil | Cons(a, List a) match (Cons(7, Nil) : List Int) { Nil -> 0, Cons(h, t) -> h } ⟹ 7 — annotation-free is ADDITIVE: the SAME decl still accepts an explicit : List Int (ADR-0079 check-mode).

Validation ⑨i-bis — issue #101: the WILDCARD match arm _.

• data Color = Red | Green | Blue match Red { Red -> 1, _ -> 0 } ⟹ 1 — a 3-ctor type, ONE explicit arm + wildcard covering the other two — picks the wildcard body.
• data Color = Red | Green | Blue match Green { Red -> 1, _ -> 0 } ⟹ 0
• data Color = Red | Green | Blue match Blue { Red -> 1, _ -> 0 } ⟹ 0
• data List a = Nil | Cons(a, List a) match (Cons(7, Nil)) { Cons(h, t) -> h, _ -> 0 } ⟹ 7 — a 2-ctor recursive type: _ covers the UNNAMED Nil case, Cons stays explicit and binds its payload.
• data List a = Nil | Cons(a, List a) match (Nil : List Int) { Cons(h, t) -> h, _ -> 99 } ⟹ 99
• data Color = Red | Green | Blue match Blue { Red -> 1, Green -> 2, _ -> 3 } ⟹ 3 — wildcard covering exactly ONE of three ctors (the other two named explicitly) — no wasted expansion.
• data List a = Nil | Cons(a, List a) match (Cons(1, Cons(2, Nil)) : List Int) { Nil -> 0, _ -> 42 } ⟹ 42 — expansion must still resolve Cons's GENERIC arity (2) to mint exactly 2 fresh binder names.

Validation ⑨j — the GENERIC PRELUDE: Option/Result + their maps + the ISO round-trips vs

• match (Some(5)) { None -> 0, Some(v) -> v } ⟹ 5 — ADR-0079/0081 generic-data guards above).
• match (Ok(7)) { Err(e) -> e, Ok(a) -> a } ⟹ 7
• match (Err(3)) { Err(e) -> e, Ok(a) -> a } ⟹ 3
• match (($mapOption) {fun z => z + 1} (Some(4))) { None -> 0, Some(v) -> v } ⟹ 5 — the INJECTED maps (mapOption/mapResult/bimap), used with no local definition.
• match (($mapResult) {fun z => z + 1} (Ok(4))) { Err(e) -> e, Ok(v) -> v } ⟹ 5
• match (($mapResult) {fun z => z + 1} (Err(9))) { Err(e) -> e, Ok(v) -> v } ⟹ 9 — mapResult passes an Err through untouched (maps the success side only).
• match (($bimap) {fun e => e + 100} {fun a => a + 1} (Right(4))) { Left(e) -> e, Right(a) -> a } ⟹ 5 — bimap g f maps BOTH sides: f over Right, g over Left.
• match (($bimap) {fun e => e + 100} {fun a => a + 1} (Left(4))) { Left(e) -> e, Right(a) -> a } ⟹ 104
• match (($eitherToResult) (($resultToEither) (Ok(5)))) { Err(e) -> 99, Ok(a) -> a } ⟹ 5 — eitherToResult ∘ resultToEither = id on Ok/Err (Result ≅ Either). Sentinel 99 = round-trip broke.
• match (($eitherToResult) (($resultToEither) (Err(3)))) { Err(e) -> e, Ok(a) -> 99 } ⟹ 3
• match (($eitherToOption) (($optionToEither) (Some(7)))) { None -> 99, Some(v) -> v } ⟹ 7 — eitherToOption ∘ optionToEither = id on Some/None (Option ≅ Either Unit).
• match (($eitherToOption) (($optionToEither) (None : Option Int))) { None -> 0, Some(v) -> v } ⟹ 0

Validation ⑨k — issue #105 FIRST-SLICE PRELUDE: fst/snd/abs/min/max/withDefault/

• ($fst) (3, 4) ⟹ 3 — fst/snd — the dogfood-json TOP papercut. p a literal pair.
• ($snd) (3, 4) ⟹ 4
• ($abs) (0 - 7) ⟹ 7 — abs — negative and positive/zero branches (both dogfooders hand-rolled 0 - n).
• ($abs) 7 ⟹ 7
• ($abs) 0 ⟹ 0
• (($min) 3) 7 ⟹ 3 — min/max — curried; both orderings (the < branch and its else).
• (($min) 7) 3 ⟹ 3
• (($max) 3) 7 ⟹ 7
• (($max) 7) 3 ⟹ 7
• (($const) 5) 9 ⟹ 5 — test-local const at ⑦b, proving the injected one generalizes the same way.
• (($const) 7) (1, 2) ⟹ 7
• ($id) 5 ⟹ 5 — a)annotation is what needed the monomorphization pre-pass —id`'s body has no such annotation).
• let n = ($id) 5 in let (a, b) = ($id) (3, 4) in n + a + b ⟹ 12
• (($withDefault) 0) (Some(9)) ⟹ 9 — two ctors — mirrors the mapOption/mapResult Err/Ok-both-arms discipline above).
• (($withDefault) 42) (None : Option Int) ⟹ 42
• if (($isDigit) (Char 48)) then 1 else 0 ⟹ 1 — CHAR KIT — isDigit: the '0'-'9' boundary (47 fails-low, 48/57 the inclusive ends, 58 fails-high).
• if (($isDigit) (Char 57)) then 1 else 0 ⟹ 1
• if (($isDigit) (Char 97)) then 1 else 0 ⟹ 0
• if (($isAlpha) (Char 65)) then 1 else 0 ⟹ 1 — isAlpha: both letter ranges (upper/lower) true, a digit false — the non-letter edge.
• if (($isAlpha) (Char 122)) then 1 else 0 ⟹ 1
• if (($isAlpha) (Char 53)) then 1 else 0 ⟹ 0
• match (($toUpper) (Char 97)) { Char(n) -> n } ⟹ 65 — toUpper/toLower — TOTAL: the letter-shift case AND the non-letter passthrough case each.
• match (($toUpper) (Char 53)) { Char(n) -> n } ⟹ 53
• match (($toLower) (Char 65)) { Char(n) -> n } ⟹ 97
• match (($toLower) (Char 53)) { Char(n) -> n } ⟹ 53
• let abs = { fun n => 999 } in ($abs) (0 - 7) ⟹ 999 — shadowing: a user let abs = … in the body WINS over the injected one (lexical scope contract).

Validation ⑨l — the List family: take/drop/length/append/head/tail, ridden over

• $length ((Nil : List Int) : List Int) ⟹ 0 — length — the empty list, a singleton, and a 3-element list (the self-recursive walk, all arms).
• $length ((Cons(7, Nil) : List Int) : List Int) ⟹ 1
• $length ((Cons(1, Cons(2, Cons(3, Nil))) : List Int) : List Int) ⟹ 3
• $length (($take 2) ((Cons(1, Cons(2, Cons(3, Nil))) : List Int) : List Int) : List Int) ⟹ 2 — (examples/list-basics) needed its own data List a; this doesn't.
• $length (($drop 2) ((Cons(1, Cons(2, Cons(3, Nil))) : List Int) : List Int) : List Int) ⟹ 1
• match ($head ((Cons(7, Nil) : List Int) : List Int)) { None -> 0 - 1, Some(v) -> v } ⟹ 7 — head — Some on a non-empty list, None on Nil (both Option arms, TOTAL).
• $length ((($range 0) 0 : List Int) : List Int) ⟹ 0 — range — build [lo, hi), verify via length (the empty range AND a non-empty one).
• $length ((($range 0) 5 : List Int) : List Int) ⟹ 5
• $length (($replicate 3) (7 : Int) : List Int) ⟹ 3 — length (count) and head (every element is the replicated value).
• match ($head (($replicate 3) (7 : Int) : List Int)) { None -> 0 - 1, Some(v) -> v } ⟹ 7

#90 — row annotations (T ! {…}) could only name the four BUILT-IN effects (throws/

• effect Net { fetch : Int -> Int } let get2 = ( {fun net => (net.fetch(1)) + (net.fetch(2))} : Thunk (Cap Net -> Int ! {Net}) ) in handle (($get2) net) with Net as net { fetch(n) => n * 10 } ⟹ 30 — types, and RUNS end to end (the #84 gap-1 pipeline that was checkProg-only until this fix).
• effect Net { fetch : Int -> Int } let test = ( {fun body => handle (($body)(net)) with Net as net { fetch(n) => n * 10 }} : Thunk (Thunk (Cap Net -> Int ! {Net}) -> Int) ) in let logic = ( {fun net => (net.fetch(1)) + (net.fetch(2))} : Thunk (Cap Net -> Int ! {Net}) ) in ($test) logic ⟹ 30 — Now types AND runs.
• effect Net { fetch : Int -> Int } let test = ( {fun body => handle (($body)(net)) with Net as net { fetch(n) => n * 10 }} : Thunk (Thunk (Cap Net -> Int ! {Net}) -> Int) ) in let prod = ( {fun body => handle (($body)(net)) with Net as net { fetch(n) => n + 1 }} : Thunk (Thunk (Cap Net -> Int ! {Net}) -> Int) ) in let logic = ( {fun net => (net.fetch(1)) + (net.fetch(2))} : Thunk (Cap Net -> Int ! {Net}) ) in (($test) logic) * 1000 + (($prod) logic) ⟹ 30005 — under each stage. 30005 = 30*1000 + 5 (test's n*10 vs prod's n+1, both over 1+2).
• effect Net { fetch : Int -> Int } let test = ( {fun body => handle (($body)(net)) with Net as net { fetch(n) => n * 10 }} : Thunk (Thunk (Cap Net -> Int ! {Net}) -> Int) ) in let prod = ( {fun body => handle (($body)(net)) with Net as net { fetch(n) => n + 1 }} : Thunk (Thunk (Cap Net -> Int ! {Net}) -> Int) ) in let logic = ( {fun net => (net.fetch(1)) + (net.fetch(2))} : Thunk (Cap Net -> Int ! {Net}) ) in let selector = (if 1 < 2 then test else prod) in ($selector) logic ⟹ 30 — pattern's "runtime-selectable" claim, confirmed live, not just narrated.

#85 — a NESTED binop in a handler clause body lost the clause's own binder. elabHClauses

• effect Net { pick : Int -> Int } handle net.pick(1) with Net as net { pick(n) => n * 10 } ⟹ 10 — LCG shape (ctr-design.md §RE2), now running in the tested superset.
• effect Net { pick : Int -> Int } handle net.pick(1) with Net as net { pick(n) => n * 3 + 1 } ⟹ 4
• effect Net { pick : Int -> Int } handle net.pick(1) with Net as net { pick(n) => (n * 3) + 1 } ⟹ 4
• effect Two { a : Int -> Int, b : Int -> Int } handle two.a(5) with Two as two { a(n) => n, b(n) => n } ⟹ 5 — clause, not just the one performed). Repro triple from #86's own report, all fixed:
• effect Two { a : Int -> Int, b : Int -> Int } handle two.a(5) with Two as two { a(n) => n + 1, b(n) => n + 1 } ⟹ 6
• effect Two { a : Int -> Int, b : Int -> Int } handle two.a(5) with Two as two { a(n) => n + n * 2, b(n) => n } ⟹ 15 — combined: multi-clause AND a nested binop in the performed clause (#85 ⊔ #86 in one program).

#87 — the parameter-carrying form's init becomes CLAUSE-NAMEABLE via the literal

• effect R { fetch : Int -> Int } handle net.fetch(5) with (R 100) as net { fetch(x) => param } ⟹ 100 — ACCEPT: a bare param clause body resumes with the carried init value directly (no arithmetic).
• effect R { fetch : Int -> Int } handle net.fetch(5) with (R 100) as net { fetch(x) => x + param } ⟹ 105 — ORIGINAL #87 report's own motivating shape (fetch(x) => x + param, README's stated intent).
• effect R { fetch : Int -> Int } handle net.fetch(5) with (R 100) as net { fetch(x) => param + x } ⟹ 105
• effect R { fetch : Int -> Int } handle (let r = net.fetch(5) in r + 1) with (R 100) as net { fetch(x) => x + param } ⟹ 106 — instead of hardcoding the literal 100 the way #87's report found.
• effect R { fetch : Int -> Int } handle net.fetch(5) with (R 100) as net { fetch(x) => x * 2 + param } ⟹ 110 — just the op-arg).
• effect R { fetch : Int -> Int } handle (let paramX = 7 in net.fetch(paramX)) with (R 100) as net { fetch(x) => x + param } ⟹ 107 — clause body — the reservation is exact-string, not a prefix block.
• effect R { fetch : Int -> Int } effect Q { ping : Int -> Int } handle ((handle (net.fetch(5)) with (R 100) as net { fetch(x) => x + param }) + (q.ping(1))) with Q as q { ping(n) => n } ⟹ 106 — second with on one handle.

ADR-0093 D5 (operator ruling, 2026-07-09) — top-level let/let rec DECLS actually RUN.

• let x = 3 data Marker = M x + 1 ⟹ 4 — otherwise parse as an APPLICATION ((3) x), the same ambiguity this whole corpus works around.
• let x = 3 data Marker = M let y = x + 1 data Marker2 = M2 x + y ⟹ 7 — plays after x's own binding.
• let rec fact : Int -> Int ! {Div} = fun n => if n < 2 then 1 else n * ($fact (n - 1)) data Marker = M let call = ($fact) 5 data Marker2 = M2 call ⟹ 120 — its own decl, avoiding both this and the earlier literal-adjacency traps in one move.
• data Pair = Mk(Int, Int) let p = Mk(3, 4) match (p : Pair) { Mk(a, b) -> a + b } ⟹ 7 — let/let rec decls compose with OTHER decl kinds (data), interleaved.
• let main = 42 data Marker = M main ⟹ 42 — form has no special elaboration path (D5: no main-only special case).
• let x : Int = 3 data Marker = M x + 1 ⟹ 4 — REAL type checker (a wrong ascription, e.g. let x : Unit = 3, would be caught below).

Clause-shape MATRIX (plan 002) — systematic coverage of the silently-missing-binder

• effect Net { fetch : Int -> Int } handle net.fetch(3) with Net as net { fetch(n) => n } ⟹ 3 — matrix: 1-op effect, bare clause body, atomic perform-site operand (baseline sanity cell).
• effect Net { fetch : Int -> Int } handle net.fetch(2) with Net as net { fetch(n) => ((n + 1) * 2) + (n * 3) } ⟹ 12 — matrix: 1-op effect, nested-binop clause body depth 3, atomic perform-site operand.
• effect Net { fetch : Int -> Int } handle net.fetch(4) with Net as net { fetch(n) => let m = n * 2 in m + 1 } ⟹ 9 — matrix: 1-op effect, let … in clause body, atomic perform-site operand.
• effect Net { fetch : Int -> Int } handle net.fetch(5) with Net as net { fetch(n) => ($({fun m => m + 1})) n } ⟹ 6 — matrix: 1-op effect, immediately-applied-lambda clause body.
• effect Net { fetch : Int -> Int } handle (net.fetch(1) + 2) + 3 with Net as net { fetch(n) => n * 10 } ⟹ 15 — matrix: 1-op effect, bare clause body, compound-LEFT perform-site operand.
• effect Net { fetch : Int -> Int } handle 3 + (2 + net.fetch(1)) with Net as net { fetch(n) => n * 10 } ⟹ 15 — matrix: 1-op effect, bare clause body, compound-RIGHT perform-site operand.
• effect Net { fetch : Int -> Int } handle (let r = net.fetch(2) in r + 1) with Net as net { fetch(n) => n * 10 } ⟹ 21 — matrix: 1-op effect, bare clause body, perform-site in a let RHS.
• effect Net { fetch : Int -> Int } handle (let t = {net.fetch(1)} in $t) + 0 with Net as net { fetch(n) => n * 10 } ⟹ 10 — REPEATED here as an explicit matrix cell rather than only living in the plan-003 section).
• effect Two { a : Int -> Int, b : Int -> Int } handle two.a(5) with Two as two { a(n) => n + 1, b(n) => n + 2 } ⟹ 6 — matrix: 2-op effect, decl order (a then b), both bodies bare, performed op is FIRST in decl order.
• effect Two { a : Int -> Int, b : Int -> Int } handle two.b(5) with Two as two { a(n) => n + 1, b(n) => n + 2 } ⟹ 7 — matrix: 2-op effect, decl order (a then b), both bodies bare, performed op is SECOND in decl order.
• effect Two { a : Int -> Int, b : Int -> Int } handle two.a(5) with Two as two { b(n) => n + 2, a(n) => n + 1 } ⟹ 6 — LAST in the handler.
• effect Two { a : Int -> Int, b : Int -> Int } handle two.b(5) with Two as two { b(n) => n + 2, a(n) => n + 1 } ⟹ 7 — written FIRST in the handler.
• effect Two { a : Int -> Int, b : Int -> Int } handle two.a(5) with Two as two { b(n) => n, a(n) => (n + 1) * 2 } ⟹ 12 — the OTHER clause's body stays bare — the #85⊔#86 combination with an asymmetric body shape.
• effect Two { a : Int -> Int, b : Int -> Int } handle two.a(5) with Two as two { a(n) => n * 2 + 1, b(n) => n } ⟹ 11 — COMPOUND one.
• effect Two { a : Int -> Int, b : Int -> Int } handle two.b(5) with Two as two { a(n) => n * 2 + 1, b(n) => n } ⟹ 5 — though it's never exercised by THIS run).
• effect Two { a : Int -> Int, b : Int -> Int } handle (two.a(3) + 1) + two.b(2) with Two as two { a(n) => n * 10, b(n) => n * 100 } ⟹ 231 — matrix: 2-op effect, compound-LEFT perform-site operand, decl order.
• effect Two { a : Int -> Int, b : Int -> Int } handle 1 + (two.a(3) + two.b(2)) with Two as two { b(n) => n * 100, a(n) => n * 10 } ⟹ 231 — matrix: 2-op effect, compound-RIGHT perform-site operand, reverse clause order.
• effect Two { a : Int -> Int, b : Int -> Int } handle (let r = two.b(4) in r + two.a(1)) with Two as two { b(n) => n * 10, a(n) => n + 1 } ⟹ 42 — matrix: 2-op effect, perform-site in a let RHS, reverse clause order.
• effect Two { a : Int -> Int, b : Int -> Int } handle two.a(6) with Two as two { a(n) => let m = n + 1 in m * 2, b(n) => n } ⟹ 14 — matrix: 2-op effect, let … in clause body on the performed clause, decl order.
• effect Three { a : Int -> Int, b : Int -> Int, c : Int -> Int } handle three.b(5) with Three as three { a(n) => n + 1, b(n) => n + 2, c(n) => n + 3 } ⟹ 7 — least like either endpoint).
• effect Three { a : Int -> Int, b : Int -> Int, c : Int -> Int } handle three.a(5) with Three as three { c(n) => n + 3, b(n) => n + 2, a(n) => n + 1 } ⟹ 6 — matrix: 3-op effect, REVERSE clause decl order (c, b, a), performed op is the one declared FIRST.
• effect Three { a : Int -> Int, b : Int -> Int, c : Int -> Int } handle three.c(5) with Three as three { c(n) => n + 3, b(n) => n + 2, a(n) => n + 1 } ⟹ 8 — FIRST in the handler.
• effect Three { a : Int -> Int, b : Int -> Int, c : Int -> Int } handle three.b(4) with Three as three { b(n) => (n + 1) * 2, a(n) => n, c(n) => n } ⟹ 10 — performed op is the MIDDLE-declared one, body is a nested binop.
• effect Three { a : Int -> Int, b : Int -> Int, c : Int -> Int } handle three.a(1) + three.b(2) + three.c(3) with Three as three { a(n) => n * 10, b(n) => n * 100, c(n) => n * 1000 } ⟹ 3210 — — exercises every clause's binder in a single program.
• effect Three { a : Int -> Int, b : Int -> Int, c : Int -> Int } handle three.a(1) + three.b(2) + three.c(3) with Three as three { c(n) => n * 1000, b(n) => n * 100, a(n) => n * 10 } ⟹ 3210 — matrix: 3-op effect, all three ops performed, REVERSE clause decl order.
• effect Three { a : Int -> Int, b : Int -> Int, c : Int -> Int } handle three.c(2) with Three as three { b(n) => n, c(n) => ((n + 1) * 2) + (n * 3) , a(n) => n } ⟹ 12 — order handler.
• effect Net { fetch : Int -> Int } handle net.fetch(3) with Net as net { fetch(n) => let m = n + 1 in (m * 2) + (n * 3) } ⟹ 17 — combines the "nested binop depth 3" and "let-body" body-shape axes in one clause.
• effect Two { a : Int -> Int, b : Int -> Int } handle two.a(3) with Two as two { b(n) => n, a(n) => ($({fun m => m * 2})) n } ⟹ 6 — clause decl order.

Programs & observation

A program is a closed term of ground type — a Comp with no free variables whose value type is a base type (Int/Unit, or a sum/product of them). The CLI entry convention (bang run / eval, the runYieldsInt harness) accepts exactly these and reports the outcome of Source.eval (Bang/Core/Semantics/Eval.lean), the reference semantics.

Observable outcomes are the constructors of the reference's Result type — nothing else about a run is observable:

This is the same observation the ◊4 contextual-equivalence work quantifies over: lr_sound holds two programs equivalent when they agree on this outcome (convergence at ground type) in every closing context. One definition, two consumers — the reference runner and the equivalence LR.

Conformance

A conforming implementation of BANG agrees with the reference semantics Source.eval (Bang/Core/Semantics/Eval.lean) on the observation defined above, for every program in the normative corpus, and diverges only where the reference diverges.

The normative corpus is the executable conformance suite:

• Bang/Examples.lean — the curated worked-examples corpus; every #guard runs the compiled kernel, so a false assertion fails lake build.
• the verified examples rendered in this reference (the Examples section above) — each a lake build-gated #guard.

Because the oracle is mechanized and every example is build-gated, drift is a failing diff, not a judgement call — the top rung of the single-source-of-truth ladder (generate / test) applied to implementations. A third-party or AI-paved implementation is checkable by running the corpus against it: invariant #1 ("proof rides the reference; anything that runs is differential-tested against Source.eval") stated as a spec clause.

Errors & terminals

BANG makes the choice most languages never do: there is no undefined behavior. Every reachable failure is a defined, fail-loud outcome. Against the C-standard trichotomy:

Static errors reject a term before it is a program: parse errors, type errors, and effect-signature violations (an ! {ρ} annotation that under-declares the inferred row). A rejected term never runs.

Runtime terminals are the fail-loud outcomes of a run — the Result failure constructors (Bang/Core/Semantics/Eval.lean) plus the IR's explicit fail-loud marker (Comp.wrong, Bang/Core/IR.lean):

The fourth Result outcome, stuck (genuine stuck), is unreachable for a well-typed ⊥-row program — that is exactly what type_safety proves, and what "no undefined behavior" means: there is no reachable failure the semantics does not name.

escapedCap is defined for v1, not silent corruption: the kernel's global-fresh capability minting guarantees an escaped cap resolves to no handler and fails loud (OCaml-effects' Effect.Unhandled). Post-v1 it becomes untypeable — scoped/region capability types (#21) make the escape unrepresentable rather than merely detected.

bang query — the agent LSP as stateless CLI subcommands (issue #80)

bang query <op> exposes the compiler's own facts (parse/elaborate/check results) as JSON — the cheapest "LSP for agents": no server, no protocol, one process per call. Every op's Lean-side implementation is Bang/Frontend/Query.lean, a public library API (every fact-producing function is public, documented as reusable outside the CLI — a Lean script can call declFactsOf/nameRefEdgesOf/lawInstancesOf directly).

bang query dump [<file.bang>] is the key operation: the COMPLETE fact base in one export, so you compose arbitrary queries (jq, python, a Lean script) instead of waiting on a new fixed verb. Every curated verb below (symbols/type/effects/def/ refs) is a thin projection of the SAME fact list dump exports — one construct, not six independent implementations.

dump's schema — a VERSIONED public contract

{
  "ok": true,
  "schemaVersion": 1,
  "bangVersion": "0.1.1",
  "decls": [ { "name": "..", "kind": "let|letRec|fn|trait|impl|data|effect",
               "type": "T"|null, "row": "{..}"|null, "typeError": "msg"|null,
               "shape": {..}|null, "pub": true|false, "module": "Mod"|null } ],
  "refs": [ { "from": "declName", "to": "referencedName" } ],
  "laws": [ { "trait": "..", "law": "..", "params": [".."], "body": "source text" } ],
  "imports": [ { "module": ".." } ],
  "uses":    [ { "module": "..", "names": [".."] } ]
}

decls/refs/laws/imports/uses are FLAT top-level arrays of flat records — a relational fact base (Glean's "predicates = tables, facts = rows" framing), never a nested tree. The concrete test: dump's output loads into DuckDB with ONE read_json call, no unnesting gymnastics —

bang query dump myfile.bang | duckdb -c "SELECT unnest(decls) FROM read_json('/dev/stdin')"

Every DeclFact key is always present — null means absent, never a missing key — so a jq '.decls[].type'-style consumer never branches on key existence, only on nullness. type/row are some only for a VALUE-typed decl (let/letRec/fn) that type-checks; typeError carries the checker's message when it doesn't; shape carries a structural summary (ops/ctors/params) for trait/impl/data/effect, which have no value-level type. refs is DECL-granularity (which decl's body mentions which name).

Position-addressing (line/col → decl) landed at DECL granularity (issue #52 slice 5, bang query hover, below) — a cursor resolves to the NEAREST-ENCLOSING top-level decl, not an exact sub-expression. EXACT sub-decl spans remain OUT of v1: Surf carries no per-node span (the Spanned-Surf tier, docs/notes/spanned-surf-design.md's Q1 — deferred until a concrete consumer needs finer-than-decl precision).

schemaVersion/bangVersion are TWO DISJOINT fields, first-class from v1 (bang's docs/notes/compiler-as-dbms-survey.md, the ONE piece of DBMS discipline adopted eagerly, not post-1.0): bang's 0.x "breaking changes allowed" policy collides with "agents write durable scripts against dump's JSON" — every unversioned BREAKING change silently invalidates every saved query. The two fields split the concern:

• schemaVersion — a plain monotonic integer, THE CONTRACT. Bumps ONLY on a BREAKING shape change (a field/table rename, removal, or meaning-change) — never for additive growth. A durable consumer keys ITS compatibility check on this field alone.
• bangVersion — PROVENANCE metadata (which compiler binary emitted this dump), NOT a compatibility signal — never gate a script's behavior on it.

The other half of the contract binds the CONSUMER: implementations MUST IGNORE UNKNOWN FIELDS (the protobuf/Kubernetes-API discipline). This is what makes "additive ⟹ non-breaking" true by construction — a script asserting schemaVersion == 1 must survive twenty compiler releases that only ADD facts; a script that hard-fails on an unrecognized key breaks that guarantee itself, regardless of what bang promises.

tools/golden-dump-caesar.json is a pinned snapshot gated by tools/test-query.sh's golden-dump-schema-pinned check — ANY shape change (breaking or additive) must re-pin this file in the same commit, so drift is always VISIBLE in the diff, never silent; a BREAKING change additionally requires the schemaVersion bump.

decls/refs/laws/imports are the extensional fact base (extracted, not computed from other facts); the curated verbs below are intensional — derived predicates (views) over this extensional base, kept few and stable per the Kythe/Glean small-core lesson (push richness into derived views, not the base schema).

KNOWN v1 LIMITATIONS (both match check --json's own documented multi-file grants, not new gaps): on a MULTI-FILE (resolver-aware) dump, "laws" is always [] — the merged program has no single contiguous source lawInstancesOf could re-derive law bodies from; and a decl's "module" is null unless the CLI layer's own resolution walk supplies provenance (Query.lean's declFactsOf alone never computes it — a flat merged Prog carries no per-decl module field). An imported (not used) decl's own "name" is QUALIFIED by the merge (Parse.bang's dropWs becomes Parse_dropWs, TypeCheck.mergeModules's convention) — def/refs/type/effects on a multi-file program address the qualified name, discoverable via dump/symbols's own "name" field.

The curated verbs (thin projections of dump)

All are --json-only (agents are the audience — no human-rendering flag in v1). Every op reads stdin when no <file.bang> is given, except type/def/refs (name-addressed multi-arg forms that always require a file). A <file.bang> with import/use is resolved the SAME way bang check/bang run resolve it — imports are visible to every op. Exit codes: 0 the op ran (including an op-level "ok":false answer, e.g. def naming a decl that doesn't exist — the tool succeeded, the ANSWER is negative); 1 the op could not run at all (a parse or import-resolution failure, still "ok":false on stdout); 2 a tool error (e.g. unreadable file) — reported on stderr, nothing on stdout, never folded into the JSON (mirrors check --json's own tool-error convention exactly).

hover — decl-granularity position query (issue #52 slice 5)

bang query hover [<file.bang>] <line> <col> answers "what decl is at this cursor, and what is its type" — the ONE position-addressed verb, resolving <line>:<col> (1-indexed, matching every other located-error convention in bang) to the NEAREST-ENCLOSING top-level decl (the LAST decl, in source order, whose name starts at-or-before the cursor). A cursor anywhere in a decl's body — not just on its name — resolves to that WHOLE decl; this is coarser than an LSP's exact sub-expression hover (see the position-addressing note above).

{"ok":true,"decl":{"name":"main","kind":"let","type":"Int","row":"{}",
 "typeError":null,"span":{"line":2,"col":5,"endLine":2,"endCol":9}}}

decl carries the SAME fields as one dump/symbols entry (name/kind/type/row/ typeError), plus span — the decl's NAME-TOKEN location, rendered with the same {"line","col","endLine","endCol"} shape bang check --json's diagnostics use (one Span-rendering convention, reused, not reinvented). A cursor before every decl's name (e.g. inside the import/use header) is an honest miss:

{"ok":false,"error":"no decl at 1:1"}

still exit 0 — the tool ran and produced a well-formed negative answer, the SAME convention def's "no such decl" miss uses. hover is resolver-aware like every other op (imports visible); on a multi-file program the cursor addresses the ENTRY file's own source text (the file passed on the command line), not an imported module's.

Known interaction (issue #100, open, not fixed by this verb): a decl whose checker- rendered type mentions a user data type can leak an internal μ-encoding placeholder (e.g. #1000070) in the type string — the SAME rendering dump/symbols/type already produce for such a decl. hover does not introduce this; it re-renders the existing fact.

Composing an arbitrary query over dump — the whole point: no fixed verb answers "every exported decl whose type carries a divergence taint", but dump + jq does:

bang query dump myfile.bang | jq -c '
  [.decls[] | select(.pub and ((.type // "") | contains("Div"))) | .name]'

bang rewrite — the CQS command side over the query fact base (issue #81)

bang query INSPECTS a program (the read model); bang rewrite <verb> REWRITES one — a pure Prog → Prog transform, implemented in Bang/Frontend/Rewrite.lean as a public library API (every rewrite is public, reusable outside the CLI, mirroring Bang.Query's own tier-1 convention) and consuming the QUERY side's own public facts (declFactsOf) rather than re-deriving a second decl inventory.

Output contract — immutable by default, mutation opt-in (the language's own description-until-forced thesis, $/force, applied to tooling): every verb prints a unified diff (source → rewritten) on stdout and touches NOTHING on disk, unless -w is given, which APPLIES the change to the file in place. There is no partial or silent mutation — a rewrite either emits a diff, or (with -w) writes the whole rewritten file, or aborts loudly with nothing written.

fmt as rewrite #0: bang fmt (the pre-existing, print-only CLI surface) is UNCHANGED — bang rewrite fmt is an ADDITIONAL surface sharing the SAME canonical printer (Bang.Format.showProg), so the two never disagree on what "canonical" means. Bang.Rewrite.fmt is a no-op on the parsed AST by construction (formatting changes printed LAYOUT only — Format.lean's own idempotency/round-trip laws already cover that at the Lean level); the diff a user sees is entirely showProg's re-layout.

rename's three loud diagnostics (ADR-0046 — never a silent guess): naming a <old> that doesn't exist, a <new> that COLLIDES with an existing top-level name, or an <old> that is ambiguous (more than one top-level decl sharing it — a malformed- program defensive case). The rewrite itself is a shadowing-aware, capture-safe AST walk (mirrors Bang.TypeCheck's own module-qualification pass, ADR-0093): a binder that shadows <old> stops the rename at that subtree, so a local variable of the same name is never touched.

The preservation gate — the moat feature

rename's static collision check only sees TOP-LEVEL names — it cannot see that the new name might collide with a LOCAL binding somewhere in the program (shadowing a call site rather than another declaration). The differential preservation gate catches this class of hazard: before emitting, bang rewrite rename re-elaborates BOTH the original and rewritten program (Bang.TypeCheck.checkAndLowerProg) and runs BOTH under the kernel ORACLE (Bang.Source.eval, the SAME reference --engine=oracle uses) — if the two outcomes disagree (a value that differs, one side elaborating and the other not, or elaboration failing with a genuinely different error), the rewrite ABORTS: no diff, no write, a loud message naming the divergence, nonzero exit.

This is a RUNG-1 (differential) preservation check, not a proof — docs/notes/ proof-export-survey.md's rung-2 (the binary LR's contextual-equivalence certificate) is the post-LR upgrade path for a machine-checked guarantee rather than a run-time differential gate.

annotate — types AND effect rows become explicit, diff-visible ascriptions

bang rewrite annotate infers the type AND effect row of every top-level let lacking an explicit ascription and splices it in — the SAME diff-by-default/-w contract every rewrite verb shares. It adds NO new checking: every fact it emits is a re-rendering of what bang query type/effects already compute (Bang.Query.typeStringOfDecl), reused directly.

The triple win: checking is cheaper than inference (the checker already computed every decl's type + row; annotate only renders it back into source), explicit context for an agent reading the file (a decl's paradigm — which effects it may perform — is visible without running the checker), and effect creep becomes diff-visible: a PR that adds Div/throws to a previously-unconstrained decl shows as a one-line change on annotate's own re-run, the same way any other diff does.

Never overwrites an existing ascription. annotate only fills in a MISSING ascription — let rec/bounded fn decls already carry a mandatory one (ADR-0073/ bite-2's own grammar), so they are always a no-op; a let that already has : T is left untouched even if the checker would infer something different-looking. A human-written ascription is authoritative.

Row annotations name only the four BUILTIN effects today (throws/state/stm/ Div) — a known gap, not a bug: naming a USER-declared effect's label in a ! {ρ} ascription requires a checker-side extension (TypeCheck.effNames) that has not yet landed. A decl whose row carries a user effect label is SKIPPED with a note (on stderr) rather than emitting an ascription that would silently fail to constrain the row it claims to — a forward pointer, not a silent gap.

Self-verified, per decl. Before ever returning a candidate ascription, annotate re-derives the checker's type string FROM the candidate and requires it to agree with what was originally inferred (roundTripsClean) — a decl whose checker rendering is ambiguous or otherwise fails this check is skipped, never emitted wrong. A failure here skips only THAT decl, never the whole file.

bang lint — a rule package over the query fact base (issue #82)

bang lint [<file.bang>] [--json] [--quiet-clean] runs a small package of rules over Bang.Query's own fact base (declFactsOf/nameRefEdgesOf) — RULES ARE QUERIES, no new analysis machinery. Human table by default, --json for the agent schema. It mirrors tools/DeadCode.lean's own Lean-side dead-code discipline (root set → transitive closure → "genuine orphan vs. intentional park" reading) at the SURFACE-program level.

Exit contract: 0 unless a warning-severity finding is present (an info-only or empty report still exits 0 — the caller inspects ok/the finding list, the SAME convention bang check --json uses); 1 when any warning finding fires; 2 the file could not be read. --quiet-clean suppresses the "no findings" success line on a clean human-table report (for a scripted caller wanting only nonzero-exit-on-real-findings) — it has no effect on --json output, which is always the complete, stable answer.

dead-private's own advisory honesty (mirroring tools/DeadCode.lean's own documented caveat): a decl reachable ONLY through a syntactic path this rule's SYNTACTIC closure (Query.nameRefEdgesOf + Query.surfUsesVar) cannot see is a false positive this rule does not itself distinguish from a genuine orphan — the finding names the decl, the human/agent judges deletability.

bang holes — residual/underdetermined positions (issue #82 item 3)

bang holes [<file.bang>] lists every top-level decl whose checked type or effect row carries a RESIDUAL hole — a position the inference could not pin down. bang has no user-facing _ hole syntax yet, but the checker still reports underdetermined positions: a bare id = {fun x => x} reports Thunk #1000003 -> #1000003, two positions (arg and result) the checker left polymorphic. Those #N markers (with N ≥ holeBase, Bang.TypeCheck.holeBase) ARE the holes — holes extracts and names them. ALWAYS JSON (agents are the audience), resolver-aware like query.

bang holes myfile.bang
{"ok":true,"holes":[{"name":"id","kind":"let","type":"Thunk #1000003 -> #1000003","row":"{}","holes":["#1000003"]}]}

A fully-pinned program reports {"ok":true,"holes":[]}. Exit contract (the query convention): 2 unreadable file (nothing on stdout), 1 parse/resolution failure (ok:false on stdout), 0 a well-formed answer (an empty holes array is still exit 0 — the caller inspects the array). This is a THIN PROJECTION of the SAME DeclFact list symbols/dump expose — no new checking logic.

bang impact — the pre-edit blast radius (issue #82 item 5)

bang impact <file.bang> <decl> reports the TRANSITIVE DEPENDENTS of decl — every top-level decl that reaches it directly or through a chain, so you know what breaks before you change it. This is the REVERSE of the reference graph bang query refs/ dump already expose (a forward edge src → tgt read backwards is "src depends on tgt"), computed as a reverse closure over that SAME edge set — no new graph walk.

bang impact myfile.bang double
{"ok":true,"decl":"double","dependents":[{"name":"main","kind":"let"},{"name":"quad","kind":"let"}]}

An empty dependents array is the honest "nothing depends on it, safe to change in isolation" answer. A nonexistent decl is a LOUD op-level miss ({"ok":false,"error":"no top-level decl named '…'"}, exit 0 — the tool ran). Same 2/1/0 exit contract as holes/query. ALWAYS JSON, resolver-aware. DECL granularity (#52).

bang semver-diff — the public-surface diff (issue #82 item 6)

bang semver-diff <old.bang> <new.bang> diffs the PUBLIC (pub) decl surface of two programs and reports the required version bump — #72's enforcement engine (elm-package precedent) falling out of the fact base. Non-pub decls are INVISIBLE (a private decl's churn never bumps a version).

bang semver-diff v1.bang v2.bang
{"ok":true,"bump":"major","added":["mul"],"removed":["sub"],"changed":[]}

The bump field is DERIVED from added/removed/changed so a caller (a release gate) keys its policy on ONE field. Exit contract: 2 if EITHER file is unreadable (tool error, nothing on stdout), 1 if EITHER side fails to parse (ok:false naming the side), 0 a well-formed diff. ALWAYS JSON. Known v1 gap (a forward pointer, not a silent miss): only VALUE-typed decls' type/row are compared — a trait/ data/effect's structural shape change is not yet a changed finding.

bang emit & bang build — compilation to Wasm (issue #136)

BANG's backend is Wasm 3.0 (ADR-0059): the pure λ + ADT + recursion fragment lowers to WasmGC. Two CLI verbs expose it — emit prints the text, build produces the artifact:

build runs the SAME module-resolved lowering emit does, then wasm-tools parse (wat→binary) + wasm-tools validate, writing a WASI command module — so:

bang build examples/json/main.bang -o json.wasm
wasmtime run json.wasm      # → 163  (== the program's Source.eval value)

This is the distribution story (docs/notes/distribution-survey.md): the compiled Wasm module IS bang's static artifact — one file, zero runtime deps, runs on any WASI+GC engine. bang build needs wasm-tools on PATH; a missing tool or an invalid module fails LOUD with the tool's own stderr, never a silent or wrong artifact. A program the GC fragment does not cover (a first-class-capability effect, or host-IO) refuses LOUDLY at emit time (EMIT-REFUSED), exit 1.

--component additionally wraps the module as a WASI component via wasm-tools component new. The preview1→WIT adapter is NOT bundled (no nixpkgs WASI adapter), so it is supplied via --adapter PATH or $BANG_WASI_ADAPTER (the pinned wasi_snapshot_preview1.command.wasm from wasmtime's releases); absent, build --component fails LOUD naming the artifact.

CLI contract

GENERATED from Main.lean's usage text and cross-checked against its bounded dispatcher arms.

Evidence

Diagnostic codes (bang explain)

GENERATED from the registry in Bang/Frontend/DiagCodes.lean (plan 013 s5) — the SINGLE SOURCE OF TRUTH. Each diagnostic carries a STABLE code (the rustc error[B004] pattern): it appears in bang check output (error[B004]: …) and in the explainCode field of bang check --json. bang explain <CODE> prints the code's summary, teaching text, and a minimal triggering example. A code stays stable across message-wording changes, so tools and docs can reference it durably.