Repository navigation
feat(kernel-utils): join - #1053
Closed
ci-belphegor wants to merge 1 commit into
Closed
ci-belphegor wants to merge 1 commit into
ci-belphegor wants to merge 1 commit into
Conversation
ci-belphegor
force-pushed
the
grypez/narrowing-7-join
branch
from
September 11, 2026 11:42
203b1df to
16c884f
Compare
ci-belphegor
added this pull request to stack #1060
September 11, 2026 11:44
ci-belphegor
force-pushed
the
grypez/narrowing-7-join
branch
from
September 29, 2026 17:37
16c884f to
4c00a4f
Compare
Contributor
Coverage Report
File Coverage
|
||||||||||||||||||||||||||||||||||||||||||||
ci-belphegor
force-pushed
the
grypez/narrowing-7-join
branch
from
September 30, 2026 13:44
4c00a4f to
4284420
Compare
ci-belphegor
force-pushed
the
grypez/narrowing-7-join
branch
from
September 30, 2026 16:18
4284420 to
fe7d3b8
Compare
ci-belphegor
removed this pull request from stack #1060
September 30, 2026 16:44
ci-belphegor
added this pull request to stack #1130
September 30, 2026 16:45
Return a narrowing of the refs' common base admitting whatever any of them admits: the method set is the union of the operands', and where two name the same method each argument position is disjoined. disjoinDeltas sits beside conjoinDeltas as its dual, and the asymmetry is the whole missing-method rule. A join is a union of authority, so its keys are the union of both sides: a method absent from an operand contributes the empty set and survives at the other operand's delta, while a hole contributes everything and leaves that position unconstrained. Narrowing is the opposite, which is why conjoinDeltas takes its keys from one side. The base is a legal operand and absorbs, so the lattice has a representable top and a fold needs no special case. It is recognizable only by identity against a minted ref's record, so a call whose refs are all unminted throws rather than trusting one of them. The result records the same base and the disjoined delta, so a join can be narrowed or joined again. narrow and join now share the minting step, since join needs the same derive-forward-record sequence against a guard it already holds. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
ci-belphegor
force-pushed
the
grypez/narrowing-7-join
branch
from
October 1, 2026 18:38
fe7d3b8 to
b3b283b
Compare
3 of 4 tasks
Contributor
Author
|
Superseded by #1134, which lands the narrowing library as one PR with no stubs. This PR's change is kept as a commit there for review. |
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.
Explanation
join({ name, refs })returns a narrowing of its operands' common base admitting exactly what any of them admits. Variadic; the result's method set is the union of the operands', and where two operands name the same method each argument position is disjoined.Every ref must carry a provenance record naming the same base — a ref the library did not mint throws. That is what makes the operation sound: each operand's guard is
AND(guard(base), X)by construction, soOR-ing the deltas stays ⊆ the base with no pattern subtyping needed.The unnarrowed base is a legal operand and absorbs, contributing
{ method: [] }for every method in its guard. Absorption therefore falls out of the algebra rather than needing a branch.Unmarks one ratchet case.
Notes for reviewers
The missing-method versus hole rule is one rule, not two, because two read as an inconsistency: a join is a union of authority, so a method absent from an operand contributes the empty set (and survives at the other operand's delta), while a hole contributes everything (and leaves that position unconstrained). A position past the end of a delta is a hole.
disjoinDeltassits directly belowconjoinDeltasso the asymmetry is visible: theORdual takes the union of keys, whereasconjoinDeltastakes its keys from one side, because narrowing must not restore authority an intermediate narrowing dropped.One deviation from the design doc, documented in the JSDoc rather than left to be discovered. The doc says the unnarrowed base "is a legal operand and absorbs." It absorbs only in company: the common base is discovered from a minted ref's record, and an unminted ref is recognizable as that base only by identity against it. So a call whose refs are all unminted throws —
refs: []and the degeneraterefs: [base]included. Refusing beats trusting an unminted ref to be a base it cannot confirm; supporting the degenerate case would need a guard fetch for a call that means "copy the base."Probing all four directions rather than just the case's own assertion:
ok:read:srv/logs/y,ok:read:srv/data/x, and rejections for["etc","passwd"]and["srv","logs","..","etc"]againstMust match one of [splitArray([srv,data],…), splitArray([srv,logs],…)].Stack
PR 7 of 12. Base: #1052.