Aggregation: concatenate fold inputs without promotion; pair_sum is Int-only

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

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,16 +1441,23 @@ 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
 
 `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)`."

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()