Add foldMap and fold

[Taneb]

List is a free monoid

I'd like to have some properties for bag-and-set equality. foldMap f is a commutative monoid morphism from lists with bag equality, and an idempotent commutative monoid morphism from lists with set equality, but I don't know how to prove these.

[MatthewDaggitt]

Hmm I'm not sure these functions really belong here for a couple of reasons. For starters we don't want to drag in the entire algebra hierarchy into Data.List.Base if we can help it. Secondly these are really just re-implementing foldr right under the assumption we're within a monoid, and we don't want to have to reprove all the properties we already have for foldr.

I think there is potential for wrapping foldr under the assumption of we're within a monoid, but I'm a bit unsure where to put it in the library. Anyone have any suggestions?

[gallais]

Data.List.Categorical? foldMap is essentially traverse with the writer monad.

[Taneb]

I accept the argument that it shouldn't be in .Base but .Categorical doesn't feel like the right place to me. Maybe a new Data.List.Algebraic?

[JacquesCarette]

Data.List.Algebraic seems fine. Data.List.Traversals could work too. Certainly should not be in .Base.

[jamesmckinna]

Thinking out loud... and bearing in mind that lists-modulo-permutation with [] and ++ is one concrete representation of the free commutative monoid, and one close to the heart of anyone who tried verification of sorting algorithms... a long time ago...

Why not add a new layer to the Algebra.* module hierarchy that specifically introduces Free structures. That way, such a module imports from the underlying algebra, and the underlying concrete representing type, but produces an abstract construction satisfying the suitable universal property...

[MatthewDaggitt]

Why not add a new layer to the Algebra.* module hierarchy that specifically introduces Free structures. That way, such a module imports from the underlying algebra, and the underlying concrete representing type, but produces an abstract construction satisfying the suitable universal property...

Could you give an example of what a definition of such a free structure would like?

[jamesmckinna]

Hmmm... I see that might require a bit more than mere casual effort, as well as making me think harder about how to understand the existing Algebra.* hierarchy. But it definitely strikes me that

