diff --git a/ROADMAP.md b/ROADMAP.md index e5fd0b9c3a0..40abc60911e 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -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 @@ -69,8 +70,8 @@ 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.) @@ -78,9 +79,9 @@ that stop hand-rolling) β†’ new non-fold residue can't merge (pairs with Β§0 wal - [ ] **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)* diff --git a/docs/plans/fold-ergonomics.md b/docs/plans/fold-ergonomics.md new file mode 100644 index 00000000000..c3f6c14d7c1 --- /dev/null +++ b/docs/plans/fold-ergonomics.md @@ -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` 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` 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.