DDIR: the sum universe — declared types, corgi as the typer, no shape… - #854
Merged
Conversation
… inference
Sums in DDIR had no type: `con Name(arity) = tag` was parse-time sugar, and
three mechanisms guessed each sum's shape from data (infer_shape_cols per
batch, infer_term_shape per term with an arity of tag+1, and shape_join, a
private bottom lattice reconciling them). The corgi bump removes bottom,
and with it the room to guess.
Now:
* `type Kind = Rare u64 | Common (u64, u64) | Empty;` declares a sum. Tags
are positions, scoped to the type; payload shapes are u64/int, (), tuples,
List(..), Option(..), Result(..), or an earlier type. Constructors build
into the whole declared sum (`Term::Inject { tag, payload, sum }` carries
every lane's shape; `Type::Ctor` disambiguates), patterns bind a tuple
payload's fields or the whole payload, and `variant(Type, tag, payload)`
is the data-driven form (corgi's Branch, over a homogeneous type).
* Built-in `Option`/`Result` with `Some`/`None`/`Ok`/`Err`; the lane a
payload cannot fix comes from the other branch of an `if` or the other
arms of a `case` (a compile-time hole, never a runtime lane).
* The typer is corgi's: `shape_of_term` lowers a term into a scratch graph
and asks `corgi::shape_of`. infer_shape_cols, infer_term_shape,
shape_of_place and shape_join are gone.
* Shapes are pinned. An input collection's shape comes from its first row
(`shape_of_row`; a variant or an empty list on input needs a declared
schema, which is a follow-up) and every later batch transcodes against
it. Each linear op compiles once, on its first non-empty batch (`Plan`),
and a later batch of another shape is the invariant violation.
* No row-wise path inside the dataflow. A term that does not lower is a
type error with corgi's message, not a fallback: `Fold` steps that read
the enclosing environment are closed by `CapList` capture, and list
projection lowers to the new `Op::Get`. Rows exist only at the ingest
and egress boundaries.
Programs: `con` decls become `type` decls (sum_skew is an ordinary program
now — both sides build the same declared sum); sum_ops uses the typed
variant form; case_ops' shape-conflicted filter becomes a well-typed one and
gains an `Option` round trip. All 14 backend programs agree with vec.
corgi is pinned at WIP 578ef3f (the streamline merge, #16), with the `serde`
feature DDIR's Term needs.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012k2GSwxmvD2LvckkoXi6GK
frankmcsherry
marked this pull request as ready for review
September 2, 2026 01:44
The Collect reducer emitted a row for every bracket, an empty list when all diffs were <= 0. A bracket whose values all cancelled is a key with no input, for which DD invokes no reducer, so the vec backend emits nothing; the corgi backend kept a stale empty list per retracted key. Under iteration this leaked: the e-graph's signature table kept signatures for minted nodes that had since been retracted, and the class map disagreed with vec by exactly those ids. The same all-cancelled bracket was also the source of a `List<()>` column (an empty list with no element shape) that the next batch's `List<T>` could not be concatenated with; the element column now always carries the input values' shape. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012k2GSwxmvD2LvckkoXi6GK
…osed terms The server's `feed` writes ADT values as closed terms, `inject(2, tuple(3, 4))`, which the sum-universe commit had turned into a parse panic. It is now `SumTy::Dynamic`: a `Value::Variant` literal the row interpreter evaluates, naming no sum, so the columnar lowering reports it as untyped rather than guessing a shape. Programs build sums from declared types as before. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012k2GSwxmvD2LvckkoXi6GK
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012k2GSwxmvD2LvckkoXi6GK
frankmcsherry
force-pushed
the
ddir-sum-universe
branch
from
September 2, 2026 02:06
7371de3 to
862b1f1
Compare
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.
… inference
Sums in DDIR had no type:
con Name(arity) = tagwas parse-time sugar, and three mechanisms guessed each sum's shape from data (infer_shape_cols per batch, infer_term_shape per term with an arity of tag+1, and shape_join, a private bottom lattice reconciling them). The corgi bump removes bottom, and with it the room to guess.Now:
type Kind = Rare u64 | Common (u64, u64) | Empty;declares a sum. Tags are positions, scoped to the type; payload shapes are u64/int, (), tuples, List(..), Option(..), Result(..), or an earlier type. Constructors build into the whole declared sum (Term::Inject { tag, payload, sum }carries every lane's shape;Type::Ctordisambiguates), patterns bind a tuple payload's fields or the whole payload, andvariant(Type, tag, payload)is the data-driven form (corgi's Branch, over a homogeneous type).Option/ResultwithSome/None/Ok/Err; the lane a payload cannot fix comes from the other branch of anifor the other arms of acase(a compile-time hole, never a runtime lane).shape_of_termlowers a term into a scratch graph and askscorgi::shape_of. infer_shape_cols, infer_term_shape, shape_of_place and shape_join are gone.shape_of_row; a variant or an empty list on input needs a declared schema, which is a follow-up) and every later batch transcodes against it. Each linear op compiles once, on its first non-empty batch (Plan), and a later batch of another shape is the invariant violation.Foldsteps that read the enclosing environment are closed byCapListcapture, and list projection lowers to the newOp::Get. Rows exist only at the ingest and egress boundaries.Programs:
condecls becometypedecls (sum_skew is an ordinary program now — both sides build the same declared sum); sum_ops uses the typed variant form; case_ops' shape-conflicted filter becomes a well-typed one and gains anOptionround trip. All 14 backend programs agree with vec.corgi is pinned at WIP 578ef3f (the streamline merge, #16), with the
serdefeature DDIR's Term needs.Claude-Session: https://claude.ai/code/session_012k2GSwxmvD2LvckkoXi6GK