Repository navigation
Feat/echo aggregation mirror - #34
Merged
Merged
Conversation
…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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
- 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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
…(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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
Contributor
|
Note Currently processing new changes in this PR. This may take a few minutes, please wait... ⚙️ Run configuration
📒 Files selected for processing: 3
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.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
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
Closes #
Type of change
How has this been verified?
Checklist
git commit -S).SPDX-License-Identifier(code/configMPL-2.0,prose
CC-BY-SA-4.0); I did not relicense existing files.Notes for reviewers