Repository navigation
modeling-discipline: add Practice 11 — parameterize, don't duplicate + concept-home boundary - #3444
Merged
Merged
Conversation
…+ concept-home boundary The Pass A/B unification (PR #3443) caught a recurring carrier- duplication / parametric-pair pattern that no existing practice named. Every Pass A/B correction and every Wave-1 worker correction had the same shape underneath: two (or more) operations / carriers / witnesses declared as distinct, where one parameterized declaration would have done — the difference was always a typed parameter (predicate, domain, policy, structural property). Existing practices catch the implementation-time symptoms: - Practice 4 (Coproduct dissolution) — flat enum with parametric structure - Practice 5 (Single-authority metadata) — one fact one location - Practice 10's 'carrier dissolution' — local coproduct cloning a std/ carrier None of them catch the design-time cause: a domain-named declaration in the design doc that's actually a parameterization of an existing primitive. That gap is what seeded Worker A/B/C with mis-shaped briefs in Wave-1. Practice 11 (NEW) names the meta-pattern. Two sub-rules: 11a — Parameterize, don't duplicate Before authoring a new operation, carrier, or witness, exhaust 'is this a parameterization of an existing one?' Worked examples (drawn from real v4 corrections): - solve_constraints + coercion_fold + LawfulRewriteWitness → find_witness(_, _, predicate, multiplicity_policy) - 7 named witnesses → 3 generic carriers (StructuralPropertyWitness<P>, HomomorphismWitness<R>, PromotionWitness) - 3 MVP terminuses → 1 MVP - traverse_node etc as primitives → derived combinators over fold_node - ProgramSchedulingEdge / TargetPlanSchedulingEdge / ArtifactSchedulingEdge → one DependencyEdge with a DependencyKind label - DependencyGraph as separate carrier → Edge-on-Node parameterized by DependencyKind (carrier dissolves entirely) - TopologicalPlan as authored ledger → lens output that folds over Node (no parallel ledger) 11b — Concept-home boundary discipline Before adding a field to a substrate file, confirm the field doesn't cross a boundary the file's identity is supposed to keep separate. The canonical violation: NodeFileBinding in extdeps/file_system.dag (extdeps shouldn't know about Node; Node↔File provenance belongs in artifact/projection/ingest). Both sub-rules apply at the design-PR / brief-authoring layer — they catch errors that propagate as N file-scale violations across every worker the brief dispatches. The cheapest fix point is the design PR. Updates: - 'Ten Modeling Practices' → 'Modeling Practices' (open-ended; was miscounting after Practice 11) - New entry in the Practice → invariant mapping bullet list - Practice 10's 'carrier dissolution' sub-case cross-refs Practice 11 for the parametric generalization - New Practice 11 section between Practice 10 and the Calibration section, with the two sub-rules + worked-examples tables + standard 🔴/🟡/🟢 dispositions - Calibration section: explicit 'Practice 11 findings are always BLOCKING at the design-PR layer even when no implementation hunks exist' - For Reviewers: new step 11 — design-PR review applies Practice 11 per declaration, with required 🔴/🟡/🟢 disposition Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 20, 2026
Closed
briansrls
added a commit
that referenced
this pull request
May 21, 2026
…n; Practice 11's runtime-symptom catcher; 3 real-corpus findings cited) (#3455) * design: L1.13 skeleton-collapse lens — kills parametric-arm duplication via constructor-name template L1.13 catches the runtime symptom of Practice 11 (just landed in #3444) parametric duplication at the match-arm level: matches whose RHSes collapse to K << N distinct skeletons under α-renaming + constructor-name substitution. Distribution-shape classifier: - PureTemplate (K=1): dispatch doing zero work - Outlier (K=2 with 1:N-1): predicate-factor - Categorical (K small, multi-group): push categorization into the coproduct's type definition - Mixed (K close to N): legitimate per-variant dispatch Sibling-of L1.1: where L1.1 catches Bool-returning matches with literal true/false arms, L1.13 catches non-Bool matches with constructor-name templating across arms. Operator-direct 2026-05-21 — first lens shipped under the "every lens demonstrates value at PR time" discipline. Three real-corpus findings cited in PR body (F14 feature_disposition, F15 PR #3452 complexity_bound_from_class, F16 manual_test_claim_for_manual_anchor). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * design: L1.13 — add §5.0 theme + §5.1 acceptance-key registry rows Address briansrls inline BLOCKING on #3455:1085 — L1.13 was added without updating the §5.0 lens→theme catalog or the §5.1 canonical acceptance-key table. Those are single-authority registries downstream consumers (e.g. src/v4/lens/coverage.dag) depend on; adding a lens without the registry rows leaves them orphaned (INVARIANTS P2 violation). Added rows: - §5.0 theme catalog: L1.13 Skeleton-collapse | derive / canonical-home - §5.1 acceptance-key: L1.13 | coverage_defect_skeleton_collapse Theme rationale: 'derive' captures L1.13's core (parametric-arm duplication is hand-rolled derivation of a categorical projection); 'canonical-home' captures the Categorical dissolution (push the categorization into the input coproduct's type definition, its canonical home). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.13 — remove advisory verdict tier; reclassify F16 as borderline Address briansrls inline BLOCKING on #3455:1109 — L1.13's verdict line created an "advisory" tier for fixtures / data tables, contradicting the universal three-disposition rule (🔴/🟡/🟢, "there is no fourth") from §5.0 / Practices 4 + 10. Fixes: 1. Verdict simplified to "hard error (🔴 dissolve-now)" with explicit note that no fourth tier exists. 2. Escape clause expanded to absorb the legitimate exceptions cleanly: - Per-arm distinct literal data (test fixtures, data tables) is Mixed under skeleton extraction → passes naturally as clean 🟢 - Distinct call arguments per arm is also Mixed for the same reason 3. F16 (manual_test_claim_for_manual_anchor) reclassified from "Outlier" to "Borderline case" — under the strict decidability rule the per-arm `claim_<name>` references are distinct free literals (K=N, Mixed). Catching F16 requires either a sub-signature L1.13.b (future) that detects per-arm-named-reference parameterization, or a separate "match-as-typed-table" lens. F16 stays in the doc as a related-pattern example for boundary clarity, NOT as a current L1.13 kill. Net: L1.13 stays clean against the three-disposition rule; F14 + F15 remain valid findings; F16 is honestly documented as out-of-current-scope. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.13 Outlier dissolution — fix L1.1 contradiction Address briansrls inline BLOCKING on #3455:1120 — the original Outlier dissolution path advised "extract a named Bool helper / sibling lens finding (L1.1 territory)," which is EXACTLY the L1.1 predicate-dissolution anti-pattern (Bool-returning fn over a coproduct with literal true/false arms per variant). Corrected dissolution path: - Consume the discriminator structurally via match patterns + guards on the existing coproduct, OR substructure the coproduct so the one-vs-many distinction is a top-level variant. - Function body becomes a 2-arm match: `match x { <Special_pattern> => special; _ => default }` with the discriminator as a sub-pattern or guard. - DO NOT extract a named Bool helper — explicit prohibition with citation to L1.1's signature. Recent precedent updated: PR #3359 connective_spec_fact was resolved via inline match-pattern with guard, NOT a Bool helper. L1.13's "extract a discriminator" reflex must satisfy L1.1 as well as itself — the discriminant is structural (substrate-known from the parsed match), not a hand-rolled helper. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.13 — tighten classifier thresholds, identity source, scope, clearing receipts Address operator discussion review on PR #3455 (6 points). All 6 addressed as fix-forwards: 1. Exact classifier thresholds. Distribution shapes now have precise definitions: - PureTemplate: K=1, histogram=[N] - Outlier: K=2, histogram=[N-1, 1], N≥3 - MultiOutlier (NEW): K≥2 with singletons + non-singletons, N≥4 — covers F14 (1:5:6) and F15 (1:1:7) which were misclassified as Categorical - Categorical: K≥2 with non-singleton-only groups, K≤⌊N/2⌋, N≥4 - Mixed: doesn't meet above thresholds 2. Skeleton substitution precision. The rule now states explicitly: replace EVERY occurrence of the matched-arm constructor identity in the RHS (not just the leading RHS constructor); α-rename pattern-bound names; do NOT collapse unrelated free names, literals, or call arguments. 3. Canonical-identity source. Lens consumes post-resolve/InferredTree canonical identities, not raw source spelling. Qualified names, imports, aliases, renamed bindings resolve to canonical identity before skeleton comparison. 4. Coverage key marked reserved-proposed. §5.1 row for L1.13 now flags "(reserved-proposed — enforcement not active until skeleton extraction + classifier + clearing receipts land)." 5. TotalMap scoping. Moved the substrate-dependency note to scope TotalMap to L1.13.b / future match-as-typed-table lens, NOT base L1.13. Base L1.13 (PureTemplate/Outlier/MultiOutlier/Categorical on F14+F15) has enough substrate today via fold_node + skeleton extraction; does NOT need TotalMap to fire or clear. 6. Clearing receipts explicit per shape. Each distribution shape's dissolution entry now includes a "Clearing receipt" sentence stating what receipt closes the finding. Categorical/MultiOutlier explicitly forbid "category_of(x): Category" hand-rolled projections (would just move the L1.13 violation to a new name). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: PM * design: L1.13 — add Fix-confidence axis per dissolution; cite candidate-state auto-fix flow Address operator framing: "every diagnostic can generate the correct code solution (and eventually apply it) — assuming intent is safely inferable." Each distribution shape now carries an explicit Fix-confidence field stating whether the auto-fix is: - DIRECT — Diff fully specified, no naming decisions: - PureTemplate: replace match with single shared RHS - Outlier: rewrite N-arm match to 2-arm (singleton arm + uniform catch-all) - TEMPLATED — Diff with name-holes reviewer can override: - MultiOutlier: substructure type (singleton variants + wrapping variant + sub-coproduct); default names derived from existing constructors (e.g. F14 "Modeled" + uniform group → "ModeledFeature" + "ModeledKind") - Categorical: same templated-name pattern - STRUCTURAL SKETCH (future sub-signatures only): lens identifies transform kind; concrete Diff requires human design Added top-level framing paragraph citing the §6 (find, transform) convolution view and PR #3364's candidate-state mechanism (candidate_dag = apply_diff(dag, Diff) → gate → commit if green). The fix-confidence axis is what makes L1.13 actionable rather than just diagnostic. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: L1.13 — fix F14/F15 classifier inconsistencies; clarify arm-count framing Address cursor REQUEST_CHANGES on #3455: 1. F14 concrete-match label was "Categorical, 1:5:6" — inconsistent with the Kills line + MultiOutlier section + classifier definition. Per the classifier, Categorical requires non-singleton-only groups; 1:5:6 has a singleton (Modeled arm) → MultiOutlier. Fixed: "Categorical, 1:5:6" → "MultiOutlier, 1:5:6" with inline justification referring to the classifier definition. 2. F15 concrete-match label was "Categorical, 1:1:7" — same inconsistency. 1:1:7 has two singletons (Constant, Unknown) → MultiOutlier. Fixed analogously with inline justification. 3. F15 "9 arms to 4" exploratory observation — the clean shape's outer match has 3 arms (ClassConstant, ClassUnknown, `_`); the "4" was counting the inner 2-arm match inside the `_` branch (3 outer + 1 inner-distinct = 4 if flattened, but the structurally meaningful reduction is 9 → 3 at the outer dispatch). Clarified the framing. Root cause of inconsistency: when I introduced MultiOutlier as a distinct shape from Categorical in commit 917942a, I updated the Kills line and the shape's definition but missed updating the F14/F15 concrete-match labels at the bottom of the section. Mechanical consistency restored. P2 (single classifier authority) + P4 (decidability) now hold across classifier definition / Kills / concrete-match labels. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
The Pass A/B unification (PR #3443) caught a recurring carrier-duplication / parametric-pair pattern that no existing modeling practice named — every Pass A/B correction (
solve_constraints+ coercion fold +LawfulRewriteWitness→find_witness; 7 witnesses → 3 generic carriers;BootstrapWitness+FixedPointWitness→PromotionWitness; etc.) had the same shape underneath: two or more operations/carriers/witnesses declared as distinct, where one parameterized declaration would have done.Every Wave-1 worker correction (PRs #3439 / #3440 / #3441) had the same shape downstream — the briefs encoded domain-named "primitives" the workers faithfully implemented, then the unification caught them at review.
The existing practices catch the implementation-time symptoms:
std/carrierNone of them catches the design-time cause: a domain-named declaration in the design doc that's actually a parameterization of an existing primitive. That gap is what seeded Worker A/B/C with mis-shaped briefs.
Practice 11 (NEW) names the meta-pattern.
What Practice 11 adds
Two sub-rules, both applying at the design-PR / brief-authoring layer:
11a — Parameterize, don't duplicate
Worked examples (drawn from real v4 corrections in PR #3443):
solve_constraints, coercion fold,LawfulRewriteWitnessfind_witness(facts, candidates, predicate, multiplicity_policy)CanonicalGroundingWitness,AcyclicityWitness,ClosedWorldDependencyWitnessStructuralPropertyWitness<P>PWitness<homomorphism>,LawfulRewriteWitnessHomomorphismWitness<R>RBootstrapWitness+FixedPointWitnessPromotionWitness(composed gate)traverse_node,sequence_node,bind_outcomeas primitivesfold_node+ Outcome-threading algebraProgramSchedulingEdge,TargetPlanSchedulingEdge,ArtifactSchedulingEdgeDependencyEdgewithDependencyKindlabelDependencyGraphseparate carrierDependencyKindTopologicalPlanas authored ledgerfold_nodeover Node)11b — Concept-home boundary discipline
Canonical violation:
NodeFileBindinginextdeps/file_system.dag— extdeps shouldn't know aboutNode; Node↔File provenance belongs in artifact/projection/ingest.Why this is design-time meta-practice
Practices 1–10 are file-scale — a reviewer reads one diff and checks whether the diff conforms. Practice 11 is design-scale — a reviewer reads the brief that produced the diff and asks whether the brief itself names duplicates as primitives.
A Practice 11 violation in a design doc propagates as N file-scale violations across every worker the brief dispatches. The cost is asymmetric: catching it in the design doc deletes the violation once; catching it after dispatch costs N rounds of corrections + N worker contexts that need to be re-briefed.
Changes
## Ten Modeling Practices→## Modeling Practices(was miscounting after Remove node override mocking mechanism from test framework #11)carrier dissolutionsub-case cross-refs Practice 11 for the parametric generalizationPure docs change. No code touched. No
src/v4/paths.Test plan
Ten Modeling Practicesreferences — none should remaincarrier dissolutioncorrectlyAnchor
Drawn from the Pass A/B unification (PR #3443) corrections + Wave-1 worker analysis (PRs #3439 / #3440 / #3441). All worked-example rows are real corrections, not hypothetical.
🤖 Generated with Claude Code