List.length is a monoid homomorphism

[Taneb]

We should probably also add raw magma and monoid bundles to Data.List.Base as an extension to #1755.

[jamesmckinna]

EDITED As with my comment to issue #1851, it's not obvious to me where homomorphisms (and proofs that they are such) properly belong. We might (and will?) carry on making honourable exceptions for ones such as List.length here, but at some point either the imports will get so heavy (or even circular, if we seek to show two structures isomorphic), or else Data.X.Base Data.X.Properties ends up that way.

[Taneb]

In this case I was expecting to put it in Data.List.Properties in the "Properties of _++_" section. We'll need length-++ to prove these in any case, so it can't go in Data.List.Base.

[MatthewDaggitt]

@jamesmckinna, apart from the lack of symmetry, what is wrong with putting them in Properties files?

[jamesmckinna]

@Taneb I agree they they perhaps 'properly' belong in Data.List.Properties, but for the frequent refrain that these fundamental modules in the hierarchy groan under their own weight. I hadn't intended that they go in .Base, sorry for the implied confusion --- hope that the revised edit above makes this clear(er).

But, to answer @MatthewDaggitt 's question, it was my own thinking about Parity and Sign that had got me wondering about where things should go (plus a nod to @JacquesCarette 's frequent calls for 'thinner' modules), and the sense that while the lemmas that are required to show that length is a homomorphism might belong in Properties, the structure which bundles that data (function plus proofs) does/might not. Not least because the homomorphism property (and even its existence by virtue of freeness of List) is a higher-level API for length than the mere assemblage of properties as above. But indeed, in the symmetric cases such as isomorphism, there is a genuine question if we are not to have circular imports.

So not so much a question of 'wrong' as one of 'where best?'. But happy to take the push-back. EDITED and as per @MatthewDaggitt 's comment on #1852, I'll move discussion to a fresh general issue.