Where should homomorphisms live in the `stdlib` hierarchy?

[jamesmckinna]

Knocking off the last outstanding task in Issue #1851 re-raised a question in my mind as well regarding where, in general, proofs homomorphism-like properties belong in the library: under the source type, in *.Properties, or somewhere else?

For example, in PR#1852 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. Similar considerations apply, mutatis mutandis, to @Taneb 's recent #1857 / #1863 : I don't regard List.length as being a homomorphism from List _ to Nat as a property of List _, rather it's a (consequence of the) universal property of the free monoid construction, of which List _ is merely a very convenient representative for the underlying carrier type of that free algebra.

Moreover the amount of additional work involved in these proofs, and especially also for the Semiring homomorphism parity from Nat to Parity, led me eventually to write this last one in a module on its own; I was at the limits of how to disambiguate all the various equational/algebraic reasoning from that already intrinsic to the structure of Nat itself, when I first tried to shoehorn this proof into Data.Nat.Properties.

It struck me before I embarked on this, but especially now afterwards, and with a categorical eye on what's going on, that it doesn't make sense to me to regard this homomorphism as a property inherent to Nat, importing structure from Parity: rather that each (through the particular lens of their respective Semiring structure) participates in the construction of a new structure/bundle, taking components from the (intrinsic/internal) Properties of each type Nat and Parity... and neither 'side' has ownership of the homomorphism. Rather, if rather prosaically, I've constructed an arrow in the (Set-/Setoid- based) category of Semirings and their homomorphisms... such that each of the Properties modules is responsible for witnessing that Nat resp. Parity is even permitted to be considered as candidate domain/codomain for such an arrow. But the arrow itself lives/should live... somewhere else, associated in the hierarchy with the abstract algebraic structure involved.

Accordingly, I suggest/propose that we have a new hierarchy below Algebra.Homomorphism|Morphism, corresponding to each of the (concrete) categories of algebras where the domain/codomain of any such homomorphism should live.

All of these decisions may already have been debated/decided/resolved in agda-categories, so it would be nice to get input from that community (esp. @JacquesCarette ?), as well perhaps as this being further impetus to migrate that development into stdlib itself...

Discussion and suggestions welcome!

(And my especial thanks to @MatthewDaggitt and @Taneb for forcing me to put my money where my mouth is ;-) The views above are, of course, entirely my own, but I might hope might be more widely shared...)

[MatthewDaggitt]

I agree the asymmetry is somewhat displeasing. The main issue I see with this proposal is dependency cycles.

1. Locally - we often exploit the morphisms within the Properties files themselves. For example most of the properties of Data.Rational.Properties are lifted via the morphisms from Data.Rational.Unnormalised.Properties....

2. Globally - there's a similar situation in Data.Nat.Binary. If we were to lift all the homomorphisms out to a global module with all homomorphisms, then to use the morphisms between the unary and binary representations of Nat we'd end up pulling in Data.Rational.Properties into the dependency graph for Data.Nat.Binary which is highly undesirable....

[jamesmckinna]

Food for thought! Thanks! I'll respond once I've digested the comments (I may need to walk back on things I wrote above and write them more clearly; I think you may have misunderstood me under 2)) and also looked at how the existing structures participate in the current library design (esp. under 1)).

[MatthewDaggitt]

Ah were you suggesting a single module per morphism target pair? e.g. one for (Nat, Sign), one for (Int, Nat) etc.?

[jamesmckinna]

[EDITED to roll my three comments into one] Exactly, with the name of such modules being not the domain, codomain pair, but the underlying function witnessing the homomorphism, so Algebra.Homomorphism.Semiring.parity, for example. And with the corresponding module contents being 'thin' on the @JacquesCarette model: only the necessary imports and the bundled record witnessing the IsXHomomorphism 'property'/construction.

[JacquesCarette]

Finally catching up, now that I've submitted the paper due today... Key to this is

and neither 'side' has ownership of the homomorphism

In agda-categories, there is a place for Functors, namely Categories.Functor.Instance.*, which is then named after the functor itself, not the domain-codomain pair. The extra Instance is because we also have Construction, where we differentiate between things that 'are' Functors and things that build Functors out of some other data. (This makes even more sense for categories).

In this case, I think Algebra.Homomorphism.Semiring.Parity is great. Unlike Functor, there are many kinds of homomorphisms in algebra, so tagging it with the kind is needed. And then naming it after the action is great. So I'm very happy with that naming.

And yes, this does have the advantage of being 'thin' and thus not leading to import cycles.

[MatthewDaggitt]

Exactly, with the name of such modules being not the domain, codomain pair, but the underlying function witnessing the homomorphism, so Algebra.Homomorphism.Semiring.parity, for example.

Hmm so the problem with this naming scheme is that its not unique. For example, there will be a zillion toNat modules. Type pairs obviously aren't necessarily unique either so we probably need a FUNCTION-DOMAIN-CODOMAIN naming scheme?

[MatthewDaggitt]

So that just leaves this issue:

Locally - we often exploit the morphisms within the Properties files themselves. For example most of the properties of Data.Rational.Properties are lifted via the morphisms from Data.Rational.Unnormalised.Properties....

Which I don't see addressed anywhere. How will the current contents of Data.Binary.Properties be structured for example? It has a load of proofs, which then are used to prove the homomorphisms, which are then used to prove a load more stuff.

[JacquesCarette]

If I were doing that, I'd split it along additive, multiplicative, order, etc lines. Data.Binary.Properties.Additive and the like.

[jamesmckinna]

I don't (yet) have good solutions to the problems raised by @MatthewDaggitt , sorry to say. Agree that there are too many toNat definitions... but that's itself a consequence of the original design, surely? (and perhaps that means parity in Data.Nat.Base should be called toParity?) Agree that we use one lot of homomorphism definitions in then processing properties of others, and maybe for certain existing modules, that's how it will stay (as fossil remains for a more ambitious refactoring PR another day). But the question is at least as much one going forward about where new stuff should be put. But @JacquesCarette 's comments suggest that one solution to the Rational / Binary wrinkle is to slice up the problem into smaller bites.

[JacquesCarette]

i've definitely found that the vast majority of import cycles and like issues can be solved by slicing things into smaller modules.

[jamesmckinna]

Closing this now as we seem to have argued ourselves out of my (much) more fine-grained position towards having individual definitions of *-(Is)Homomorphism lemmas occur... wherever (but mostly in *.Properties it seems).