Data.Parity as per issue #1851

[jamesmckinna]

UPDATED:

• Parity admits a commutative semiring structure (with 0 = 0ℙ; 1 = 1ℙ etc.)
• a function parity from Nat to Parity in Data.Nat.Base
• a function toSign from Parity to Sign
• a function fromSign from Sign to Parity
• proofs that (toSign, fromSign) form an abelian group iso from (Parity, 0, _+_) to (Sign, +, _*_)
• miscellaneous tidyings up of Data.Sign etc. to reflect new names for algebraic structures/bundles, cf. issue Data.Integer.Properties.+-isAbelianGroup should be called +-0-isAbelianGroup #1844 and in line with review comments on current PR
• CHANGELOG

Not TODO (for subsequent PR):

• proof that parity is a commutative semiring homomorphism from Nat to Parity [fixes #1894] parity is a semiring homomorphism #1904
• rationalise the many instances in the library where the 0, 1, 2+ n pattern analysis of a Nat argument takes place (esp. wrt N{-}ary operations and Reflection, as well as the obvious Binary and Nat examples); but see this branch and PR rationalise use of suc (suc n) and suc n@(suc _) patterns throughout; remove 2+ _ pattern #1870

[MatthewDaggitt]

Looks good to me. Left some comments.

To be honest, this looks like a good size PR. If we resolve my comments above, then I'm happy to merge this in and then leave the morphisms to a second PR.

It raised a question in my mind as well regarding where homomorphism-like properties belong in the library: under the source type, in .Properties, or somewhere else? I currently have Parity import Sign in order to define the operations, but it strikes me that there's an asymmetry to that decision, which might better be reflected in having subdirectories of the Algebra. hierarchy which record concrete instances of (Semi)RingHomomorphisms etc. suggestions welcome!

Having Data.Parity import Data.Sign is absolutely fine. That's how the rest of the library operates. Yes, in theory you could pull everything out to some neutral ground in Algebra but it would be very hard to find, and you'd probably end up re-exporting it publicly into the Data modules again which would greatly complicate the dependencies.

[jamesmckinna]

OK, @MatthewDaggitt thanks for the comments, and the suggestion to slice the PR up.
As for things being hard-to-find... I had hoped there might be instant acclaim/agreement/assent to the suggestion of Algebra.Homomorphism.AbelianGroup.* as a place for such things to go, with individual modules concerning one and only one such structure (so that eventually, we might have long list of such things, but none of them 'hard-to-find'?).
As for the need for subsequent re-importing, you may well have a point, but I'd want to see it before commenting further.

[MatthewDaggitt]

As for things being hard-to-find... I had hoped there might be instant acclaim/agreement/assent to the suggestion of Algebra.Homomorphism.AbelianGroup.* as a place for such things to go, with individual modules concerning one and only one such structure (so that eventually, we might have long list of such things, but none of them 'hard-to-find'?).

Feel free to open an issue dedicated especially to discussing this issue, with your proposal and we can have a discussion 👍 I agree, it's definitely something worth thinking about!

[jamesmckinna]

Removed duplicate bundles, and renamed according to the scheme in Data.Nat, for consistency's sake, but I have got thoroughly confused as to whether the names of various structures/bundles do/should or not include their units.

[jamesmckinna]

I didn't know how to manage all the equation/inequational reasoning in Nat.Properties together with equational reasoning across the parity function: the typechecker kept complaining about how to resolve ambiguities in the ≡-Reasoning... and it is too late at night now to think sensibly about this... so it is in a module on its own (reflecting my earlier sympathies/inclinations/thoughts on the topic)

[MatthewDaggitt]

@jamesmckinna I thought we had (twice!) agreed that we weren't going to add anything more to this PR? Please could remove the last commit from branch, so that I can merge it in without having to go put the whole thing through any more review cycles. As discussed, we can then open a new PR with the second set of additions.

[jamesmckinna]

Ooops. How to I reverse out of this? git revert <commit-hash>? Only this last commit needs to go, I think.

[jamesmckinna]

I think, as well, that the subtlety of how 'agreement' is arrived at as to the size of a PR is clearer to you than to me. And of course, enthusiasm to finish a task carried me away somewhat...

[MatthewDaggitt]

Ooops. How to I reverse out of this? git revert ? Only this last commit needs to go, I think.

IGNORE (SEE BELOW): I tend to use git rebase -i HEAD^X where X is the number of commits I want to go back. You then delete the offending commit from the opened file, and it should then remove it for you.

I think, as well, that the subtlety of how 'agreement' is arrived at as to the size of a PR is clearer to you than to me. And of course, enthusiasm to finish a task carried me away somewhat...

So a PR should be opened as a request for comment/approval on a "completed" unit of work. Obviously some changes may be made in response to the comments, but the ideally the core contribution of the PR should not change. The problem with continuously adding to an open PR is that it becomes very difficult to the reviewers to re-review things efficiently, as they don't know how it interacts with what was already in the PR, so they often end up having to look through the previously reviewed stuff again. Yes, it's possible to view the subsequent commits individually, but it is still difficult to then mentally map those on to the final code that is going to be committed.

[MatthewDaggitt]

I tend to use git rebase -i HEAD^X where X is the number of commits I want to go back. You then delete the offending commit from the opened file, and it should then remove it for you.

Sorry, this was bad advice! That only works when you're working on a private local branch. If the branch is shared, then it is problematic as it changes the history. You're right, revert is the right way to go.

[jamesmckinna]

Hope that worked, and apologies for (once again) blundering around/treading on toes. No need on your part to apologise for the git advice... especially in the face of my 'learning by breaking things'. I'm not actively trying to break the maintainer, but I see the effect now... 🤦

[MatthewDaggitt]

No worries, all looks good now! Thanks for making the requested changes 👍