[DRY?] Direct definition vs. generic combinators, ctd. in Algebra.Definitions.RawMonoid

[jamesmckinna]

Addition: suggest adding to Data.Vec.Functional.Base

-- Non-empty folds

foldr₁ : (A → A → A) → Vector A (suc n) → A
foldr₁ {n = zero}  _⊕_ xs = head xs
foldr₁ {n = suc _} _⊕_ xs = (head xs) ⊕ foldr₁ _⊕_ (tail xs)

foldl₁ : (A → A → A) → Vector A (suc n) → A
foldl₁ _⊕_ xs = foldl _⊕_ (head xs) (tail xs)

(and perhaps also retrofitting to Data.Vec.Base, too)

Refactoring: suggest replacing the definitions in Algebra.Definitions.RawMonoid with

sumʳ sumˡ sum : ∀ {n} → Vector Carrier n → Carrier

sumʳ {n = zero}  xs = 0#
sumʳ {n = suc _} xs = Vector.foldr₁ _+_ xs

sumˡ {n = zero}  xs = 0#
sumˡ {n = suc _} xs = Vector.foldl₁ _+_ xs

sum = Vector.foldr _+_ 0#

(with the last one for backwards compatibility; but even for right-associative addition, sumʳ avoids redundancy in the {n = 1} case)
and then also

_×_ : ℕ → Carrier → Carrier
n × x = sum (Vector.replicate n x)

_×′_ : ℕ → Carrier → Carrier
n ×′ x = sumˡ (Vector.replicate n x)

(again: using sumʳ in the first definition might be an improvement? although a breaking change...)

BUT as to performance/intensional reduction behaviour:

• it seems that replacing the existing direct definitions of _×_ and _×′_ in this way, even with {-# INLINE ... #-} directives, just doesn't quite give the correct unfolding behaviour for the existing proofs in Algebra.Properties.Monoid.Mult.* to go through properly;
• is there some way to achieve this? (eg by more inlining? if so, how/when do we decide what's appropriate; stdlib seems to be quite sparing in its appeals to such 'extralogical' techniques)
• would such a change actually be more efficient in practice than the existing direct definitions?

It seems as though the 'generic' definitions ought to be more robust/reusable/'better' (esp. as Vector.replicate is simply const, so the use of head and tail in the various folds is inlinable/eliminable?), but it just ... doesn't quite seem to work :-(

Any help/insight into how to (understand how to) resolve this trade-off welcome! It feels as though I am missing something fundamental, but possibly non-obvious, about what's going on here.

[JacquesCarette]

Ghastly. But such is the fate of the functional representation. So much right-programming, just when I'd gotten used to the beauty of left-programming!

I wish there were a better symbol than _×_. Again, something less symmetric would be nice.

[jamesmckinna]

Not quite sure what "Ghastly" is referring to... but:

• the existing 'right' definition (ie. sum/_×_) makes clear it is for simplicity and ease of proving properties, while the 'left' (_×′_) is 'optimised for type-checking'; the refactorings attempt to systematise this even-handedly for right as well as left... as well as going via the still-more general summation operators...
• the choice of symbols is also 'legacy', but as part of Add new Bool action on a RawMonoid plus properties #2450 I'm experimenting with new notation, towards deprecation of the existing choices (but as with my comments on that PR, I'm not as doctrinaire about any symmetric connotation, or otherwise, for existing symbols, or else we wouldn't have chosen _∙_ for a Magma operation... ;-) and while I understand that the notations for Algebras expect a single/homogeneous sorting of the operation(s), the fact that we have a two-sorted operation doesn't a priori mean, for me at least, that we need some kind of 'handedness' for the associated symbol, as the type does the disambiguation... whether Agda's parser is smart enough to do that, however, is another matter?) That said, suggestions welcome!
• the choice of Data.Vec.Functional is also 'legacy', but I don't see much point in trying to relitigate that (although others have suggested doing so); but I'm not sure that would necessarily affect the question at hand, namely why does using fold incur a penalty wrt equational reasoning?

The (implied) criticism of existing choices in stdib is part of the reason for my interest in refactoring here, but any (further) insights into how to deal that, and especially the last point, as painlessly as possible would be welcome!

[jamesmckinna]

Second thoughts on the refactoring: cf. the twist on Russell's "the advantages of theft over honest toil" being that there's always a choice between making a definition (and getting the property 'for free', except that you have to show equivalence with the 'old'/'standard' one), and sticking with the 'old' definition and proving a property; in this case one way out of the bottle is simply to prove, in Algebra.properties.Monoid.Mult that:

• n × x ≈ sum (Vector.replicate n x) and (UPDATED: and this is already the symmetric form of Algebra.Properties.Monoid.sum-replicate!)
• n ×′ x = sumˡ (Vector.replicate n x)

(UPDATED: needed to rethink what I had previously written)