Evaluation judgments

02.04.03 2026-10-18 — Evaluation judgments

A map of cousins for treating the REPL transcript as equateable oordelen, not pretty-print. This note does not invent FPL language semantics; it names a pattern and what we have not built. Implementation of first-class errors and deadlines on the |- line waits on a later plan.

The pattern

Multi-component evaluation judgments: each successful (or failed) phrase leaves a line you could copy into a fixture — value, and eventually type, cost, error — in one shape. Status between phrases (clock, head, wall ms) stays on the phrase bar; what you would equate belongs on the judgment line.

Today the shell already uses turnstile form and bar costs:

;;! -( 22:52:09 )-< command 1 >-----------------------------{ head: 0 }-
1 | 1 +
|- 2 : ...
;;! -( 22:52:17 )-< command 2 >-------------{ head: 1; fuel: 3; ms: 0.4 }-

See REPL phrase costs for what fuel and ms on the bar mean now (fuel = steps spent; event.fuel remains the budget). The same meter is also called gas in the literature (PLFA); see Fuel, gas, and deadlines below.

Axes

Three questions for every cousin below:

Judgment line vs between-phrase status. What is equateable (|- …) vs chrome (;;! { … })?
Spent fuel vs wall time. Steps are deterministic enough to name; wall ms is a thermometer, not a law.
Failure as value vs failure as channel. Does the error sit in the value domain (Result / error-union), or only on stderr / exception unwind?

Vocabulary. When spent fuel later appears on the judgment line, call that component a deadline (steps taken under the meter). Prefer chrome @ <n> (e.g. |- 2 : ... @ 3), not / — FPL tokens are Forth-like, so / is already a plausible word, and overloaded judgment punctuation fights the OCaml habit of one meaning per operator. Keep wall ms on the bar.

Markers (three jobs)

Job	Glyphs / chrome	What it means	Where it lives
Falsum / absurdity	⊥, LaTeX `\lightning`, Unicode ↯ (U+21AF), ASCII `_\|_`	Context is logically impossible (empty type, contradiction)	Elaborator / type checker / proof assistant — sometimes a value (`Void`, `Empty`)
Runtime failure as value	Result / `Err`, error-union, handled effect	Computation failed but stayed a term you can match / equate	Evaluator — what belongs on `\|-` once FPL has native error syntax
Diagnostic annotation	`!`, `^` span, caret under source	“Look here in the buffer” — not a term	Printer / UI (today’s `ERROR: l:c …` is closer to this than to ⊥)

Falsum is primarily a static / proof story. Printing ⊥ / _|_ for “out of gas” or “no row matches” would blur runtime with logic. Domain-theory “bottom” (nontermination) is yet another meaning — do not overload that word here.

↯ is a fine later materialization (glyph view / rich TTY) for contradiction / absurdity only; ASCII default for that job stays _|_. Transcript chrome stays ASCII-first, like the ;;! bars. Do not steal FPL ? / _ (holes) for errors.

Two channels for failure

Channel	Shape	Job
Judgment / equate	`\|- ! err/out-of-gas : Error [@ n]`	Fail as a term-shaped line; `!` marks failure; `err/…` is the path tag
Locus + tip	Source line + `^^^^` + Elm-ish prose; optional Clipper face	Point at the span; speak a hint (not a term)

/ in err/… is FPL path namespace (like . elsewhere), not deadline chrome. Deadline stays @ <n>. HTTP status numbers are optional aliases on the banner (e.g. 408 for out-of-gas) — catalog in Errors and diagnostics (02.03.01). Public site today: fpl-lit-scratch.

Diagnostics (Elm tone, Rust spans, Clipper face)

Tone: Elm — human banner, plain “I …”, short hints. Structure (later): Rust / Elm carets under the bad span. Peers: Gleam, Roc (caret + hint). Face: Kakoune’s terminal assistant (Clippy ASCII), not a Kakoune typechecker — we call it Clipper.

Canonical Clipper face (from Kakoune assistant_clippy):

 ╭──╮
 │  │
 @  @  ╭
 ││ ││ │
 ││ ││ ╯
 │╰─╯│
 ╰───╯

Local TTY only (offline for now). Multi-mascot hello/bye chrome lives in the walker REPL, not on the published site. Kakoune-style assistants:

Id	Face	Notes
`clipper`	paperclip above	common
`clipper-smoke`	+ cigarette	rare
`clipper-jonko`	+ joint; eyes `O`/`o`	rare; “peut-être français” is a quip, not a face
`meatdog`	tiny dog	uncommon
`none`	line only	uncommon

One pick per session greets and says bye. Diagnostic Clipper-on-every-error stays deferred. Not a TRPG.

Full error sketch (illustration only — not printed yet)

-- OUT OF GAS ---------------------------------------- err/out-of-gas  408

I ran out of steps before this phrase could finish.

3|  [ 1 drop ] 1000000 repeat
   ^^^^^^^^^^^^^^^^^^^^^^^^^^
The meter hit zero here.

 ╭──╮
 │  │
 @  @  ╭
 ││ ││ │  Immortal Joe is coming for you.
 ││ ││ ╯  Oh boy — you better look out for
 │╰─╯│    your ice cream, Jack!
 ╰───╯

Hint: Lower the loop, raise --fuel, or hitch a ride with meatdog.
|- ! err/out-of-gas : Error @ 1000000

Today the TTY still prints ERROR: l:c …. Wiring this sketch is a later plan.

Cousins at a glance

Family	What they do	Why not exactly the equateable REPL transcript
Rust / Zig / Swift Result, Elm / Roc	Errors as values (`Result`, error unions)	Often type-level; REPL rarely shows an equational `= Err(…)` term
OCaml / SML exceptions	Exceptions are not values until caught	utop prints an exception; you do not equate it as a term
Effect handlers (Eff, Koka, Unison abilities)	Failure is an effect; handlers make it a value again	Close to “error as first-class”; more runtime model than utop line
Idris / Agda / Coq fuel (PLFA gas)	Nat budget so recursion is total	Literal “deadline”; proof technique more than REPL chrome
Granule / graded modal types	Resources in types	Cost-as-part-of-meaning; not a spent-steps printout
Lean `#eval` / `#check`	Commands that print judgments	Close to judgment lines; less “error as equateable value”

“Exceptions as values” is the intuitive label; the sharp variant is errors in the value domain (Result / error-union), not stack-unwinding.

Lineage

Result and error-unions

Rust Result, Zig error sets, Elm / Roc Result: failure is a value you can match and return.

Steal: errors in the value domain, so a transcript can show the same shape for ok and fail once FPL has native error syntax.
Not yet: no FPL error term; TTY failures are still ERROR: … lines, not |- ….

Effect handlers

Eff, Koka, Unison abilities: failure (and other effects) as something a handler can turn back into a value. Eff (Bauer & Pretnar) is the research language that made algebraic effects + handlers programmable with an OCaml-ish surface; Koka and Unison are denser relatives.

Steal: failure as an effect you can handle, not only an exit.
Not yet: no effect system; Eff is a cousin, not a delivery promise.

Effects vs dependent types (sober). Related axes, not the same: value-domain errors are Result-shaped; handlers are a control story that can produce such a value; dependent types can index or refine an error payload. Effect rows and graded modalities track effects in types without full dependent types. FPL has none of this yet.

Restarts and supervision

Erlang supervision, Eiffel rescue/retry, the Common Lisp condition system: recover or restart without pretending the failure never happened.

Steal: a north-star for “gore restart” — recoverable failure in a live system.
Not yet: no design; not a numbered playground part. Open as ambition only.

Fuel, gas, and deadlines

Academic name. A fuel (also gas) argument is a natural-number budget decremented on recursive calls so a definition is total. Classic homes: Coq fuel / Program Fixpoint patterns; PLFA (Wadler / Kokke / Siek) “gas” for interpreters in Agda; the same idea around step-indexing. Idris / Agda totality checkers are cousins (fuel is one decreasing measure). Granule and graded / coeffect systems track how much in types — cost as meaning — without always aborting at runtime.

What FPL did. The walker got a pragmatic step budget so session re-runs cannot wedge forever (feat(eval): bound each run line by a step budget, default 1e6 steps / top-level run line; HOLES.md fuel-scope). The API and bar field stay fuel for now (event.fuel = budget; bar fuel = spent). Gas is the synonym; chrome may say “out of gas.”

Wasteland aside. Mad Max flavour for this corner is welcome in prose and later glyph views — not a new language keyword. Renaming the bar key fuel → gas is a separate feat if someone wants the theme in the TTY.

Steal: spent steps as something you can name next to the result; deadline = that spent count on a future judgment slot (@ <n> chrome preference above).
Not yet: fuel and ms sit on the next ;;! bar only; nothing on |- yet.

Deferred (separate plan)

Do not invent syntax in this note. Locked shapes for later work:

Fail judgment: |- ! err/<tag> : Error [@ n] with path tags under err/ (see 02.03.01). Starter: err/out-of-gas (408), err/no-row (404).
Locus chrome: ^ under the span + Elm paragraphs + Clipper speaking the tip (sketch above).
Deadline on success lines as @ <n>; bar may keep head, &, wall ms.

Until then, the ledger in README.md keeps those promises as deferred.