sum as an accumulating fold; sum-++ by way of fold-++

[jamesmckinna]

At present, Data.Vec.Base.sum specialises the base case of its defining fold to be 0.
This toy/low-hanging fruit PR introduces,
in Data.Vec.Base:

• fold-sum n xs with accumulating parameter n
• sum = fold-sum 0

and in Data.Vec.Properties:

• fold-sum n xs ≡ sum xs + n
  and then a new (equivalent) proof of
• sum-++ using foldr-++ and the above lemma

[MatthewDaggitt]

Hmm so I have to confess I don't quite see the advantage of writing fold-sum n xs over sum xs + n?

[jamesmckinna]

Hmmm... fair comment, except: it irked me (what a world, where my pet peeves become PRs ;-)) that the the proof of sum,-++ appears to be an opportunistic property of sum, rather than a generic property of folds, cashed out in a specific instance...
... but to then to be able exploit that genericity, one needs an accumulator-style presentation of sum... fold-sum (terrible name), of which sum itself then becomes an instance. The function fold-sum, and its characteristic property, are all and only to mediate between sum-as-special-instance, and sum-as-generic-fold-with-accumulator. But the two expressions you identify above are not defintionally equal*, only provably so.

So there's a systematisation pay-off, I suppose, on the one hand, at the cost of a lemma factorisation on the other. Potayto, potahto.

[MatthewDaggitt]

Hmm, I kind of see where you're coming from, but I think fold-sum as a function is unlikely to be a useful addition in its own right. If you're concerned about making the proof more general, I think better to generalise even further to something like the following lemma about fold:

foldr-extractBase : (M : CommutativeMonoid a l) (open CommutativeMonoid M) →
                    ∀ (e xs : Vec ℕ m) → foldr _∙_ e xs ≡ foldr ε xs + e

[jamesmckinna]

Interesting comment! And related (perhaps) to @Taneb 's PR #1281 ... for a more comprehensive treatment?

[jamesmckinna]

But for now, suggest we label this one status: abandoned?