Explain inverse#762
Merged
frankmcsherry merged 3 commits intoJun 17, 2026
Merged
Conversation
Re-land the proof-of-concept (removed from TimelyDataflow#760 as PR-scoped) on the follow-up branch where it belongs: the universal backstop reverses `flatmap` — the op the live rewrite still panics on — via the existing Dataflow primitives (forward pair table, join on the output, REFORM the whole input). Grounds the inverse work before the real rule + wiring. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…egression Replace the `panic!` on `LinearOp::FlatMap` in the reverse walk with a real rule, `emit_lookup_flatmap`. FlatMap is same-depth (it doesn't touch iteration time) and its list rides as one opaque value, so no envelope change is needed: build the (output -> input) pair table by running the op forward on the input side, join the demand on the packed output, and recover the whole input (the `None`-inverse endpoint). The one wrinkle — a plain flatmap drops the source row and the key isn't unique — is handled by re-keying the input by itself before exploding (the source rides through in the join key) and re-projecting to (k, pos, elem) after; a chain_in <= chain_out filter keeps it sound in iterating scopes. No new primitive; uses the existing project/flatmap/join. With this, `writable => explainable` is restored for flatmap programs. Verified: a flatmap sufficiency test passes, and the full suite — incl. the heavy --ignored relational sweeps — stays green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Collect (NEST) is a Reducer, so the reverse walk already routes it through the
non-min keyed lookup ("demand all same-key inputs") — which is exactly the
demand for a collected list (all its members). A sufficiency test over a
`| collect` program confirms the existing path handles a List-valued reducer
output; no new rule needed.
Co-Authored-By: Claude Opus 4.8 (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
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.
After #760 (Value/ADT data model), the explain rewrite covered the relational subset but panic!'d on FlatMap — so the new ADT expressiveness wasn't explainable, breaking
the writable ⟹ explainable invariant. This closes that gap, minimally and additively (no rewrite of the working relational rules, no envelope change).
value, so it slots into the existing flat envelope. The (output → input) pair table is built by running the op forward on the input side; the one wrinkle — a plain
flatmap drops the source and the key isn't unique — is handled by re-keying the input by itself before exploding (the source rides through in the join key), then
re-projecting to (k, pos, elem); a chain_in ≤ chain_out filter keeps it sound in iterating scopes. No new primitive.
Verified: flatmap and collect programs explain end-to-end (demand regenerates the queried output), and the full suite — including the heavy --ignored relational sweeps —
stays green.
Deferred (not needed for the invariant): the full (PRESERVED/RESIDUAL/REFORM) inverse-interface unification + opaque-value envelope (which would also delete the
Term-arity shape pass) — an independent cleanup for later.
🤖 Generated with Claude Code