types/rtti/data: make tuples open - #1680
Conversation
`toData` mapped a `Tuple` to `{ prefix }`, which the data form reads as an
exact length, while `parse` and `validate` treat tuples as open. The same
schema therefore gave two answers depending on which reader consumed it.
`toData` now maps a `Tuple` to `{ prefix, rest: unknown }`, and
`arraySetValidate` reads a position past the array's end as `undefined` —
the rule the object side already applies to keys — so a position is required
exactly when its set excludes `undefined` and no minimum length is tested
for. `../validate/proof.f.mjs` runs its acceptance table through the data
form as well, so the three readers cannot drift apart again.
Changelog:
- **BREAKING CHANGES:** `types/rtti/data`: `toData` maps a tuple schema to the
open `{ prefix, rest: unknown }`, matching `parse`/`validate` acceptance;
`{ prefix }` alone is now the exact-length set. Tuples render with a rest
element (`readonly[42,...readonly(unknown)[]]`) and as JSON Schema with
`items` rather than `items: false`.
Deploying with
|
| Status | Name | Latest Commit | Preview URL | Updated (UTC) |
|---|---|---|---|---|
| ✅ Deployment successful! View logs |
functionalscript | e7b9d19 | Commit Preview URL Branch Preview URL |
Aug 24 2026, 12:05 PM |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b644c6fa3f
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
…sitions Two consequences of open tuples, both found by the review bot on #1680. `[unknown]` and `[]` are both every array, but only the second normalized to `{ array: true }`, so one set had two spellings and `equal` said false. `arraySet` now drops a trailing position stating exactly its `rest`, when the `rest` admits `undefined` — without that proviso the two differ on a present `undefined`, so `{ prefix: [number], rest: number }` stays "one or more". `toTs` printed a trailing position the array may end before as required, so the emitted TypeScript rejected `[]` for a schema that admits it. It now prints those positions optional, as the object side already prints the key they are the counterpart of.
o2alexanderfedin
left a comment
There was a problem hiding this comment.
The change itself verifies clean — the acceptance divergence is fixed, arraySetSubset is sound, and the mutation coverage is real. One correction:
fjs/types/rtti/data/module.f.mjs:294-296 — the stated reason for the trim guard is inverted. "Without that proviso the two differ on a present undefined, which only the position admits" is not what the code does: { prefix: [number], rest: number } rejects [undefined] (position 0 reads undefined, which number excludes), and so does { prefix: [], rest: number }. Exhausting all arrays of length <= 3 over {undefined, 1, 'a', null}, the sole value the two spellings differ on is the empty array — { prefix: [], rest: number } admits it, { prefix: [number], rest: number } does not. That absent case, not a present undefined, is what makes the untrimmed pattern "one or more numbers". The guard is right; only its justification is backwards. The same sentence is in the PR body and in the reply to the Codex comment. Note data/proof.f.mjs:476-478 already states it correctly ("a position restating a rest that excludes undefined … is what makes this 'one or more'").
The guard was right, its stated reason inverted. The two spellings do not
differ on a present `undefined` — `{ prefix: [number], rest: number }` rejects
`[undefined]`, position 0 reading a value `number` excludes, and so does
`{ prefix: [], rest: number }`. They differ on exactly one value, `[]`: the
arrays that stop before the position are the ones it reads `undefined` at, and
the `rest` alone imposes nothing there. That absent case is what makes the
untrimmed pattern "one or more numbers", as `data/proof.f.mjs` already said.
Reported by @o2alexanderfedin on #1680.
|
@o2alexanderfedin you're right, and thank you for exhausting it rather than eyeballing it. I reproduced it: over The guard stands; only its justification was inverted. Corrected in f8f560c:
The same sentence is fixed in the PR body, and I left a correction on the Codex thread where it also appeared. Generated by Claude Code |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f8f560c5ca
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
The extra-entry filter tested `Number(k) >= pn`, which is false for a
non-index key — `Number('foo')` is `NaN` — so an enumerable property on an
array was dropped from validation entirely. `parse` and `../validate` walk the
value's entries rather than its length and hold `foo` to the element type, so
the data form accepted what they reject, which is the parity this branch
exists to restore.
The filter now keeps every entry the prefix has not declared, non-index keys
included, and the no-`rest` case rejects on that same set rather than on
`value.length` — the exact-length pattern's "nothing past the prefix" now
covers a non-index key too, where the previous reading of it panicked on an
absent `rest`.
Reported by the Codex review bot on #1680.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 0beaf25bbf
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
`Number(k) < pn` treated any key coercing into the prefix range as a declared position, so `'-1'` was skipped from validation entirely — accepted by the data form, rejected by `parse` and `../validate`, the parity break again — and `'01'`, `'1.5'` and `' 1'` were skipped by any pattern with a long enough prefix. `arrayIndex` rounds the number back through `String` and compares it against the key, which rejects every non-canonical spelling at once rather than one at a time: only the canonical spelling of a non-negative integer names a position, and everything else is a property of the array object, held to the `rest` like an index past the prefix. Reported by the Codex review bot on #1680.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b7654185a9
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| const extra = Object.entries(value).filter(([k]) => { | ||
| const i = arrayIndex(k) | ||
| return i === undefined || i >= pn | ||
| }) |
There was a problem hiding this comment.
Skip unconstrained tuple extras before enumerating them
For an open tuple, rest is unknown, so extra entries cannot affect validation, but Object.entries(value) eagerly reads every enumerable value before filtering or validating it. Consequently, an array with a throwing enumerable getter on an undeclared property succeeds under both validate([number]) and parse([number])—which ignore extras—but validate(toData([number])) throws while reading that getter. Avoid enumerating values when the rest is unconstrained (and filter keys before retrieving values) to preserve the promised reader parity.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
The divergence is real, but I'm not changing it in this pull request, and leaving this thread open for @sergey-shandar to decide.
It predates the branch. I ran the same input against 002b819's data/module.f.mjs and this branch's, side by side — [1] with a throwing enumerable boom getter, schema [number]:
parse([number]) ok
validate([number]) ok
data BEFORE this PR THREW: read
data AFTER this PR THREW: read
The pre-branch arraySetValidate also called Object.entries(value) unconditionally, after its length check, which [1] passed. So the getter was read before this branch and is read after it; nothing here made it reachable.
Two further reasons to leave it. The value is outside the model — FunctionalScript values are plain immutable data, and a property that throws on read is not one, so no proof could construct it without reaching outside the subset the repository type-checks. And Object.entries(value) on the value is what parse and validate themselves do for array/record schemas, so skipping it only for a top rest would make the data form quieter than the readers it is supposed to agree with, in one shape and not the others.
If it is worth fixing, it is worth fixing as its own change — a todo/ file under fjs/types/rtti/todo/, covering all three readers rather than this one branch of one of them, since the repository tracks issues as files next to the code. Happy to write it up; I'd rather not widen a pull request whose subject is tuple openness.
Note also that this is the third finding on this one function in three rounds, each reshaping the last. The first two were real regressions from this branch and are fixed; this one is not from this branch. I'm stopping bot-driven changes to arraySetValidate here rather than iterating further.
Generated by Claude Code
o2alexanderfedin
left a comment
There was a problem hiding this comment.
Re-verified at b7654185. The rewritten trim justification checks out: exhausting 1,477 arrays (length <= 3 over {undefined, 1, 0, -0, NaN, 'a', null, true, 1n, [], {}}, plus sparse and odd-key variants) leaves [] as the only dense witness separating { prefix: [number], rest: number } from { prefix: [], rest: number }, and [undefined] is rejected by both — exactly as the new text says.
The non-index-key change and its arrayIndex follow-up close the parity gap: a 1,932-pair parse / validate / data-form differential over arrays carrying '-1', '-Infinity', '01', '1.5', ' 1', '1e0', '', '-0', 'foo' and holes now shows 0 disagreements, against 42 at 0beaf25b (all the negative-key class). Five mutations of arrayIndex and the filter each redden data/proof.f.mjs's arrays or validate/proof.f.mjs's sameAcceptanceInTheDataForm; arraySetSubset stays sound over 90,601 pattern pairs x 22 values including those keys; gates green (tsc clean, 3107 tests, cov 100/100/100, ci-update idempotent).
One nit, non-blocking: "differing … on exactly one value, []" holds for dense arrays only — an array with a hole at index 0 ([ , ], [ ,1]) also reads undefined there and so separates the two spellings.
"Exactly one value, `[]`" held for dense arrays only. An array with a hole at
the position reads `undefined` there just as one ending before it does, so it
separates `{ prefix: [number], rest: number }` from
`{ prefix: [], rest: number }` the same way: `[ , 1]` belongs to the second
and not the first. The distinction the guard turns on is "nothing at that
position", not "the array stopped".
Reported by @o2alexanderfedin on #1680.
|
Thanks for the re-verification, and the nit is right — fixed in a92b585. Reproduced it:
Since the push resets your approval: the diff since The one thread still open is the throwing-getter enumeration, which I left for you deliberately: it reproduces identically at Generated by Claude Code |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: a92b585c56
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Replacing the `value.length` test with an entry test lost the bound for a
sparse array: `[1, ,]` has length 2 and one entry, so `{ prefix: [number] }`
accepted it where it had rejected it before, and `array(never)` accepted
`[ , ]`. A hole past the prefix is not an entry, but the array is still that
long, and this is the set `Ts<>` renders as a tuple of exactly `pn` positions
and JSON Schema as `items: false`.
The no-`rest` case now tests both: no undeclared entry, non-index keys
included, and no length past the prefix. A shorter array is unaffected — the
declared loop has already held every position it leaves unfilled to a set
admitting `undefined`.
Reported by the Codex review bot on #1680.
o2alexanderfedin
left a comment
There was a problem hiding this comment.
The length bound is back and correct. extra.length === 0 && value.length <= pn restores exactly what main enforced for the no-rest arm, and both halves of the && are load-bearing: dropping the length test reddens validate.arrays on vx([1, , ]), dropping extra.length === 0 reddens it on the non-index key, and <= → < reddens on vx([1]). <= rather than === is the right call and the renderers pin the reasoning — dataToTs prints { prefix: [option(string)] } as readonly[(undefined|string)?] and toJsonSchema as items: false with no minItems, both of which admit the shorter array the declared loop already cleared; the comment's Ts<>/items: false claims check out (TupleTs is a mapped tuple of exactly pn positions, and arraySetSchema emits items: false iff rest === undefined).
The three readers still differ on one family — an all-holes array against array(never) (and option/or wrappers of it): parse and validate say ok, the data form says error. That is byte-identical to main's behaviour, it is the pre-existing hole-blindness in the entry-walking readers rather than anything this PR introduced, and the data form is the reader that is right there, so it is not a regression of the PR's goal. tsc, 3107 tests, cov (100%/exit 0) and ci-update (clean tree) all pass.
toDatamapped aTupleto{ prefix }, which the data form reads as an exactlength, while
parseandvalidatetreat structs and tuples as open. The sameschema gave two answers depending on which reader consumed it:
The divergence was arrays-only — struct keys already agreed, the two kinds
normalizing an absent
restagainst opposite identity elements. Fixesfjs/types/rtti/todo/data-form-open-tuples.md, deleted here.What changed
toDatamaps aTupleto{ prefix, rest: unknown }. An open tupledeclaring nothing is therefore the whole array kind, which is what
validate([])already accepted.arraySetValidatereads a position past the array's end asundefined—the rule the object side already applies to keys — so a position is required
exactly when its set excludes
undefined, and no minimum length is testedfor. What is left over is tested against
rest, non-index keys included, or,with no
rest, must not be there at all, by length as well as by entry. Sameshape as
objectSetValidate, one kind over.arraySetnow takes arestrather than an optional one: every array setis stated with one, and the absent
restis what it normalizes an empty oneto. It also trims a trailing position stating exactly its
restwhen therestadmitsundefined, so that one set keeps one spelling:[],[unknown]andarray(unknown)are oneNode, and[number, unknown]is[number]'s. The proviso is what keeps the trim from widening the set: thetwo spellings differ only on the arrays with nothing at that position — one
ending before it, one holding a hole at it — so
{ prefix: [number], rest: number }keeps its position and stays "one ormore numbers".
arraySetSubsetis unchanged. Only the longest array each side admitsneeds testing: a position
qinsists on is onepinsists on as soon as thepointwise check passes, since otherwise
undefinedwould be a member ofp.prefix[i]and not ofq.prefix[i]. It stays sound, and gains one moreknown incompleteness, documented in
data/README.mdalongside the existingtwo.
toTsprints the rest element that says atuple is open, and a position the array may end before as optional
(
readonly[number,(undefined|string)?,...readonly(unknown)[]]). Thetype-level
Tstransformer cannot express either generically, but printingone concrete pattern is not subject to that limitation, and the divergence is
documented at both ends.
toJsonSchemaemitsitemsfor what follows theprefix, with
minItemsnow computed as the object side'srequiredlist is:one past the last position excluding
undefined, and an optional positionhas
undefinedstripped from its schema.What now spells an exact-length array
{ prefix }with norest. No thunk-form schema produces it in general today(
array(never)reaches only the empty array); the plannedcloseform(
fjs/types/rtti/todo/close-type.md) is what will, and its mapping table —open
rest: unknown,['close', S]→rest: never— is what this landsagainst. The proofs cover that arm through data-form literals so it does not
rot in the meantime.
Checks
npx tsc,npm start test(3107 tests), andnpm run cov(100% lines,branches, functions) all pass. No Rust touched. The TypeScript the printer now
emits for optional positions was compiled under
--strictto confirm a shorterarray is assignable to it.
The acceptance table in
validate/proof.f.mjsnow runs through all threereaders —
parse,validate, and the data form'svalidate— on acceptancealone: the data form reaches a value through the canonical union rather than
the schema's syntax, so it reports a miss as its own kind-wise failure rather
than repeating
or'sno match. This is the property the issue existed torestore, and it is where a future
toDatathat changes which values a schemaadmits will fail.
Two reader divergences remain, both byte-identical to
mainand neitherintroduced here: the data form reads an array's enumerable properties where
the schema-form readers walk only what a tuple declares, and the entry-walking
readers are blind to holes where the data form counts them. Each is a
candidate
todo/covering all three readers rather than a patch to one branchof one of them.
Changelog:
types/rtti/data:toDatamaps a tuple schema to theopen
{ prefix, rest: unknown }, matchingparse/validateacceptance;{ prefix }alone is now the exact-length set. Tuples render with a restelement and omittable positions optional
(
readonly[42,(undefined|string)?,...readonly(unknown)[]]), and as JSONSchema with
itemsrather thanitems: false.🤖 Generated with Claude Code
https://claude.ai/code/session_013vWeuBrBMSmBJBkLhfBmdu