Zulip Chat Archive

Stream: Is there code for X?

Topic: A Different `finset.fold`


view this post on Zulip Marcus Rossel (Jan 16 2021 at 10:42):

The definition of finset.fold is explained as follows:

fold op b f s folds the commutative associative operation op over the f-image of s,
i.e. fold (+) b f {1,2,3} = f 1 + f 2 + f 3 + b.

The consequence of this is that the types of b and f x have to match.
Is there someway to perform a fold over a finset, where b can have a different type than f x?
And e.g. the requirement could be that ...

∀ (x y : α) (b : β), op (op b (f x)) (f y) = op (op b (f y)) (f x)

view this post on Zulip Eric Wieser (Jan 16 2021 at 11:00):

I suspect the issue is that the typeclasses used to express the current docs#finset.fold don't exist to express what you suggest

view this post on Zulip Eric Wieser (Jan 16 2021 at 11:03):

(I guess this applies to docs#multiset.fold too)

view this post on Zulip Eric Wieser (Jan 16 2021 at 11:08):

Ah, I think you want (s.1.map f).foldr op b (docs#multiset.foldr)

view this post on Zulip Marcus Rossel (Jan 16 2021 at 12:10):

Ahhh that's exactly it. Thanks for always being so helpful @Eric Wieser!


Last updated: May 17 2021 at 16:26 UTC