Skip to content
spockIt’s only logical !
Decision record. This page preserves design history or future direction; it does not define current Spock behavior.

RFD 0012 — fn v2: name your refusals, span your tables, declare your polarity

Status: SHIPPED (July 2026) — all three features, spec’d in v0.md §7.4 and graphql.md §5.1, dogfooded in examples/instagram/v0.spock (which the upgrade left with one new finding: v0-FEEDBACK G17, statements cannot pass values). Implements v0-FEEDBACK G2, G3, and G11 as one milestone. This revises RFD 0009 §3’s ordering — fn v2 lands before the filter RFD — by the roadmap’s own rule: language work is the differentiator. The filter sub-language remains next after this.

1. The evidence

The instagram dogfood (examples/instagram/v0-FEEDBACK.md) hit three walls in the fn tier, and they are one wall seen from three sides — the contract half of a fn is less expressive than its escape half:

  • G2. A fn cannot name its refusals. follow refuses self-follows, private targets, and blocked pairs; all three surface as the same not_found envelope. Distinct product rules, zero distinct names.
  • G3. One statement means one table. approve_follow_request is broken by construction: approving must flip the request and create the follow row, and no single statement writes two tables. The only workaround is the raw floor, which bypasses every guard the file wrote.
  • G11. Twelve of 37 fns are pure reads served as GraphQL mutations — misfiled semantics, uncacheable, unparallelizable.

2. The shape

fn profile(user: user) -> profile_page {          // unmarked = read
  unchecked sql("""SELECT ... FROM user WHERE id = :user""")
}


mut fn approve_follow_request(request: follow_request) -> follow_request
    ! request_not_pending {
  unchecked sql("""
    SELECT spock_refuse('request_not_pending')
    WHERE NOT EXISTS (SELECT 1 FROM follow_request
                      WHERE id = :request AND status = 'pending')
  """)
  unchecked sql("""
    INSERT INTO follow (follower, target)
    SELECT requester, target FROM follow_request WHERE id = :request
  """)
  unchecked sql("""
    UPDATE follow_request SET status = 'approved'
    WHERE id = :request
    RETURNING *
  """)
}

2.1 Polarity (G11): fn reads, mut fn writes

The unmarked form is the read. This is the exposure-model default (RFD 0004: fail toward the failure you can see): an author who forgets mut on a body that writes gets a load failure, not silently misfiled semantics. The engine enforces it with sqlite3_stmt_readonly on every prepared statement of an unmarked fn — the body stays opaque to the checker, and the polarity is still total, because the engine can read what the language cannot.

Surfacing follows the polarity: read fns become Query root fields (GraphQL) and gain GET /rest/v1/rpc/<fn> with arguments in the query string (the PostgREST stable-function symmetry); mut fns stay on the Mutation root. POST /rest/v1/rpc/<fn> keeps working for both — POST is the universal call form; GET on a mut fn is refused with 405.

mut becomes a keyword — a source-level break for programs using it as an identifier, recorded in spec §2.3 alongside set/null/float.

Read fns claim their names on the Query root next to the derived <t>/<t>_by_pk fields; a collision (a read fn named exactly like a table) fails at startup like every other claim collision.

2.2 Multi-statement bodies (G3): the last statement answers

A body is now a sequence of unchecked sql(...) escapes. The laws:

  • Each escape is still exactly one SQL statement (the existing law, per escape). Each carries its own unchecked — the ledger counts escapes.
  • One transaction per call wraps the whole sequence — IMMEDIATE for mut fns (RFD 0005’s serializable stance), DEFERRED for reads.
  • Statements execute in order. The last statement produces the return value; it alone is checked against the declared return shape (at load, as today). Earlier statements are guards and effects: they are executed and their rows drained, results discarded. A non-final statement may return no columns (plain DML needs no RETURNING).
  • Parameters are checked across the set: every :param in any statement must be declared; every declared param must appear in at least one statement. Each statement binds only the params it names.
  • Arity semantics (-> t miss shouts, before commit) apply to the last statement’s rows, unchanged.

