|
| 1 | +// SPDX-License-Identifier: CC-BY-SA-4.0 |
| 2 | +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | += ECHOTYPES.JL — next-Claude handoff: the EchoAggregation mirror (2026-06-27) |
| 4 | +:toc: macro |
| 5 | +:toclevels: 2 |
| 6 | + |
| 7 | +_A ready-to-paste prompt that orients a fresh Claude session on porting the general |
| 8 | +`EchoAggregation` from this repo (echo-types, Agda) into its executable Julia companion |
| 9 | +`EchoTypes.jl`. Copy the block under <<the-prompt>> verbatim into a new session opened in |
| 10 | +an `EchoTypes.jl` checkout. Everything outside that block is framing for a human reader; |
| 11 | +the block itself is self-contained._ |
| 12 | + |
| 13 | +[NOTE] |
| 14 | +==== |
| 15 | +This is a *handoff*, not an affirmation or a roadmap. It lives in *echo-types* because |
| 16 | +echo-types is the Agda *source of truth* for the result being mirrored — but the actual |
| 17 | +work happens in the *separate* `EchoTypes.jl` repository, which is **not** part of the |
| 18 | +cloud session that wrote this file. Open a fresh local session in an `EchoTypes.jl` clone |
| 19 | +(e.g. on the desktop app) and paste the prompt there. |
| 20 | +
|
| 21 | +The dated, signed receipt of what was true and checked on the Agda side is |
| 22 | +`AFFIRMATION.adoc` (repo root); the musts/intends/wishes detail is |
| 23 | +`docs/status/STATUS-2026-06-19.adoc`. This file just gets the mirror session productive fast. |
| 24 | +==== |
| 25 | + |
| 26 | +toc::[] |
| 27 | + |
| 28 | +[#the-prompt] |
| 29 | +== The prompt (paste this verbatim) |
| 30 | + |
| 31 | +[source,markdown] |
| 32 | +---- |
| 33 | +You are picking up work in **EchoTypes.jl**, the executable Julia companion to the Agda |
| 34 | +repo **echo-types**. EchoTypes.jl mirrors the finite-domain shadow of echo-types and |
| 35 | +*falsifies-by-counterexample on concrete data* — the Agda always stays the source of truth. |
| 36 | +This is the repo `hyperpolymath/EchoTypes.jl`. |
| 37 | +
|
| 38 | +TASK |
| 39 | +Add an `EchoAggregation` module that mirrors the GENERAL monoid/group aggregation that |
| 40 | +landed in echo-types as `proofs/agda/EchoAggregation.agda` (issue #175; also covers the |
| 41 | +no-section sibling #174). The macro-economics reading is just one instance of it. |
| 42 | +
|
| 43 | +THE SOURCE OF TRUTH (echo-types, already merged to main) |
| 44 | +`proofs/agda/EchoAggregation.agda` ships, under `--safe --without-K`, zero postulates: |
| 45 | +- `record Monoid ℓ` — `Elem`, `ε`, `_⊕_`, `assoc`, `identity-l`, `identity-r`. |
| 46 | +- `⊕-fold` over a list, and `⊕-fold-++` : the fold is a MONOID HOMOMORPHISM over `_++_` |
| 47 | + (folding a concatenation = combining the two folds). |
| 48 | +- `record GroupAggregator {ℓ} (K V) (M)` with `agg : V → Elem`, plus `aggregate-values` |
| 49 | + and the *proved* headline law `aggregation-as-fold` (aggregating a concatenation equals |
| 50 | + combining the aggregates). |
| 51 | +- Instances: `sumMonoid` / `countMonoid` / `maxMonoid` over ℕ (0/+/⊔) and `minMonoid` over |
| 52 | + `Maybe ℕ` (`nothing` = ∞), plus a worked `countAggregator`. |
| 53 | +- `no-canonical-disaggregation-of` — generic non-disaggregability: any collision (two |
| 54 | + distinct values with the same aggregate) ⇒ no section, via `no-section-of-collapsing-map`. |
| 55 | +- `module Example-PairSum` — the macro `ℕ × ℕ → ℕ` ledger: `pairSum (a,b) = a+b` IS literally |
| 56 | + the `sumMonoid` fold of a two-element list (`pairSum-is-fold`), with `pairSum-non-injective` |
| 57 | + and `no-canonical-disaggregation` (the Sonnenschein–Mantel–Debreu / representative-agent |
| 58 | + critique, type-theoretically). |
| 59 | +
|
| 60 | +WHAT TO BUILD (Julia, executable, property-tested — keep it a finite-domain falsifier) |
| 61 | +1. A `Monoid` struct (carrier, identity `ε`, op `⊕`) and `⊕fold(m, xs)` over a `Vector`, |
| 62 | + with a property test that the homomorphism law holds on random finite data: |
| 63 | + `⊕fold(m, vcat(xs, ys)) == ⊕fold(m, xs) ⊕ ⊕fold(m, ys)`. |
| 64 | +2. Instances: `sumMonoid`, `countMonoid`, `maxMonoid` over `Int` (0 / + / max), and |
| 65 | + `minMonoid` over `Union{Nothing,Int}` (`nothing` = ∞). Property-test each one's identity |
| 66 | + and associativity laws on random data. |
| 67 | +3. `aggregate_values(agg, kvs)` plus a test of `aggregation-as-fold`. |
| 68 | +4. `pairsum((a,b)) = a + b`, with tests witnessing: `pairsum_is_fold` (it equals the |
| 69 | + `sumMonoid` fold of `[a, b]`), non-injectivity (two distinct pairs, same sum), and |
| 70 | + no-canonical-disaggregation (exhibit that no left inverse / section exists on a concrete |
| 71 | + collision — a chosen "raise" cannot satisfy `raise ∘ pairsum == id` because two pairs map |
| 72 | + to the same total). |
| 73 | +
|
| 74 | +HONEST SCOPE (preserve — do not overclaim) |
| 75 | +- `aggregation-as-fold` is the fold's monoid-HOMOMORPHISM law, NOT full SQL GROUP-BY |
| 76 | + operational semantics. |
| 77 | +- `avg` is deliberately ABSENT — it is not a monoid. Express it as `sum / count`. |
| 78 | +- no-canonical-disaggregation refutes a *section* (a LEFT inverse), NOT the existence of |
| 79 | + *some* representative choice. Do NOT restate it as a failed surjection — the aggregate map |
| 80 | + is onto; the content is that no disaggregating section exists. |
| 81 | +
|
| 82 | +HOUSE RULES (non-negotiable) |
| 83 | +- EchoTypes.jl is a **Julia package** — not Rust, not Agda. Follow the existing `Echo*` |
| 84 | + module conventions (look at e.g. `EchoTotalCompletion`, `EchoLossTaxonomy`, and how |
| 85 | + `test/runtests.jl` is structured). Wire the new module into the package and its test suite. |
| 86 | +- Branch: do all work on `claude/ecstatic-wright-OBEvx` (create locally if absent); open a |
| 87 | + **draft** PR; never push to another branch without explicit permission. Use the GitHub MCP |
| 88 | + tools for PRs (no `gh` CLI). Note this estate squash-merges and deletes the branch each |
| 89 | + round, so start from current `main`. |
| 90 | +- Licence: SPDX header on every file. Julia *code* in this estate is `MPL-2.0`; long-form |
| 91 | + *prose* is `CC-BY-SA-4.0`. Check the headers already in the repo and match them. |
| 92 | +- Commits signed (`git commit -S`) with the session's standard `Co-Authored-By` + |
| 93 | + `Claude-Session` footers; PR body carries the standard Claude Code footer. |
| 94 | +- Attribution string: write **"Claude Opus 4.8"** in any attestation; never put a bare |
| 95 | + model-id slug in a committed artefact, commit message, or PR body. |
| 96 | +
|
| 97 | +BUILD / TEST |
| 98 | + julia --project=. -e 'using Pkg; Pkg.instantiate()' |
| 99 | + julia --project=. -e 'using Pkg; Pkg.test()' |
| 100 | +
|
| 101 | +FIRST MOVE |
| 102 | +Read an existing `Echo*` module + `test/runtests.jl` to learn the repo's shape. Add |
| 103 | +`EchoAggregation` + its `@testset`, get `Pkg.test()` green, open a draft PR on |
| 104 | +`claude/ecstatic-wright-OBEvx`, and cross-reference echo-types #175 (and #174). |
| 105 | +
|
| 106 | +DO NOT REOPEN (settled on the Agda side) |
| 107 | +- The general/macro split: the macro economics IS the `Example-PairSum` instance of the |
| 108 | + general `EchoAggregation`; nothing is re-proved. |
| 109 | +- The no-section refutation target (a *left* inverse — exactly what non-disaggregability |
| 110 | + denies). |
| 111 | +- The citation-level scope of the cross-repo bridge (there is no Agda↔Julia import path; the |
| 112 | + Julia mirror re-implements the finite shadow and falsifies on data — it does not import the |
| 113 | + Agda). |
| 114 | +---- |
| 115 | + |
| 116 | +== Pointers (for the human handing this over) |
| 117 | + |
| 118 | +* *Where the work happens:* the separate `hyperpolymath/EchoTypes.jl` repo (Julia). This |
| 119 | + handoff is filed in echo-types only because echo-types holds the spec being mirrored. |
| 120 | +* *The spec to mirror:* `proofs/agda/EchoAggregation.agda` (general monoid/group form, #175); |
| 121 | + its honest scope is documented in that module's guardrail and in `docs/echo-types/MAP.adoc`. |
| 122 | +* *Issues:* echo-types *#175* (general `EchoAggregation`) and *#174* (the no-section sibling |
| 123 | + the generic `no-canonical-disaggregation-of` also discharges). |
| 124 | +* *Precedent:* EchoTypes.jl v0.2.0 already mirrors several `Echo*` modules |
| 125 | + (`EchoTotalCompletion`, `EchoLossTaxonomy`, `EchoEntropy`, …) as finite-domain falsifiers — |
| 126 | + follow that established pattern for the new `EchoAggregation` shadow. |
| 127 | +* *Cross-repo receipts:* echo-types `AFFIRMATION.adoc` + `docs/status/STATUS-2026-06-19.adoc` |
| 128 | + are the verified-Agda-side snapshot; the oikos `MacroAggregation` reading |
| 129 | + (`oikos/docs/alib-aggregate-bridge.adoc`) is the macro instance cited at the design level. |
0 commit comments