From d2c9f4c2a321de062be12430e94e8edfdff0ff7e Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 20 Oct 2026 12:45:27 +0000 Subject: [PATCH 1/5] feat: mirror EchoAggregation (general monoid/group aggregation, echo-types#175) Finite-domain shadow of echo-types EchoAggregation.agda at 703dd77: Monoid, GroupAggregator, the fold and its homomorphism law (aggregation-as-fold), the sum/count/max/min instances, the generic no-canonical-disaggregation, and the macro Example-PairSum instance. Laws are checked on samples, never proved; the Agda stays the source of truth. avg is absent (not a monoid), as upstream. Adds 27 assertions (258 -> 285), including a negative control showing monoid_laws_hold can return false. No version bump; that is left to the owner. Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- README.adoc | 13 +++- src/EchoTypes.jl | 178 ++++++++++++++++++++++++++++++++++++++++++++++- test/runtests.jl | 66 ++++++++++++++++++ 3 files changed, 254 insertions(+), 3 deletions(-) diff --git a/README.adoc b/README.adoc index 4422477..2256dfc 100644 --- a/README.adoc +++ b/README.adoc @@ -136,6 +136,14 @@ audience move 4 — blur loses perturbation tag) `+source_no_section_holds+`, `+gap_paired+` |`+EchoLLEncoding.agda+` (cementing-negative — the LL `+!A := 1+` shadow admits an encoded section paired with source-side no-section) +|*unreleased* `+Monoid+`, `+GroupAggregator+`, `+oplus_fold+`, +`+aggregate_values+`, `+aggregation_as_fold_holds+`, `+sum_monoid+` / +`+count_monoid+` / `+max_monoid+` / `+min_monoid+`, +`+no_canonical_disaggregation_of+`, `+pair_sum+` and its +`+pair_sum_*+` checks |`+EchoAggregation.agda+` (general monoid/group +aggregation, echo-types#175; the macro `+pairSum+` ledger is an instance. +Laws are checked on samples, not proved; `+avg+` is absent because it is +not a monoid) |=== ==== What is intentionally NOT mirrored @@ -233,8 +241,9 @@ v0.3.0 adds executable shadows of the Tier-3 audience-facing spine that landed upstream on 2026-05-27/28 (`+EchoProvenance+`, `+EchoSecurity+`, `+EchoProbabilisticSupport+`, `+EchoDifferential+`) plus the cementing-negative `+EchoLLEncoding+` (LL shallow-encoding gap with -paired source-side no-section). Test suite: *258 passing assertions -across 19 testsets*, organised as finite shadows of named Agda lemmas +paired source-side no-section). Unreleased on top of v0.3.0: +`+EchoAggregation+` (mirrored from echo-types `+703dd77+`). Test suite: +*285 passing assertions across 21 testsets*, organised as finite shadows of named Agda lemmas plus the semantic-fibre vocabulary exercise over the kernel. Registered as `+EchoTypes+` in the hyperpolymath professional registry; *not* registered in the Julia General registry and intentionally *not* part of diff --git a/src/EchoTypes.jl b/src/EchoTypes.jl index dbd0a81..f8cb13c 100644 --- a/src/EchoTypes.jl +++ b/src/EchoTypes.jl @@ -24,6 +24,11 @@ # worked instance`) + cementing-negative EchoLLEncoding (the # trivial-⊤-shadow LL gap with paired source-side no-section). # +# Unreleased on top of v0.3.0: EchoAggregation (general monoid/group +# aggregation, echo-types#175), mirrored from echo-types origin/main +# @ 703dd77af402e959b46f49e8ce2e084521bedbae. The rest of this header's +# provenance pin is unchanged. +# # Retraction discipline (R-2026-05-18): no graded-comonad framing, # no universal-property or conservativity claims appear here. F5 (full # OFS, honestly funext-qualified) earned back upstream 2026-05-27; the @@ -88,7 +93,16 @@ export EchoWitness, echo_intro, in_fiber, fiber, # EchoLLEncoding (v0.3.0) LLShallowEncoding, trivial_encoding, trivial_encoding_has_section, ll_encoding_gap, - source_no_section_holds, gap_paired + source_no_section_holds, gap_paired, + # EchoAggregation (unreleased; general monoid/group form, echo-types#175) + Monoid, GroupAggregator, monoid_laws_hold, + oplus_fold, oplus_fold_append_holds, + aggregate_values, aggregation_as_fold_holds, + sum_monoid, count_monoid, max_monoid, min_monoid, min_inf, + count_aggregator, no_canonical_disaggregation_of, + pair_sum, pair_sum_is_fold, ledger1, ledger2, + pair_sum_collapses, pair_sum_non_injective, + no_canonical_disaggregation_pair_sum # ====================================================================== # Kernel — Echo.agda @@ -1276,4 +1290,166 @@ function gap_paired(linear_samples=(LEcho(true, Linear), LEcho(false, Linear))) source_no_section = source_no_section_holds(linear_samples)) end +# ====================================================================== +# EchoAggregation.agda — aggregation as a monoid fold (echo-types#175) +# +# The GENERAL aggregation form: a `Monoid` carrier, a `GroupAggregator` +# mapping values into it, the fold `⊕-fold`, and the homomorphism law +# `aggregation-as-fold` (aggregating a concatenation = combining the two +# aggregates). The macro-economics reading (micro ledger -> macro total, +# the Sonnenschein–Mantel–Debreu critique) is one INSTANCE, mirrored as +# the `pair_sum` block below. +# +# Finite-shadow caveat: Agda proves `assoc`, `identity-l/r` and the fold +# law for ALL inputs. Julia can only check them on supplied samples, so +# every `*_holds` function below is a falsifier on the data it is given, +# never a proof. `avg` is deliberately absent (not a monoid), as upstream. +# ====================================================================== + +""" + Monoid(ε, op) + +The aggregation carrier (`Monoid`, EchoAggregation.agda): a unit `ε` and +an associative binary `op` (`_⊕_`). Laws are NOT enforced at construction; +`monoid_laws_hold` checks them on samples. +""" +struct Monoid{E,OP} + ε::E + op::OP +end + +""" + monoid_laws_hold(M, samples) -> Bool + +`assoc`, `identity-l`, `identity-r` of `M`, checked over every triple / +element drawn from `samples`. A `false` is a counterexample; a `true` is +evidence on those samples only. +""" +function monoid_laws_hold(M::Monoid, samples) + all(a -> M.op(M.ε, a) == a && M.op(a, M.ε) == a, samples) && + all(t -> M.op(M.op(t[1], t[2]), t[3]) == M.op(t[1], M.op(t[2], t[3])), + Iterators.product(samples, samples, samples)) +end + +""" + oplus_fold(M, xs) + +`⊕-fold`: fold a list through the monoid (`foldr op ε`). +""" +oplus_fold(M::Monoid, xs) = foldr(M.op, xs; init = M.ε) + +""" + oplus_fold_append_holds(M, xs, ys) -> Bool + +`⊕-fold-++`: the fold is a monoid homomorphism on list concatenation, +`⊕-fold (xs ++ ys) == ⊕-fold xs ⊕ ⊕-fold ys`, checked at `xs`, `ys`. +""" +oplus_fold_append_holds(M::Monoid, xs, ys) = + oplus_fold(M, vcat(xs, ys)) == M.op(oplus_fold(M, xs), oplus_fold(M, ys)) + +""" + GroupAggregator(agg) + +A value -> monoid-element aggregator (`GroupAggregator`, +EchoAggregation.agda). The group-by key `K` is phantom upstream and has no +runtime content here. +""" +struct GroupAggregator{AG} + agg::AG +end + +""" + aggregate_values(G, M, vs) + +`aggregate-values`: map the aggregator over `vs`, then fold through `M`. +""" +aggregate_values(G::GroupAggregator, M::Monoid, vs) = + oplus_fold(M, map(G.agg, vs)) + +""" + aggregation_as_fold_holds(G, M, vs, ws) -> Bool + +`aggregation-as-fold` (the #175 headline law): aggregating `vs ++ ws` +equals combining `aggregate_values` of each, checked at `vs`, `ws`. +Honest scope: the fold's homomorphism property, NOT SQL GROUP-BY's full +operational semantics. +""" +aggregation_as_fold_holds(G::GroupAggregator, M::Monoid, vs, ws) = + aggregate_values(G, M, vcat(vs, ws)) == + M.op(aggregate_values(G, M, vs), aggregate_values(G, M, ws)) + +# --- The four concrete instances (ℕ modelled as non-negative Int) ----- + +"`sumMonoid`: (ℕ, 0, +)." +sum_monoid() = Monoid(0, +) + +"`countMonoid`: the SAME monoid as `sum_monoid`; counting happens in the aggregator." +count_monoid() = sum_monoid() + +"`maxMonoid`: (ℕ, 0, max). 0 is the max-identity on ℕ." +max_monoid() = Monoid(0, max) + +""" + min_inf(a, b) + +`_⊓∞_`: min over ℕ ∪ {∞}, with `nothing` = ∞ (the min-identity) and an +`Int` standing for `just n`. +""" +min_inf(a::Nothing, b) = b +min_inf(a::Integer, b::Nothing) = a +min_inf(a::Integer, b::Integer) = min(a, b) + +"`minMonoid`: (ℕ ∪ {∞}, ∞, ⊓∞) with `nothing` = ∞." +min_monoid() = Monoid(nothing, min_inf) + +"`countAggregator`: every value contributes 1 to the sum monoid." +count_aggregator() = GroupAggregator(_ -> 1) + +""" + no_canonical_disaggregation_of(agg_map, x, y) -> Bool + +`no-canonical-disaggregation-of`: an aggregation map with a collision +(`x != y`, `agg_map(x) == agg_map(y)`) admits no section. This is +`no_section_of_collapsing_map` under aggregation-flavoured names, as +upstream. It refutes a *section* (a left inverse), NOT the existence of +some representative choice. +""" +no_canonical_disaggregation_of(agg_map, x, y) = + no_section_of_collapsing_map(agg_map, x, y) + +# --- Example-PairSum: the macro instance (ℕ × ℕ -> ℕ by +) ------------- + +"`pairSum (a , b) = a + b`." +pair_sum(p::Tuple{Integer,Integer}) = p[1] + p[2] + +""" + pair_sum_is_fold(p) -> Bool + +`pairSum-is-fold`: `pair_sum` IS the `sum_monoid` fold of its two fields, +so the macro instance is a special case of the general form. +""" +pair_sum_is_fold(p::Tuple{Integer,Integer}) = + pair_sum(p) == oplus_fold(sum_monoid(), [p[1], p[2]]) + +"`ledger₁ = (0 , 1)`." +ledger1() = (0, 1) + +"`ledger₂ = (1 , 0)`." +ledger2() = (1, 0) + +"`pairSum-collapses`: both ledgers aggregate to 1." +pair_sum_collapses() = pair_sum(ledger1()) == pair_sum(ledger2()) + +""" + pair_sum_non_injective() -> Bool + +`pairSum-non-injective`: the two echoes over total 1 are distinct. +""" +pair_sum_non_injective() = + echo_intro(pair_sum, ledger1()) != echo_intro(pair_sum, ledger2()) + +"`Example-PairSum.no-canonical-disaggregation`: no section of `pair_sum`." +no_canonical_disaggregation_pair_sum() = + no_canonical_disaggregation_of(pair_sum, ledger1(), ledger2()) + end # module EchoTypes diff --git a/test/runtests.jl b/test/runtests.jl index d9cea9b..13a71dd 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -432,4 +432,70 @@ using Test @test gp.encoded_section @test gp.source_no_section end + + # ------------------------------------------------------------------ + # EchoAggregation (general monoid/group form, echo-types#175; mirrors + # echo-types main @ 703dd77). Finite shadow: laws are checked on + # samples, never proved. HONEST BOUND: the fold's homomorphism law, + # NOT SQL GROUP-BY semantics; `avg` is absent (not a monoid). + # ------------------------------------------------------------------ + + @testset "Aggregation: monoid fold + homomorphism law (EchoAggregation.agda)" begin + nat = 0:6 + for M in (sum_monoid(), count_monoid(), max_monoid()) + @test monoid_laws_hold(M, nat) + end + # min over ℕ ∪ {∞}: `nothing` is ∞. + mins = [nothing; collect(nat)] + @test monoid_laws_hold(min_monoid(), mins) + + # Falsifier: a non-monoid is rejected (subtraction is not associative; + # 0 is only a right identity), so `monoid_laws_hold` can say `false`. + @test !monoid_laws_hold(Monoid(0, -), nat) + + # ⊕-fold-++ at each instance. + @test oplus_fold_append_holds(sum_monoid(), [1, 2, 3], [4, 5]) + @test oplus_fold_append_holds(max_monoid(), [1, 5, 3], [4, 2]) + @test oplus_fold_append_holds(min_monoid(), [3, nothing, 1], [4, 2]) + @test oplus_fold_append_holds(sum_monoid(), Int[], [4, 5]) + @test oplus_fold_append_holds(min_monoid(), Union{Nothing,Int}[], Union{Nothing,Int}[]) + + # Concrete fold values. + @test oplus_fold(sum_monoid(), [1, 2, 3]) == 6 + @test oplus_fold(max_monoid(), [1, 5, 3]) == 5 + @test oplus_fold(min_monoid(), [3, 1, 2]) == 1 + @test oplus_fold(min_monoid(), Union{Nothing,Int}[]) === nothing # empty min = ∞ + + # aggregation-as-fold with the worked count aggregator: + # count of a concatenation = sum of the counts. + C = count_aggregator() + @test aggregate_values(C, sum_monoid(), [:a, :b, :c]) == 3 + @test aggregate_values(C, sum_monoid(), Symbol[]) == 0 + @test aggregation_as_fold_holds(C, sum_monoid(), [:a, :b], [:c, :d, :e]) + + # A value-dependent aggregator over max. + G = GroupAggregator(v -> v.price) + rows = [(price = 3,), (price = 9,), (price = 4,)] + @test aggregate_values(G, max_monoid(), rows) == 9 + @test aggregation_as_fold_holds(G, max_monoid(), rows[1:1], rows[2:3]) + end + + @testset "Aggregation: Example-PairSum macro instance + no-section (EchoAggregation.agda)" begin + # pairSum is the sumMonoid fold of its two fields. + @test all(pair_sum_is_fold, [(a, b) for a in 0:4 for b in 0:4]) + + # Many-to-one: distinct ledgers, one total, distinct echoes. + @test pair_sum_collapses() + @test ledger1() != ledger2() + @test pair_sum_non_injective() + @test in_fiber(pair_sum, echo_intro(pair_sum, ledger1()), 1) + @test in_fiber(pair_sum, echo_intro(pair_sum, ledger2()), 1) + + # Keystone: no canonical disaggregation (no section). + @test no_canonical_disaggregation_pair_sum() + + # Matched negative: an injective aggregation has no collision to + # exhibit, so the witness correctly does not fire. + @test !no_canonical_disaggregation_of(identity, ledger1(), ledger2()) + end end From 03c626e54bee222aea9fe9bee2174a945e923ac8 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 20 Oct 2026 12:48:30 +0000 Subject: [PATCH 2/5] fix: address CodeRabbit review on the EchoAggregation mirror - monoid_laws_hold: materialise samples once (one-shot iterators work) and reject an empty sample instead of returning a vacuous true. - oplus_fold: document that it is a right fold, matching Agda's foldr. - min_inf: type the nothing-first method's second argument as Union{Nothing,Integer} so the domain is closed. - README: name both provenance commits (eed4250 for the existing rows, 703dd77 for EchoAggregation); test count 285 -> 290. Adds 5 assertions covering the one-shot iterator, the empty-sample error, the closed min_inf domain and the right-fold direction. Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- README.adoc | 10 +++++++--- src/EchoTypes.jl | 16 +++++++++++----- test/runtests.jl | 12 ++++++++++++ 3 files changed, 30 insertions(+), 8 deletions(-) diff --git a/README.adoc b/README.adoc index 2256dfc..92b6d6d 100644 --- a/README.adoc +++ b/README.adoc @@ -64,7 +64,10 @@ The Agda. This release mirrors `+hyperpolymath/echo-types+` at (2026-05-28 head, after the Tier-3 audience-facing spine landed — EchoProvenance, EchoSecurity, EchoProbabilisticSupport, EchoDifferential, EchoLLEncoding, plus the EchoCanonicalIdentitySuite -re-export bundle): +re-export bundle). The unreleased `+EchoAggregation+` entry below is +mirrored from a later commit, +`+703dd77af402e959b46f49e8ce2e084521bedbae+`; every other row keeps the +pin above: [width="100%",cols="50%,50%",options="header",] |=== @@ -242,8 +245,9 @@ landed upstream on 2026-05-27/28 (`+EchoProvenance+`, `+EchoSecurity+`, `+EchoProbabilisticSupport+`, `+EchoDifferential+`) plus the cementing-negative `+EchoLLEncoding+` (LL shallow-encoding gap with paired source-side no-section). Unreleased on top of v0.3.0: -`+EchoAggregation+` (mirrored from echo-types `+703dd77+`). Test suite: -*285 passing assertions across 21 testsets*, organised as finite shadows of named Agda lemmas +`+EchoAggregation+` (mirrored from echo-types `+703dd77+`, not from +`+eed4250+`). Test suite: +*290 passing assertions across 21 testsets*, organised as finite shadows of named Agda lemmas plus the semantic-fibre vocabulary exercise over the kernel. Registered as `+EchoTypes+` in the hyperpolymath professional registry; *not* registered in the Julia General registry and intentionally *not* part of diff --git a/src/EchoTypes.jl b/src/EchoTypes.jl index f8cb13c..5d0ae52 100644 --- a/src/EchoTypes.jl +++ b/src/EchoTypes.jl @@ -1323,18 +1323,24 @@ end `assoc`, `identity-l`, `identity-r` of `M`, checked over every triple / element drawn from `samples`. A `false` is a counterexample; a `true` is -evidence on those samples only. +evidence on those samples only. `samples` is materialised once, so one-shot +iterators work; an empty `samples` is an error rather than a vacuous `true`. """ function monoid_laws_hold(M::Monoid, samples) - all(a -> M.op(M.ε, a) == a && M.op(a, M.ε) == a, samples) && + ss = collect(samples) # materialise once: `samples` is traversed four times + isempty(ss) && error("monoid_laws_hold: samples must be non-empty") + all(a -> M.op(M.ε, a) == a && M.op(a, M.ε) == a, ss) && all(t -> M.op(M.op(t[1], t[2]), t[3]) == M.op(t[1], M.op(t[2], t[3])), - Iterators.product(samples, samples, samples)) + Iterators.product(ss, ss, ss)) end """ oplus_fold(M, xs) -`⊕-fold`: fold a list through the monoid (`foldr op ε`). +`⊕-fold`: fold a list through the monoid as a RIGHT fold, +`x₁ ⊕ (x₂ ⊕ (… ⊕ ε))` (`foldr op ε`), matching Agda's `foldr`. For an +associative `op` the direction is immaterial; for a non-associative one the +result depends on it, so this fixes the reading falsifiers are run against. """ oplus_fold(M::Monoid, xs) = foldr(M.op, xs; init = M.ε) @@ -1395,7 +1401,7 @@ max_monoid() = Monoid(0, max) `_⊓∞_`: min over ℕ ∪ {∞}, with `nothing` = ∞ (the min-identity) and an `Int` standing for `just n`. """ -min_inf(a::Nothing, b) = b +min_inf(a::Nothing, b::Union{Nothing,Integer}) = b min_inf(a::Integer, b::Nothing) = a min_inf(a::Integer, b::Integer) = min(a, b) diff --git a/test/runtests.jl b/test/runtests.jl index 13a71dd..7048e57 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -453,6 +453,18 @@ using Test # 0 is only a right identity), so `monoid_laws_hold` can say `false`. @test !monoid_laws_hold(Monoid(0, -), nat) + # Samples are materialised once (one-shot iterators work) and an + # empty sample is an error, not a vacuous `true`. + @test monoid_laws_hold(sum_monoid(), (x for x in nat)) + @test_throws ErrorException monoid_laws_hold(sum_monoid(), Int[]) + + # `min_inf` keeps its domain closed: ℕ ∪ {∞} only. + @test min_inf(nothing, nothing) === nothing + @test_throws MethodError min_inf(nothing, "x") + + # ⊕-fold is a RIGHT fold: for non-associative `-` it is 1-(2-(3-0)). + @test oplus_fold(Monoid(0, -), [1, 2, 3]) == 2 + # ⊕-fold-++ at each instance. @test oplus_fold_append_holds(sum_monoid(), [1, 2, 3], [4, 5]) @test oplus_fold_append_holds(max_monoid(), [1, 5, 3], [4, 2]) From c92efbd2e6f91100d4b4a25e16f7576400f383da Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 20 Oct 2026 13:12:55 +0000 Subject: [PATCH 3/5] fix: accept generators in the fold-law checks (Codex P2) oplus_fold_append_holds and aggregation_as_fold_holds used vcat on their inputs. vcat of two generators nests them as elements instead of concatenating, so the former threw a MethodError and the latter returned a false counterexample on inputs that satisfy the law. Both now materialise their inputs once; oplus_fold does too, so one-shot iterables work. Adds 4 assertions (generator, filtered generator, aggregation over generators, fold of a filtered generator); 290 -> 294. Each failed before the change. Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- README.adoc | 2 +- src/EchoTypes.jl | 14 ++++++++++---- test/runtests.jl | 7 +++++++ 3 files changed, 18 insertions(+), 5 deletions(-) diff --git a/README.adoc b/README.adoc index 92b6d6d..1104cfe 100644 --- a/README.adoc +++ b/README.adoc @@ -247,7 +247,7 @@ cementing-negative `+EchoLLEncoding+` (LL shallow-encoding gap with paired source-side no-section). Unreleased on top of v0.3.0: `+EchoAggregation+` (mirrored from echo-types `+703dd77+`, not from `+eed4250+`). Test suite: -*290 passing assertions across 21 testsets*, organised as finite shadows of named Agda lemmas +*294 passing assertions across 21 testsets*, organised as finite shadows of named Agda lemmas plus the semantic-fibre vocabulary exercise over the kernel. Registered as `+EchoTypes+` in the hyperpolymath professional registry; *not* registered in the Julia General registry and intentionally *not* part of diff --git a/src/EchoTypes.jl b/src/EchoTypes.jl index 5d0ae52..c966c52 100644 --- a/src/EchoTypes.jl +++ b/src/EchoTypes.jl @@ -1337,12 +1337,13 @@ end """ oplus_fold(M, xs) -`⊕-fold`: fold a list through the monoid as a RIGHT fold, +`⊕-fold`: fold a list (any finite iterable, materialised once) through the +monoid as a RIGHT fold, `x₁ ⊕ (x₂ ⊕ (… ⊕ ε))` (`foldr op ε`), matching Agda's `foldr`. For an associative `op` the direction is immaterial; for a non-associative one the result depends on it, so this fixes the reading falsifiers are run against. """ -oplus_fold(M::Monoid, xs) = foldr(M.op, xs; init = M.ε) +oplus_fold(M::Monoid, xs) = foldr(M.op, collect(xs); init = M.ε) """ oplus_fold_append_holds(M, xs, ys) -> Bool @@ -1350,8 +1351,11 @@ oplus_fold(M::Monoid, xs) = foldr(M.op, xs; init = M.ε) `⊕-fold-++`: the fold is a monoid homomorphism on list concatenation, `⊕-fold (xs ++ ys) == ⊕-fold xs ⊕ ⊕-fold ys`, checked at `xs`, `ys`. """ -oplus_fold_append_holds(M::Monoid, xs, ys) = +function oplus_fold_append_holds(M::Monoid, xs, ys) + # Materialise once: `vcat` of two generators would nest them as elements. + xs, ys = collect(xs), collect(ys) oplus_fold(M, vcat(xs, ys)) == M.op(oplus_fold(M, xs), oplus_fold(M, ys)) +end """ GroupAggregator(agg) @@ -1380,9 +1384,11 @@ equals combining `aggregate_values` of each, checked at `vs`, `ws`. Honest scope: the fold's homomorphism property, NOT SQL GROUP-BY's full operational semantics. """ -aggregation_as_fold_holds(G::GroupAggregator, M::Monoid, vs, ws) = +function aggregation_as_fold_holds(G::GroupAggregator, M::Monoid, vs, ws) + vs, ws = collect(vs), collect(ws) # see oplus_fold_append_holds aggregate_values(G, M, vcat(vs, ws)) == M.op(aggregate_values(G, M, vs), aggregate_values(G, M, ws)) +end # --- The four concrete instances (ℕ modelled as non-negative Int) ----- diff --git a/test/runtests.jl b/test/runtests.jl index 7048e57..043bc1e 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -472,6 +472,13 @@ using Test @test oplus_fold_append_holds(sum_monoid(), Int[], [4, 5]) @test oplus_fold_append_holds(min_monoid(), Union{Nothing,Int}[], Union{Nothing,Int}[]) + # Generators / lazy iterables are accepted (not nested by `vcat`). + @test oplus_fold_append_holds(sum_monoid(), (x for x in 1:2), (y for y in 3:4)) + @test oplus_fold_append_holds(sum_monoid(), (x for x in 1:6 if x > 2), (y for y in 3:4)) + @test aggregation_as_fold_holds(count_aggregator(), sum_monoid(), + (v for v in 1:2), (v for v in 3:5)) + @test oplus_fold(sum_monoid(), (x for x in 1:3 if x > 1)) == 5 + # Concrete fold values. @test oplus_fold(sum_monoid(), [1, 2, 3]) == 6 @test oplus_fold(max_monoid(), [1, 5, 3]) == 5 From 9ef30befcadb25258be31b2e82669c1b28cc465b Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 20 Oct 2026 13:18:57 +0000 Subject: [PATCH 4/5] fix: flatten array inputs to the fold-law checks (Codex P2) collect preserves array shape, and vcat of two matrices stacks rows instead of appending their iteration sequences, so with a non-commutative monoid (string concatenation) oplus_fold_append_holds returned false on inputs that satisfy the law. Inputs now go through a small _items helper (vec(collect(xs))), used by oplus_fold, oplus_fold_append_holds and aggregation_as_fold_holds. Arrays are read in column-major iteration order. Adds 3 assertions (294 -> 297); the append check failed before the change. Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- README.adoc | 2 +- src/EchoTypes.jl | 12 ++++++++---- test/runtests.jl | 7 +++++++ 3 files changed, 16 insertions(+), 5 deletions(-) diff --git a/README.adoc b/README.adoc index 1104cfe..d705d71 100644 --- a/README.adoc +++ b/README.adoc @@ -247,7 +247,7 @@ cementing-negative `+EchoLLEncoding+` (LL shallow-encoding gap with paired source-side no-section). Unreleased on top of v0.3.0: `+EchoAggregation+` (mirrored from echo-types `+703dd77+`, not from `+eed4250+`). Test suite: -*294 passing assertions across 21 testsets*, organised as finite shadows of named Agda lemmas +*297 passing assertions across 21 testsets*, organised as finite shadows of named Agda lemmas plus the semantic-fibre vocabulary exercise over the kernel. Registered as `+EchoTypes+` in the hyperpolymath professional registry; *not* registered in the Julia General registry and intentionally *not* part of diff --git a/src/EchoTypes.jl b/src/EchoTypes.jl index c966c52..472b5c5 100644 --- a/src/EchoTypes.jl +++ b/src/EchoTypes.jl @@ -1334,16 +1334,20 @@ function monoid_laws_hold(M::Monoid, samples) Iterators.product(ss, ss, ss)) end +# Items of a finite iterable as a plain Vector in iteration order. `vec` drops +# any array shape, so `vcat` appends sequences rather than stacking rows. +_items(xs) = vec(collect(xs)) + """ oplus_fold(M, xs) -`⊕-fold`: fold a list (any finite iterable, materialised once) through the +`⊕-fold`: fold a list (any finite iterable, materialised once as a flat vector) through the monoid as a RIGHT fold, `x₁ ⊕ (x₂ ⊕ (… ⊕ ε))` (`foldr op ε`), matching Agda's `foldr`. For an associative `op` the direction is immaterial; for a non-associative one the result depends on it, so this fixes the reading falsifiers are run against. """ -oplus_fold(M::Monoid, xs) = foldr(M.op, collect(xs); init = M.ε) +oplus_fold(M::Monoid, xs) = foldr(M.op, _items(xs); init = M.ε) """ oplus_fold_append_holds(M, xs, ys) -> Bool @@ -1353,7 +1357,7 @@ oplus_fold(M::Monoid, xs) = foldr(M.op, collect(xs); init = M.ε) """ function oplus_fold_append_holds(M::Monoid, xs, ys) # Materialise once: `vcat` of two generators would nest them as elements. - xs, ys = collect(xs), collect(ys) + xs, ys = _items(xs), _items(ys) oplus_fold(M, vcat(xs, ys)) == M.op(oplus_fold(M, xs), oplus_fold(M, ys)) end @@ -1385,7 +1389,7 @@ Honest scope: the fold's homomorphism property, NOT SQL GROUP-BY's full operational semantics. """ function aggregation_as_fold_holds(G::GroupAggregator, M::Monoid, vs, ws) - vs, ws = collect(vs), collect(ws) # see oplus_fold_append_holds + vs, ws = _items(vs), _items(ws) # see oplus_fold_append_holds aggregate_values(G, M, vcat(vs, ws)) == M.op(aggregate_values(G, M, vs), aggregate_values(G, M, ws)) end diff --git a/test/runtests.jl b/test/runtests.jl index 043bc1e..21e6516 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -479,6 +479,13 @@ using Test (v for v in 1:2), (v for v in 3:5)) @test oplus_fold(sum_monoid(), (x for x in 1:3 if x > 1)) == 5 + # Arrays of any shape are read as their flat iteration sequence, so + # `vcat` appends them rather than stacking rows (non-commutative `*`). + S = Monoid("", *) + @test oplus_fold_append_holds(S, ["a" "b"], ["c" "d"]) + @test aggregation_as_fold_holds(GroupAggregator(identity), S, ["a" "b"], ["c" "d"]) + @test oplus_fold(S, ["a" "b"; "c" "d"]) == "acbd" # column-major order + # Concrete fold values. @test oplus_fold(sum_monoid(), [1, 2, 3]) == 6 @test oplus_fold(max_monoid(), [1, 5, 3]) == 5 From dc1dd40c640470ae2aa8f7c9a9685b8fcf251d92 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 20 Oct 2026 13:25:53 +0000 Subject: [PATCH 5/5] fix: concatenate fold inputs without promotion; pair_sum is Int-only (Codex P2 x2) - oplus_fold_append_holds / aggregation_as_fold_holds joined their inputs with vcat, which promotes element types (an Int next to a Float64 is converted, and can round). With an exact non-promoting max this reported a false counterexample on a lawful monoid. They now use _concat, which keeps each element as given. - pair_sum and pair_sum_is_fold accepted any Integer tuple, but sum_monoid's unit is an Int, so Int8 inputs overflowed in the direct sum but not in the fold and pair_sum_is_fold returned false. The example models N as non-negative Int, so both methods are restricted to Tuple{Int,Int}. Both reproduced before the change. Adds 5 assertions (297 -> 302). Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- README.adoc | 2 +- src/EchoTypes.jl | 25 +++++++++++++++++++------ test/runtests.jl | 12 ++++++++++++ 3 files changed, 32 insertions(+), 7 deletions(-) diff --git a/README.adoc b/README.adoc index d705d71..cd518c4 100644 --- a/README.adoc +++ b/README.adoc @@ -247,7 +247,7 @@ cementing-negative `+EchoLLEncoding+` (LL shallow-encoding gap with paired source-side no-section). Unreleased on top of v0.3.0: `+EchoAggregation+` (mirrored from echo-types `+703dd77+`, not from `+eed4250+`). Test suite: -*297 passing assertions across 21 testsets*, organised as finite shadows of named Agda lemmas +*302 passing assertions across 21 testsets*, organised as finite shadows of named Agda lemmas plus the semantic-fibre vocabulary exercise over the kernel. Registered as `+EchoTypes+` in the hyperpolymath professional registry; *not* registered in the Julia General registry and intentionally *not* part of diff --git a/src/EchoTypes.jl b/src/EchoTypes.jl index 472b5c5..4b6cacc 100644 --- a/src/EchoTypes.jl +++ b/src/EchoTypes.jl @@ -1338,6 +1338,11 @@ end # any array shape, so `vcat` appends sequences rather than stacking rows. _items(xs) = vec(collect(xs)) +# Concatenate two item lists WITHOUT promoting element types: `vcat` of an +# Int vector and a Float64 vector converts the integers, which can round them +# and make a lawful monoid look as if it violated the append law. +_concat(xs, ys) = append!(append!(Any[], xs), ys) + """ oplus_fold(M, xs) @@ -1356,9 +1361,10 @@ oplus_fold(M::Monoid, xs) = foldr(M.op, _items(xs); init = M.ε) `⊕-fold (xs ++ ys) == ⊕-fold xs ⊕ ⊕-fold ys`, checked at `xs`, `ys`. """ function oplus_fold_append_holds(M::Monoid, xs, ys) - # Materialise once: `vcat` of two generators would nest them as elements. + # Materialise once (`vcat` of two generators would nest them as elements) and + # concatenate without type promotion. xs, ys = _items(xs), _items(ys) - oplus_fold(M, vcat(xs, ys)) == M.op(oplus_fold(M, xs), oplus_fold(M, ys)) + oplus_fold(M, _concat(xs, ys)) == M.op(oplus_fold(M, xs), oplus_fold(M, ys)) end """ @@ -1390,7 +1396,7 @@ operational semantics. """ function aggregation_as_fold_holds(G::GroupAggregator, M::Monoid, vs, ws) vs, ws = _items(vs), _items(ws) # see oplus_fold_append_holds - aggregate_values(G, M, vcat(vs, ws)) == + aggregate_values(G, M, _concat(vs, ws)) == M.op(aggregate_values(G, M, vs), aggregate_values(G, M, ws)) end @@ -1435,8 +1441,15 @@ no_canonical_disaggregation_of(agg_map, x, y) = # --- Example-PairSum: the macro instance (ℕ × ℕ -> ℕ by +) ------------- -"`pairSum (a , b) = a + b`." -pair_sum(p::Tuple{Integer,Integer}) = p[1] + p[2] +""" + pair_sum(p) + +`pairSum (a , b) = a + b` on `ℕ × ℕ`, with ℕ modelled as non-negative `Int`. +Restricted to `Int` on purpose: a narrower integer type would overflow here +while the `sum_monoid` fold (whose unit is an `Int`) would not, breaking +`pair_sum_is_fold` for inputs the method accepted. +""" +pair_sum(p::Tuple{Int,Int}) = p[1] + p[2] """ pair_sum_is_fold(p) -> Bool @@ -1444,7 +1457,7 @@ pair_sum(p::Tuple{Integer,Integer}) = p[1] + p[2] `pairSum-is-fold`: `pair_sum` IS the `sum_monoid` fold of its two fields, so the macro instance is a special case of the general form. """ -pair_sum_is_fold(p::Tuple{Integer,Integer}) = +pair_sum_is_fold(p::Tuple{Int,Int}) = pair_sum(p) == oplus_fold(sum_monoid(), [p[1], p[2]]) "`ledger₁ = (0 , 1)`." diff --git a/test/runtests.jl b/test/runtests.jl index 21e6516..c1cefb8 100644 --- a/test/runtests.jl +++ b/test/runtests.jl @@ -479,6 +479,14 @@ using Test (v for v in 1:2), (v for v in 3:5)) @test oplus_fold(sum_monoid(), (x for x in 1:3 if x > 1)) == 5 + # Concatenation does not promote element types: an exact (non-promoting) + # max over an Int and a Float64 that `vcat` would have rounded together. + X = Monoid(0, (a, b) -> a > b ? a : b) + @test monoid_laws_hold(X, [0, 1, 2, 2^53, 2^53 + 1, 0.5]) + @test oplus_fold_append_holds(X, [2^53 + 1], [Float64(2^53)]) + @test aggregation_as_fold_holds(GroupAggregator(identity), X, + [2^53 + 1], [Float64(2^53)]) + # Arrays of any shape are read as their flat iteration sequence, so # `vcat` appends them rather than stacking rows (non-commutative `*`). S = Monoid("", *) @@ -509,6 +517,10 @@ using Test @testset "Aggregation: Example-PairSum macro instance + no-section (EchoAggregation.agda)" begin # pairSum is the sumMonoid fold of its two fields. @test all(pair_sum_is_fold, [(a, b) for a in 0:4 for b in 0:4]) + # ℕ is modelled as Int: a narrower type would overflow in `pair_sum` but + # not in the fold, so it is rejected rather than silently disagreeing. + @test_throws MethodError pair_sum((Int8(100), Int8(100))) + @test_throws MethodError pair_sum_is_fold((Int8(100), Int8(100))) # Many-to-one: distinct ledgers, one total, distinct echoes. @test pair_sum_collapses()