• on the one hand, one wants to know that a given concrete representation 'is' free (or in other words, to know that the underlying carrier of the Free algebra is intensionally the concrete data type, so that it can be used in computation)
• on the other that the notion of Free construction is only ever 'up-to' (ie it's abstract) The latter point was dragging me towards the Algebra.* hierarchy for such results:
• statement of the universal Free property, in terms of appropriate Morphism types
• definition of one such concrete RawY structure/bundle
• proof that it satisfies the Free characterisation But I can see this needs more work before I can confidently make the case. This is more time than I perhaps have right now. Let's see what the Christmas lockdown affords me in terms of (thinking) time.

[JacquesCarette]

As it turns out, the proper notion of Free has recently landed in agda-categories (https://agda.github.io/agda-categories/Categories.FreeObjects.Free.html).

I've been meaning to revisit free commutative monoid. I've got a completely bit-rotted version that goes all out and proves it's indeed the expected left adjoint. The tricky part is that everything needs to go "Setoid" (which is fine wrt the current library) and proof-relevant. (Actually, I've got multiple bit-rotted versions of that in that repo, I'm not even sure which one is the least rotted.)

There are quite a few 'Free' structures in that repo that are not bit-rotted. I really need to finish writing that paper... The interesting thing is that there's a couple more properties that are nice that arise when you prove full adjoint instead of just 'free'.

[Taneb]

I'm revisiting is. Was there any problem with putting the properties in Data.List.Properties?

[jamesmckinna]

So... none of the above suggestions had *.Properties as a candidate destination, and I definitely think it shouldn't go there, because it is not a general property of parametrically polymorphic lists, but only of those for which the carrier type has additional IsMonoid structure...

Instead, I'd still argue for a place under Algebra.Properties.(Commutative)Monoid, on the model of sum under Algebra.Properties.(Commutative)Monoid.Sum , with a different list/vector representation there, but that's the point: fold and foldMap are witnessing homomorphism properties which hold independently of the representation of the underlying carrier type of the free object at hand. So I, personally, don' t think they belong as properties of such representing data types at all, but of the associated Algebra gadgetry.

Indeed, for a general (haskell) Functor instance f, Foldable f iff ∀ a. Monoid a → Algebra f a where the latter is the 'usual' notion of a being an f-algebra, viz. there's a map f a → a. List is but one such Functor... cf #1099

[JacquesCarette]

I agree with @jamesmckinna .

[Taneb]

As I've said before, I really don't think that things like foldMap should go in the Algebra.* hierarchy.

If I understand what @jamesmckinna is proposing, it's to have in Algebra.Properties.Monoid.Sum or somewhere similar the function foldMap : (A -> M) -> List A -> M. where M is the carrier of a Monoid.

This will work find until we have two different representations of lists, at which point it's not clear where they should live. (this is not an idle concern, I've been off-and-on-again working on Okaski random-access lists). It also falls if we also want to have foldMap for Vec over Monoids.

If we instead have a generic specification of what a foldMap function ought to be, we still have the problem of where to put the instances of this specification. For this problem, we have precedent to help us: instances for algebraic structures (like Monoid), except when they are "fundamental" in some sense like the trivial monoid, have been put in the *.Properties modules, e.g. Data.Nat.Properties.+-monoid.

[jamesmckinna]

Nathan, thanks once more for the considered response. [EDITED sorry I hit send before finishing the thought]

While I am indeed arguing for something like Algebra.Properties.Monoid.Fold (and even that such a thing would subsume Sum in the obvious way), I am actually arguing for (much) more: that such a module (or: the constructions it embodies, plus their properties) should take an arbitrary (container) Functor as a parameter.

Then List would naturally arise as one such, but so would all the others. The question of indexed containers such as Vec is indeed a bit more challenging.

As for the precedent(s) of optimising for the common cases of Nat, List etc. and their structures, I think there is then a question about how we think parameterised modules (or module constructions) should be instantiated: at call-/import-sites, or with dedicated versions...? But in the examples you cite, and for the representation I proposed for foldMap, that would lead to Data.X.Base defining RawFunctor instances, and Data.X.Properties as defining their companion IsFunctor instances.

Or have I misunderstood what you want under Data.X.Properties?

[Taneb]

What would the contents of such a module be?

[jamesmckinna]

We would, of course, also need the definitions of Algebra f a for Functor f and carrier a. The RawAlgebra notion here is simply f a -> a as we would have it in eg haskell, but being an 'algebra for a functor' (as well as 'algebra for a monad' all the more so) needs some additional equations... and I think we would at least want (for any decent 'algebraic' functor) a 'singleton' map on f , a -> f a together with the equation a -> f a -> a = id. Algebras for a monad would require a lot more, commutation with the multiplication etc.

[Taneb]

Before this morning it had been a long time since I've thought about this PR, so I'll state my current design idea explicitly:

Somewhere in the Data.List hierarchy add a function foldMap : (M : Monoid c l) -> (A -> M.Carrier) -> List A -> M.Carrier. When I first opened this PR I was warned not to add this to Data.List.Base but I think that's not as bad now as we pass a RawMonioid rather than a Monoid and not increase at all Data.List.Base's dependency graph.

In Data.List.Properties provide proofs of the following properties, given M : Monoid c l:

• foldMap-[]-homo : foldMap f [] == epsilon
• foldMap-++-homo : foldMap f xs <> foldMap f ys == foldMap (xs ++ ys)
• A property showing that foldMap and [_] make lists a free monoid. (I haven't worked out exactly what this would look like).

I'd also like to add similar for Vec and Vec.Functional eventually.

I don't understand why you think we need to define an Algebra type for Functors.

[jamesmckinna]

Well, looking at Data.List.Effectful, and Data.List.Instances, I would think the best place to put instances of an IsFoldable structure would be in the former for the definitions and properties, and the latter for declaring the instances. Looking back over the thread, this was @gallais's suggestion originally, I think (modulo the renaming in v2.0 of Categorical to Effectful).

[JacquesCarette]

I really dislike that Data.List.Base depends on any part of Algebra at all. Those bundles should be defined, IMHO, in Data.List.Bundles (which could certainly be re-exported by Data.List) In this particular case, the parts of Algebra have been properly split up, so that the harm to the dependency graph is quite minimal, so it's not urgent that it be refactored.

Data.List.Folds ? Or indeed, Data.List rather than Data.List.Core ?