“The last statement answers” was chosen over marking a return statement: it needs no new syntax, the reading order of the body is the execution order, and a body that wants to answer with an earlier row re-reads it — one cheap SELECT, inside the same transaction, is the total price of keeping the grammar flat.

2.3 Declared refusals (G2): minted by the signature, raised by the body

The ! clause grows a second population. Today every code must resolve to a derived code or a reserved code (E039). Now a code that resolves to neither is a refusal minted by this fn — a product rule with a name. The contract carries it; introspection, TS types, and the error envelope speak it.

The raise channel is an engine builtin, following the §7.1 pattern:

SELECT spock_refuse('account_private')
WHERE EXISTS (SELECT 1 FROM user WHERE id = :target AND private)

spock_refuse(code) always errors when evaluated; a guard that selects zero rows never evaluates it. The runtime intercepts the error and routes:

  • code is a refusal declared by this fn → the §8.1 envelope with that code, kind refused, status 409 (the conflict family, next to the derived constraint violations), table: null, fields: [].
  • anything else → internal, before commit. That covers undeclared codes (the body broke its signature) and derived/reserved codes: a derived code can only be produced by its constraint, and a refusal can only be produced by its fn. If bodies could hand-raise user_username_taken, derived errors would stop being evidence.

Refusals share the one wire-level code namespace with derived codes. Nothing enforces global shape on refusal names (derived codes are <table>_<field>_<kind> by construction; refusals are free-form idents) — collision with a code some future table derives is possible and unenforced; the fix, if it ever bites, is renaming the refusal.

3. What this deliberately does not do

  • Pagination / cursors (G16) — deferred, user decision (July 2026). A fn returning rows is conceptually a named filter — view-shaped — and pagination discipline belongs to the universal dynamic query layer (the filter sub-language, RFD 0009 track 3), applied uniformly to tables, future views, and row-returning fns. It would be wrong to invent a per-fn cursor convention here and a table-level one there. fn v2 keeps the author-owns-LIMIT stance.
  • Actor context (G12). The claims seam arrives with auth; fn v2 creates its consumer surface but does not fake identity.
  • Composed return shapes (G8). Records stay flat and scalar.
  • Checked (non-escape) statements. The body remains all-escape; a checked statement language is not this RFD.
  • Verifying that a declared refusal is raisable. The body is opaque by design; a declared-but-never-raised refusal is dead metadata, visible in introspection, harmless at runtime. Symmetrically, E039’s typo-catching narrows: a misspelled derived code in a ! clause now mints a refusal instead of erroring. Accepted: the misspelling never fires (the real constraint still routes to the true derived code at runtime), so the failure is visible metadata, not wrong behavior.

4. Contract mechanics (§6 freeze discipline)

All additive — old contract JSON loads in new consumers:

  • FnDef.readonly: bool, #[serde(default)] (= false). Pre-v2 JSON has no field; every pre-v2 fn was a mutation, and false keeps it one.
  • FnDef.sql becomes a statement array; the deserializer accepts the old bare string as a one-element array. New JSON always writes the array (old consumers reading new JSON is not promised — §6).
  • FnDef.refusals: [string], #[serde(default)] (= empty). errors keeps carrying all declared codes, refusals included, so existing consumers of errors see the full vocabulary without new logic.

TS emission (spock gen types): fn entries gain readonly: true | false — a typed client must know which GraphQL root to address. Refusal codes join the error union via errors, no new shape.

5. The doctrine line

fn v1 proved the contract could reach into the escape (prepare-time validation). fn v2 proves the direction holds under pressure: polarity is declared in the signature and enforced against the opaque body; the transaction envelope spans statements the checker never reads; and the error vocabulary stays derived-or-declared — never improvised — even when the body is the thing speaking. The escape may replace the body, never the contract.