feat(stdlib): Aggregate.affine — SQL group-by + aggregation primitives — db-theory #3 (7 externs)#527
Merged
Conversation
…s — db-theory #3 (7 externs) New `Aggregate` module exposing SQL aggregation as typed scalars: db_count / db_sum / db_min_int / db_max_int (Int monoids), db_avg (Float, derived as SUM/COUNT), db_group_by (full grouped result-set as JSON), and db_group_count (convenience over (key, count) buckets). Codegen prelude adds `__as_db{Count,Sum,MinInt,MaxInt,Avg,GroupBy, GroupCount}` helpers delegating to `globalThis.__as_sqlite.agg*` / `groupBy` / `groupCount`. Deno-ESM smoke witnesses all 7 externs across 5 fold-shaped assertions + 2 group-bucket shape assertions. Cross-doc: docs/academic/proofs/db-theory-3-aggregation-as-fold.md states the headline safety property #DB-3.1 (aggregation-as-fold): each aggregator is a commutative monoid and group-by is the indexed sum (Green/Karvounarakis/Tannen provenance-semiring framing). Aggregator monoid table in cross-doc shows COUNT/SUM/MIN/MAX are proper monoids; AVG derived as SUM/COUNT. Echo-types upstream extension tracked at hyperpolymath/echo-types#175 — proposes new EchoAggregation.agda module with `Monoid` + `GroupAggregator` carriers + signature for `aggregation-as-fold` lemma. The proof reduces to existing closure properties (EchoCost as existence witness; OmegaPow.additive-principal for ω^n monoid closure). Sibling: echo-types#174 (Transaction safety). Stacked on feat/db-2-transactions (#526) — auto-rebase after #526 merges into main. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Jun 2, 2026
…s — db-theory #3 (7 externs) (#527) ## Summary - New `stdlib/Aggregate.affine` module with 7 externs: `db_count`, `db_sum`, `db_min_int`, `db_max_int`, `db_avg`, `db_group_by` (whole result-set as JSON), `db_group_count` (key/count buckets as JSON). - Codegen + Deno-ESM JS prelude wired; smoke + harness witness all 7 externs with both single-row aggregates and grouped buckets. - Cross-doc proof obligation at `docs/academic/proofs/db-theory-3-aggregation-as-fold.md` — each aggregator is a commutative monoid, group-by is the indexed sum (Green/Karvounarakis/Tannen). - **Stacked on [#526](#526 (Transactions) — base will flip to `main` once #526 merges; auto-rebase will pick up cleanly. ## Echo-types audit cross-doc Per owner directive 2026-06-01, mandatory audit step. Found: no existing `Monoid`/`Semiring` infrastructure in echo-types. Closest scaffolding: `EchoCost.CostAlgebra` (left-identity only), `OmegaPow.additive-principal`. Filed [hyperpolymath/echo-types#175](hyperpolymath/echo-types#175) proposing new `EchoAggregation.agda` module with `Monoid` + `GroupAggregator` carriers + signature for `aggregation-as-fold` lemma. Sibling: [echo-types#174](hyperpolymath/echo-types#174) (Transaction safety). ## Aggregator monoid table | Aggregator | Elem | ε | ⊕ | Comm? | Idemp? | |------------|-----------------|----|----|-------|--------| | COUNT | ℕ | 0 | + | ✓ | ✗ | | SUM | ℕ (or ℤ, ℝ) | 0 | + | ✓ | ✗ | | MIN | ℕ ∪ {∞} | ∞ | min | ✓ | ✓ | | MAX | ℕ ∪ {-∞} | -∞ | max | ✓ | ✓ | | AVG | derived: SUM/COUNT (not a monoid — no identity) | ## Test plan - [x] `dune runtest test/test_main.exe` — 368 tests green (one more than baseline since AOT smoke picked up `Aggregate.affine`). - [x] `tools/run_codegen_deno_tests.sh` — `aggregate_smoke.harness.mjs` passes all 8 assertions (5 single-row + 3 grouped). - [x] Stack discipline: based on `feat/db-2-transactions`; will rebase onto main once #526 lands. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Jun 2, 2026
Appends today's three db-theory stdlib PRs to the [Unreleased] section. Repo's changelog-reusable.yml automation isn't wired yet (manual append per the file's own header pointer). Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
2 tasks
hyperpolymath
added a commit
that referenced
this pull request
Jun 2, 2026
## Summary Refresh the authoritative status surfaces in this repo to reflect the stdlib **db-theory triplet** that landed yesterday and today: - PR #525 — `Sqlite.affine` schema introspection + bulk I/O + error inspection (db-theory #1c, 6 externs) - PR #526 — `Transaction.affine` (db-theory #2, affine-bounded write-set isolation, 8 externs) - PR #527 — `Aggregate.affine` (db-theory #3, SQL group-by + aggregation primitives, 7 externs) - PR #528 — CHANGELOG sync (already merged) `CHANGELOG.md` is already up to date via #528, so this PR touches only the four files that ledger that work as status, not as history. ## What changed - `docs/CAPABILITY-MATRIX.adoc` — replace the stale "19/19 stdlib files" sentence (the AOT gate now discovers files dynamically) and call out the db-theory triplet as the current authoring frontier alongside Http / Json / Dict-Map. - `docs/TECH-DEBT.adoc` §C STDLIB — add a `STDLIB-05` row capturing the full Sqlite arc (#522 / #524 / #525), Transaction (#526), and Aggregate (#527), with pointers to the two academic proofs the PRs already shipped (`docs/academic/proofs/db-theory-{2,3}-*.md`). - `docs/stdlib-roadmap.adoc` — promote `Sqlite.affine` from `partial / Coverage audit needed` to `usable`, and add `Aggregate.affine` + `Transaction.affine` rows to the inventory snapshot. - `.machine_readable/6a2/STATE.a2ml` — bump `last-updated` to `2026-06-02` (this file mirrors, it does not lead — per its own drift-flag). ## What was deliberately *not* touched - `docs/ROADMAP.adoc` — language/compiler progress; the db-theory PRs are stdlib-side and don't move the language roadmap. - A `TEST-NEEDS` file — none exists at repo root; the three PRs each shipped their own Deno-ESM smoke harness under `tests/codegen-deno/` (`sqlite_introspect_bulk` / `transaction_smoke` / `aggregate_smoke`) and the AOT gate auto-picked the new modules up. - License / SPDX headers — per the estate's no-automated-licence-edits rule. ## Test plan - [x] `bash tools/check-doc-truthing.sh` passes locally — banner / primacy / mirror invariants intact, over-claim ratchet unchanged (no new baseline entry needed). - [x] Commit GPG-signed; verified `gpg: Good signature`. Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (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.
Summary
stdlib/Aggregate.affinemodule with 7 externs:db_count,db_sum,db_min_int,db_max_int,db_avg,db_group_by(whole result-set as JSON),db_group_count(key/count buckets as JSON).docs/academic/proofs/db-theory-3-aggregation-as-fold.md— each aggregator is a commutative monoid, group-by is the indexed sum (Green/Karvounarakis/Tannen).mainonce feat(stdlib): Transaction.affine — affine-bounded write-set isolation — db-theory #2 (8 externs) #526 merges; auto-rebase will pick up cleanly.Echo-types audit cross-doc
Per owner directive 2026-06-01, mandatory audit step. Found: no existing
Monoid/Semiringinfrastructure in echo-types. Closest scaffolding:EchoCost.CostAlgebra(left-identity only),OmegaPow.additive-principal. Filed hyperpolymath/echo-types#175 proposing newEchoAggregation.agdamodule withMonoid+GroupAggregatorcarriers + signature foraggregation-as-foldlemma. Sibling: echo-types#174 (Transaction safety).Aggregator monoid table
Test plan
dune runtest test/test_main.exe— 368 tests green (one more than baseline since AOT smoke picked upAggregate.affine).tools/run_codegen_deno_tests.sh—aggregate_smoke.harness.mjspasses all 8 assertions (5 single-row + 3 grouped).feat/db-2-transactions; will rebase onto main once feat(stdlib): Transaction.affine — affine-bounded write-set isolation — db-theory #2 (8 externs) #526 lands.🤖 Generated with Claude Code