feat(core): supply the Grate bridge's index — the read stops being forged - #127
Merged
Merged
Conversation
`mfAssocFunction1` sampled the outer rebuild once and broadcast the result, so `grate ∘ iso` collapsed every position onto index 0 — silently, behind a matrix cell that pins typing only. `MultiFocus.tuple`, `representable` and `apply` all tabulate, so the sampled value was wrong for all three. - `Function1BroadcastOptic[S, T, A, B, X0]` is the witness for the one inner kind whose write has exactly one value to build; the kernel writes it per index (`broadcastFrom`) and reads the inner's bundle per index for every inner. - `Z = Xo`: the outer's leftover is threaded through the composition instead of being forged, so the outer's `from` receives what its own `to` produced. - `unobserved[A]` names the two remaining stand-ins (an uninhabited index type, an inner leftover the kernel cannot produce); the class's own `from` is the only index site left and is guarded by the constant-bundle contract. - `MultiFocusFunction1Spec`: positional read/modify/replace across all three Grate factories, the bundle-inner diagonal read, and the previously mis-titled `.andThen` block fixed. - `GrateShapeSpec`: the Naperian sub-shape's 23-cell footprint (6 composing / 18 structural voids), compile-pinned. - QA page: generated Grate sub-table, a legend that states ✓ is a *typing* claim, and carrier-level caveats; `optics.md` + `multifocus.md` cross-link it and the stale `Z = (Xo, Xi)` claim is corrected.
…rged The `Direct → MultiFocus[Function1[X0, *]]` bridge's product must read a bundle it did not build (`Function1BroadcastOptic.from`), and its carrier stores only `Unit`. Baseline 81a53d3d left that read at a `null.asInstanceOf[X0]` sentinel guarded by the constant-bundle contract. - `data.RepresentativeIndex[X0]` — the witness: a real index, with canonical instances for the index types the Grate factories fix with one (`Int` → 0 for `tuple` and `apply` over `Function1[Int, *]`, `Boolean` → false, `Unit` → ()), singletons via `ValueOf`, and `at(i)` for everything else. - `Function1BroadcastOptic` stores `at` and reads there; the bridge's given takes the witness, so `iso.andThen(grate)` stays import-free wherever an instance exists and is REFUSED for an uninhabited index type (there is no index to witness, so the read that has no answer is refused rather than forged). - `unobserved` keeps its two remaining sites, both existential leftovers the write path discards; its docstring now states that neither is an index — an index witness cannot stand in for per-position data. - Spec (13 blocks): the witness read is observable (a varying bundle at 0 vs 1 gives -1000 vs -990, white-box), the shipped path is witness-invariant (round trip + `modify`), `grate ∘ iso` stays positional under a non-canonical witness, an algebraic index bridges via a one-line `given`, an unwitnessed index does not bridge (`typeChecks`), the shipped instances name real values, and the Boolean-indexed cell resolves off the companion. - Docs: `multifocus.md` bridge row + composition-limits paragraph, the generated QA grate legend (script + page kept identical), the `core` row of the agent guide, and a CHANGELOG entry. Design note, measurements and the alternative supplies (cats' `Representable` has no representative index; `ValueOf` does not cover `Int`/`Boolean`) in docs/research/2026-09-30-grate-witness-index.md. Also formats `GrateShapeSpec` (the baseline commit left it non-scalafmt-clean). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Contributor
|
🚀 Cloudflare Pages preview for https://b8292859.cats-eo-docs.pages.dev Branch alias: https://feat-grate-witness-index.cats-eo-docs.pages.dev Built from commit |
Contributor
Benchmark A/BAllocation (B/op) — authoritative
442 more benchmarks
Timing (ns/op) — directional only, same-VM but shared runner
base_sha: |
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.
What this changes
MultiFocus[Function1[X0, *]](the Grate carrier) has exactly one read that no rule of the typesystem can serve: the
Direct → MultiFocus[Function1[X0, *]]bridge's product must turn a writtenbundle
X0 => Bback into aT, and its own carrier stores onlyUnit. That read was anull.asInstanceOf[X0]sentinel guarded by a documented constant-bundle contract. It is now a real,caller-supplied index.
data.RepresentativeIndex[X0](new) — the witness. Shipped instances for the index types theGrate factories fix with a canonical value (
Int→0,Boolean→false,Unit→()), anysingleton type via
ValueOf, andRepresentativeIndex.at(i)for everything else.Function1BroadcastOpticstoresatand reads there;forgetful2multifocusFunction1nowtakes the witness.
unobservedkeeps its two remaining sites — both existential leftovers the write pathdiscards — and its docstring now states the stronger invariant: neither site is an index.
The first commit (
f7065947) is the sibling baseline change "compose the Function1 (Grate)carrier positionally" (source branch
fix/grate-positional-composition, commit81a53d3d),replayed onto
main. It is not onmainand has not been pushed anywhere; the second commitcannot compile without its
Function1BroadcastOptic/ per-index-write kernel work.If you'd rather review them separately I can push the baseline as its own branch and retarget this
PR onto it — say the word.
Behaviour: nothing user-observable changes (measured, not asserted)
Every shipped path hands that
froma constant bundle (modify/replace/collect*map theoptic's own broadcast, and the kernel's fallback passes a constant), so the witness value cannot be
observed through them. The baseline's positional guarantee is also untouched:
grate ∘ isostillrebuilds per index through
broadcastFrom, which needs no index at all.A test pins the read rule itself on a hand-built varying bundle (
-1000at index 0 vs-990atindex 1) — white-box, because outside
eothe carrier's leftoverXis abstract, so a caller cannoteven name such a bundle (
Found: Unit, Required: bridged.X). That is the honest shape of thischange: it makes an unobservable read structural rather than contract-guarded.
Costs, honestly
Composer. Call sites are unchanged forInt/Boolean/Unit/ singleton index types (instances resolve off the companion — still noimports); a grate over an algebraic index needs
given RepresentativeIndex[X] = RepresentativeIndex.at(v).Function1[Nothing, *], a phantom slot):there is no index to witness, so a read that has no answer is refused instead of forged. That is a
capacity regression in an exotic corner, and it is deliberate.
Boolean→falseinstance does privilege a value. Dropping the shippedinstances together is the stricter-consistency option: three composition cells go red and every
caller writes a
given.Relationship to #123 (please read this before deciding)
#123 retired
representableAtbecause "position is a read-time argument, never a property of theoptic" — and its write-up records that giving
repr0runtime meaning would take "a field on theoptic class plus a runtime witness match (the
Function1BroadcastOpticshape)". This PR is thatshape, so it has to be the deliberate exception, not a quiet contradiction:
.at(i)subsumes a factory's index; nothing subsumes the bridge's. Every read of a builtGrate optic is caller-driven. The bridge's
fromis the opposite: the kernel hands it a wholebundle and there is no caller to ask — real value at construction, or forged value at the read.
repr0said"this optic is at this index" (false — two calls built the same optic). The witness says "if you
ever have to read a bundle this optic did not build, read it here" — unobservable on every shipped
path.
If the line's answer is "hold #123's ruling consistently — no index on an optic, ever", then this PR
should be closed rather than merged, and the sentinel stays. Both are recorded in the design note
(§4 for the comparison, §7 for the recommendation with its cost).
Tests / evidence
Design note with the full analysis, the stand-in inventory, the measured candidate supplies
(
Representablehas no representative index;ValueOfdoes not coverInt/Boolean) and thealternative designs:
docs/research/2026-09-30-grate-witness-index.md.core/testOnly dev.constructive.eo.MultiFocusFunction1Spec— 14 examples / 349 expectations:the witness read is observable on a varying bundle; the shipped path is witness-invariant (round
trip equals identity,
modifyunaffected) for two different witnesses;grate ∘ isostayspositional under a deliberately wrong witness (
at(2):(10,20,30) → (11,21,31)); an algebraicindex bridges off a one-line
given; the witness works on refactor(core): retire MultiFocus.representableAt — therepr0index was unobservable #123's own permutedTri/Slotfixture (index order ≠ field order) with
modifystill equal to the instance'smap; anunwitnessed index does not bridge (
typeChecks); the shipped instances name real values; theBoolean-indexed cell resolves import-free.
tests/testOnly dev.constructive.eo.{GrateShapeSpec, CompositionMatrixSpec, UnlawfulFixturesSpec}— 23 / 121 / 4 examples (the
iso ∘ gratecell stays green; no cell moves).scalafmtCheckAll scalafmtSbtCheck benchmarks/scalafmtCheck githubWorkflowCheck mimaReportBinaryIssues test→ green,
scalafixAll --check→ green,sbt doc→ clean (no new scaladoc warnings),docs/mdoc→ 0 errors,docs/laikaSite→ generated.multifocus.md(bridge row + the "carries no constraint"paragraph), the generated QA grate legend (script and page kept in sync), the Grate grid's header
comment in
GrateShapeSpec,mima.sbt(0.19 break entry per the line's convention),CHANGELOG.md,and the
corerow of the agent guide.Not benchmarked, by construction:
MultiFocusCollectBenchdrivesMultiFocus.tupledirectly andnever builds a bridge, so this change cannot appear on that measured path (neither win nor loss).