Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 5 additions & 4 deletions ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,8 @@ This window = a few days of STABILITY — shrink the fail-open surface, don't "l
- [ ] **confront the skipped modeling decisions** — the `🟡` comment backlog ([Disposition plan](docs/plans/disposition-carrier.md))
- [ ] **axiom + syllogism lens** (DESIGN open thread #1) — every claim chains back to an axiom, no orphan/cycle; stays `[ ]` until it runs executably over this doc ([scope](docs/plans/axiom-syllogism-lens.md))

## ✦ Ergonomics LANE — make the fold the path of least resistance *(proposed; slots in the §0–§4 stability band, upstream of §0 — bright-stag to number/place)*
## ✦ Ergonomics LANE — make the fold the path of least resistance *(lead lane of the stability band, upstream of §0 — placed bright-stag-194)*
→ [charter: spine + ranked focus](docs/plans/fold-ergonomics.md)

Why a tier: **"it compiles but nothing works" traces to non-fold residue** — a hand-rolled `match` has a
`_ =>` fail-open escape; a fold over a closed coproduct is total by construction and has none. So the chain
Expand All @@ -69,18 +70,18 @@ Guardrail (§6 — ergonomics is the #1 purity-trap magnet): every item **names
friction it retires** (displaced cost), never "cleaner."

**◆ Milestones:** staging/`then_outcome` combinator seeded ✓ (#5512 — compiler front-end de-pyramided to a
stage fold) → **▸ inert-abstraction lens (measure the residue)** → fold reachable by default (the combinators
that stop hand-rolling) → new non-fold residue can't merge (pairs with §0 wall)
stage fold) → **▸ measure the residue (inert-abstraction lens) + fix the root (generic inference)** → fold
reachable *by default* → new non-fold residue can't merge (pairs with §0 wall)

**Audit half — measure the friction + the residue (decidable; wall-able):**
- [ ] **inert-abstraction lens** *(keystone)* — flag any item *defined + self-tested + zero non-test consumers*; generalizes the inert-lens backstop (#5433) from lenses to all carriers. **First RED witness = `Placement` / `Materialization` / `RealizationObjective`** (charter §4: "modeled + witness-passing, no non-test consumer") — a genuinely-inert carrier the lens *fires* on day one, so the lens isn't itself inert (its own §6 guardrail). (`cached_stage` is the *resolved* case — now wired, see Fix half — so it's the worked example, not the witness.)
- [ ] **non-fold-residue audit** — `_ =>` catch-alls over *closed* coproducts · `unwrap_or_default` in inference · hand-rolled recursion where a fold exists. These are the decidable fail-open shapes → §0 wall candidates, not just lenses
- [ ] **fold-friction audit** — what makes the fold awkward to reach (the #5512 pre-state: generic fn-params mis-inferred as kernel `Witness`/`Optional`, forcing typed-param workarounds) — the friction predicts where new residue appears

**Fix half — make the fold the path of least resistance:**
- [ ] **generic-inference fix** *(fix keystone — #1, start here)* — the root that makes the fold reachable *by default*, not just reachable; collapses a fan-out of hand-rolls (`qualified_name` trio · `ParseTable` · `cached_stage` indirection) and is the prereq for §0's realization-grounding (~120 `Value` bridges become a fold, not a 131-site grind). Dissolve-on `feature:free-monoid-entry-generic-inference` ([charter](docs/plans/fold-ergonomics.md) §3)
- [ ] **generalize the staging combinator** — `then_outcome` (Kleisli for the `Outcome` monad) seeded the pattern (#5512); lift it to the standard way to compose fail-closed stages, so a pipeline is a fold of typed stages, not a `bind_outcome` pyramid
- [ ] **wire the seams, don't strand them** — an abstraction lands *consumed* or scaffold-marked with a dissolution trigger ([construction-justification rule](docs/plans/construction-justification-rule.md), #5476). Worked example (the full arc): `cached_stage` seeded inert (#5512) → caught by the keystone lens → wired with a `Miss`-stub wrapping `stage_resolve`. **Boundary:** this lane owns only that the seam *lands consumed-or-marked*; **§1/§2 own *enabling* the resolve-cache** (the realization work) — one home each.
- [ ] **fold ergonomics in the type system** — fix the inference friction the audit surfaces so the typed-param workaround isn't needed (composes with §0's fail-closed-inference work)

**Own runway — down-ranked (the lane's §6 guardrail applied to its own scope):**
- [ ] **ban source comments** (`.dag` + `.rs`) — *separate runway, sequenced BELOW the fold items.* Orthogonal to folds (it's documentation-hygiene), load-bearing (grammar `02_parse`/`syntax`), and the item most likely to swallow the lane. Displaced cost: reviewer reads multiples of the real diff (a comment-heavy `.dag` fn is ~10% code) + LOC inflation; that's the pain, not "cleaner." Construction arc: model the live-state survivors → migrate → **delete the rest aggressively** (git is the backup) → **parser refuses free `//`** (§5, lands LAST). *(calm-seal-13: pilot CI-gate files → fan out → wall; deletion has no modeling-blocker — no gate text-scans comment bodies)*
Expand Down
100 changes: 100 additions & 0 deletions docs/plans/fold-ergonomics.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,100 @@
# Plan — fold ergonomics: make the fold the path of least resistance

**Status:** charter + ranked focus · **DESIGN.md + the carriers remain the authority** (DESIGN §6). A
task's real state is its branch/PR, not this file. Linked from `ROADMAP.md` ✦ *Ergonomics LANE*.

**Carrier facts below were gathered by two tree-wide sweeps (fold inventory + non-fold-residue/friction),
2026-06-22. Re-grep the live counts before acting — they rot.**

---

## 0. Thesis — "it compiles but nothing works" traces to non-fold residue

A hand-rolled `match` carries a `_ =>` fail-open escape; a fold over a *closed* coproduct is total by
construction and has none. So the causal chain is **ergonomics → adoption → fail-closed**: when the fold
is awkward to reach, people hand-roll, and every hand-roll reintroduces a fail-open arm. This lane
**stops new residue by making folds ergonomic**; §0's fail-open-shape walls **retire the old**. The two
together drain the [model↔realization fork](model-realization-fork.md), the residue's deepest instance.

Guardrail (DESIGN §6 — ergonomics is the #1 purity-trap magnet): every item **names the fail-open class
or measured friction it retires** (displaced cost), never "cleaner."

## 1. The spine is already real (accomplishments, with receipts)

The fold is not aspirational here — it is the actual architecture, at scale:

- **`fold_node`** (`src/v2/std/node.dag:228`) — one catamorphism, **69+ call sites across 7 stages**
(translate 43, eval 12, name_resolve 7, infer 3, resolve 2, compile 2). Traversal is not re-coded per
stage; operations come from *inhabitance*, not per-type op lists (DESIGN §4/§6).
- **`bind_outcome`** (`src/v2/std/diagnostic.dag:225`) — **246+ sites** (translate 172, eval 31, compile
31, ingest 12). The `Outcome` railway monad is the genuine spine, not a demo.
- **`coercion_fold`** (`src/v2/std/coercion.dag:279`) — **50+ sites**, *one* procedure asked three
directions (ingest-forward / emit-inverse / homomorphism check) via the same `find_witness`
catamorphism. The **model-side coercion fold is already built** (this reframes any "build the coercion
fold" framing — see Root A).
- **#4699** — `06_translate` de-accumulated: 4,912 → 3,973 lines, `_go` accumulators **35 → 0**. The
single largest "stop hand-rolling recursion-with-accumulator" receipt in the tree.
- **#5512** — front-end de-pyramided: `compile_ingest_staging` went from a 5-deep `bind_outcome` pyramid
to a fold of five first-class typed stages under **`then_outcome`** (Kleisli for the `Outcome` monad);
`cached_stage` wired live (seam consumed, not stranded). The seed this lane names.
- **#5428 / cardinality P4** — numeric tower grounded fail-closed; cardinality propagates through folds
as a homomorphism, uint8 overflow → typed `Rejected`. A model↔realization fork instance *closed*.
- **`merge_envs`** — a 6-line root fix cut reconcile from 81% → 6% of the pipeline (~2× self-compile).
The canonical "fix the language layer, not the symptom" win — the lane's whole thesis in one diff.

## 2. The diagnosis — two roots, the lane's two halves

**Root A — the realization side isn't folded (the fail-open).** The model side folds; the Rust `Value`
enum is reconciled by **~120 per-site `_ => false` bridges** — `Value::eq` (`v1_interpreter.rs:707`),
binop coercion, 63 inference mismatches, 91 in `complexity.rs`. A modeled coproduct (`Nat = Zero|Succ`)
vs its native realization (`Int`) is compared per-site, and a miss is a *silent false*
(`nat_add(85,32) == 117` → `false`). This is DESIGN's model↔realization fork, and it is where wrong
answers actually hide. The deepest remaining instance is the **`Value::Null` split**:
`Optional`/`Witness`/miss overloaded onto one sentinel across **~131 sites** — it resists a blanket
guard because it *is* a fork, so it needs grounding, not an error arm.

**Root B — generic inference is weak, so the fold is awkward to reach (the friction).** Two concrete
failures:
- generic fn-param results mis-infer as kernel `Witness`/`Optional` → must route through a typed param
(the `resolve_probe` workaround in `staging.dag`; same in `target_model.dag`);
- generic type-alias instantiation fails — `type QualifiedName = FreeMonoid<Symbol>` won't define
("variant not found in type `FreeMonoid`") → **55 lines of hand-rolled `qualified_name_eq`/`for_all`**
(`qualified_name.dag:25–57`), and it is the *same* root that makes v2 still hand-roll `ParseTable`.

Root A is the fail-open class the lane retires; Root B is the friction that keeps producing it.

## 3. Ranked focus (displaced cost named, per the §6 guardrail)

**#1 — fix generic inference** *(fix keystone — the root with measured fan-out)*. **Retires:** the
typed-param-workaround tax and the `FreeMonoid<Symbol>` block. One well-scoped inferencer change collapses
a fan-out of hand-rolls — `qualified_name`'s trio → `fold_list`/`==`, `ParseTable` → the Realization
carrier, the `cached_stage` indirection → a plain inline match. This is the literal "make the fold the
path of least resistance": today the fold is reachable but *taxed*; after this it is reachable *by
default* — the only item that changes the default, which is the whole point of an ergonomics lane.
Dissolution trigger already exists (`feature:free-monoid-entry-generic-inference`); a root fix, not a
grind. **Prerequisite for #2** (makes the realization grounding expressible as a fold, not a 131-site
hand-grind).

**#2 — ground each primitive into its realization** *(highest safety / displaced cost)*. **Retires:** the
~120 silent-`false` `Value` bridges. Make the straddle *unwritable* — native form `==` modeled form by
construction, so the per-site arms disappear (exactly what #5428 did for the numeric tower, fail-closed).
The deep sub-root is the `Value::Null` split (~131 sites, own runway). The safety axis literally: every
silent `false` is a deferred bug paid later at interest.

**#3 — the lens backstop** *(cheapest gate; gates #1/#2 so new residue can't merge)*. The
**inert-abstraction lens** (generalize the inert-lens backstop #5433 from lenses to *all* carriers — flag
*defined + self-tested + zero non-test consumers*) and the **non-fold-residue audit** (`_ =>` over closed
coproducts · `unwrap_or_default` in inference · hand-rolled recursion where a fold exists). A pure reader
over the same `Node` tree (zero substrate edits). Decidable, wall-able. First RED witness =
`Placement`/`Materialization` (a genuinely-inert carrier — *not* the now-wired `cached_stage`, so the lens
isn't itself inert).

**Start with #1.** It is the most elegant (a root with measured fan-out), it is the prerequisite that
makes #2 a fold instead of a grind, and it is the only one that changes the default.

## 4. Dissolution trigger (DESIGN §6)

Delete this doc when the fold is reachable by default — generic inference no longer forces typed-param
workarounds (Root B closed), the realization side grounds into the model with no per-site `_ => false`
bridges (Root A closed), and the inert-abstraction lens gates new residue on the floor. At that point the
absent residue + the green lens *are* the authority and this charter is redundant.