|
| 1 | +// SPDX-License-Identifier: MPL-2.0 |
| 2 | +// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | +// |
| 4 | +// Aggregate.affine — SQL group-by + aggregation primitives (db-theory #3). |
| 5 | +// |
| 6 | +// Aggregation is a thin convenience layer over the existing Sqlite |
| 7 | +// extern surface. The runtime contract is: each aggregator extern |
| 8 | +// runs a SQL query that returns *exactly one row* with the aggregate |
| 9 | +// in column 0, and that result is unwrapped to a typed scalar |
| 10 | +// (`Int` / `Float`). The `db_group_by` extern returns the whole |
| 11 | +// grouped result-set as a JSON array — caller parses with `Json::parse`. |
| 12 | +// |
| 13 | +// **Proof obligation #DB-3.1 (aggregation-as-monoid-homomorphism)** |
| 14 | +// Each scalar aggregator is a commutative monoid; group-by is the |
| 15 | +// indexed sum. Formally, for any aggregator `M` (with identity `ε` |
| 16 | +// and combine `⊕`) and any partition `{group_k}` of the row set: |
| 17 | +// aggregate(SELECT M(v) FROM t GROUP BY k) |
| 18 | +// = { k ↦ foldr ⊕ ε (map M.agg group_k) } |
| 19 | +// |
| 20 | +// Concretely: COUNT is `(ℕ, 0, +)`, SUM is `(ℕ, 0, +)`, MIN is |
| 21 | +// `(ℕ ∪ {∞}, ∞, min)`, MAX is `(ℕ ∪ {-∞}, -∞, max)`. AVG is *not* |
| 22 | +// a monoid (no identity) — express as `SUM/COUNT`. |
| 23 | +// |
| 24 | +// Status: pending against `hyperpolymath/echo-types#175` — proposes |
| 25 | +// a new `EchoAggregation.agda` module with `Monoid` + `GroupAggregator` |
| 26 | +// carriers reducing to the standard provenance-semiring framing |
| 27 | +// (Green / Karvounarakis / Tannen). Cross-doc: |
| 28 | +// `docs/academic/proofs/db-theory-3-aggregation-as-fold.md`. |
| 29 | +// |
| 30 | +// **Why this is the natural db-theory #3** |
| 31 | +// Aggregation is the most-used non-trivial query shape outside |
| 32 | +// selection/projection — every SQL report depends on it. Wiring |
| 33 | +// aggregation through typed monoids (rather than ad-hoc strings) |
| 34 | +// gives us the foundation for later db-theory items: #4 (selection |
| 35 | +// distributivity over agg), #6 (agg over indexed scans), #9 (CRDTs |
| 36 | +// as monoids with convergence). |
| 37 | + |
| 38 | +module Aggregate; |
| 39 | + |
| 40 | +// ── Scalar aggregators (single-row result) ───────────────────────── |
| 41 | +// |
| 42 | +// Each extern runs a SQL returning exactly one row with the aggregate |
| 43 | +// in column 0. `params_json` follows the same JSON-array contract as |
| 44 | +// the `db_query*` family. Empty result-sets degenerate to the |
| 45 | +// aggregator's identity (`0` for COUNT/SUM, runtime-defined for MIN/MAX). |
| 46 | + |
| 47 | +/// COUNT — returns the cardinality of the result-set. SQL form: |
| 48 | +/// `SELECT COUNT(*) FROM t WHERE ...` or `SELECT COUNT(col) FROM t ...`. |
| 49 | +/// Identity: 0. Monoid: `(ℕ, 0, +)`. |
| 50 | +pub extern fn db_count(d: Db, sql: String, params_json: String) -> Int; |
| 51 | + |
| 52 | +/// SUM — returns the sum of an integer-valued expression. SQL form: |
| 53 | +/// `SELECT SUM(col) FROM t WHERE ...`. Identity: 0. Monoid: `(ℕ, 0, +)`. |
| 54 | +pub extern fn db_sum(d: Db, sql: String, params_json: String) -> Int; |
| 55 | + |
| 56 | +/// MIN — returns the minimum integer value. SQL form: |
| 57 | +/// `SELECT MIN(col) FROM t WHERE ...`. Identity: ∞ (runtime: sentinel). |
| 58 | +/// Monoid: `(ℕ ∪ {∞}, ∞, min)`. |
| 59 | +pub extern fn db_min_int(d: Db, sql: String, params_json: String) -> Int; |
| 60 | + |
| 61 | +/// MAX — returns the maximum integer value. SQL form: |
| 62 | +/// `SELECT MAX(col) FROM t WHERE ...`. Identity: -∞. Monoid: |
| 63 | +/// `(ℕ ∪ {-∞}, -∞, max)`. |
| 64 | +pub extern fn db_max_int(d: Db, sql: String, params_json: String) -> Int; |
| 65 | + |
| 66 | +/// AVG — returns the average as a Float. **NOT a monoid** (no identity); |
| 67 | +/// implemented as `SUM/COUNT`. The host adapter rounds following IEEE 754. |
| 68 | +pub extern fn db_avg(d: Db, sql: String, params_json: String) -> Float; |
| 69 | + |
| 70 | +// ── Multi-row aggregation (GROUP BY) ─────────────────────────────── |
| 71 | +// |
| 72 | +// `db_group_by` runs a SQL with a GROUP BY clause and returns the |
| 73 | +// entire result-set as a JSON array. Each element is itself a JSON |
| 74 | +// array of column values, in the order declared in the SELECT list. |
| 75 | +// Caller parses with `Json::parse` and pattern-matches the shape. |
| 76 | +// |
| 77 | +// Example: |
| 78 | +// db_group_by(d, "SELECT dept, COUNT(*), SUM(salary) FROM e GROUP BY dept", "[]") |
| 79 | +// -> '[["eng", 12, 1450000], ["sales", 5, 420000], ...]' |
| 80 | +// |
| 81 | +// The shape contract is *adapter-enforced*: a missing GROUP BY clause |
| 82 | +// still works (single-row result) but defeats the purpose. A future |
| 83 | +// typed `Group<K, V>` carrier would lift this to a parametric type; |
| 84 | +// blocked on the dependent-type story for parametric externs |
| 85 | +// (typed bindings #DB-3.2). |
| 86 | + |
| 87 | +pub extern fn db_group_by(d: Db, sql: String, params_json: String) -> String; |
| 88 | + |
| 89 | +// ── Group-bucket count (convenience over db_group_by) ────────────── |
| 90 | +// |
| 91 | +// `db_group_count` returns the count-per-group as a JSON array of |
| 92 | +// `[key, count]` pairs. Equivalent to: |
| 93 | +// `db_group_by(d, "SELECT key, COUNT(*) FROM t GROUP BY key", ...)` |
| 94 | +// — but encapsulates the SELECT-list shape so callers don't need to |
| 95 | +// inline the COUNT(*) projection. The key column is referenced by |
| 96 | +// name (`key_col`), the table by name (`table`). |
| 97 | + |
| 98 | +pub extern fn db_group_count(d: Db, table: String, key_col: String) -> String; |
0 commit comments