Add Haskell's Foldable

[MatthewDaggitt]

The results in Algebra.Operations.CommutativeMonoid would really benefit from being proved over a suitable Foldable structure rather than individually for List/Vec/Vector etc.

See https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Foldable.html

Perhaps someone whose familiar with it, could suggest whether we can leverage dependant types to improve the definition somehow?

[gallais]

I don't think it's a low hanging fruit. Foldable cannot fit in a record like
Functor or Monad do because of size issues!

[jespercockx]

Can't we just have a Foldable that is parametrized over the level of the return type? At least that's what @UlfNorell did in https://github.com/UlfNorell/agda-prelude/blob/master/src/Container/Foldable.agda.

[jamesmckinna]

Cf. My ICFP2017 talk at TyDe on Foldable https://icfp17.sigplan.org/track/tyde-2017-papers (and Tarmo Uustalu's independent discovery of the same thing somewhat earlier): it would be nice to have a suitable setting in which that characterisation is provable, and hence, as a by-product, be able to dispense with Foldable altogether... But the higher-rank characterisation perhaps hints at what dark level-polymorphic magic might be required to achieve that end.

[jamesmckinna]

And yes, let's please try to have this: sum and product have no business being defined in Data.List.Base, being special to ℕ ... which means that Data.List.Properties ends up importing Data.Nat.Divisibility in order to establish a single property of product, while properties of sum such as sum-++ are not defined as instances of the corresponding general property of foldr: not a rational approach, IMNSVHO.

UPDATED This specific point is handled by #2558 (and #2561 for the Bool counterparts).

[jamesmckinna]

Meanwhile, is the general issue now closed by #2300 ? I hope so!