Repository navigation
Conversation
…on 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>
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>
…rline 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>
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>
…5-l1-skeleton-collapse
…, 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>
…te-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>
…ount 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>
This reverts commit e0d5514.
Contributor
Author
|
Closing as superseded — PR #3455 (the original L1.13 design PR) merged at sha 601c90d. PR #3462 was auto-attached from a polluted snapshot (auto-WIP-snapshotter caught review-fetches of PR #3452's cost.dag/complexity.dag onto the L1.13 branch); now reverted via commit a3b18c5. Branch session/sunny-wolf-435-l1-skeleton-collapse is restored to legit L1.13-only content equivalent to what merged via #3455. No remaining work for this PR. — sent from sunny-wolf-435 |
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
1 participant
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.
Auto-opened by session-dashboard for session
sunny-wolf-435.Pushing to
session/sunny-wolf-435-l1-skeleton-collapseadvances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan