feat: iteration abstractions

[JamesGallicchio]

• Typeclasses for foldl, foldr, and non-directional folds
• Iterable typeclass for collections that can produce a Stream-like iterator object. Used to implement Std.Range folds, and more generally for any collection where external iteration is the more natural iteration

[kmill]

Is there a reason to reinvent the Lean 4 core ToStream and Stream interfaces? https://github.com/leanprover/lean4/blob/bb8cc08de85f3daf67c6fb3feda245681c4b56fd/src/Init/Data/Stream.lean#L43

ToStream is the toIterator function, and Stream is the step function. There's a comment at the top of the file why they rejected Iterable (it involves a universe bump).

[JamesGallicchio]

Yep, in this case I want the universe bump. The reason it was avoided in core is because IO is not universe-polymorphic, and the devs wanted Streams to work in IO.

I haven't really run into this issue yet (because so far in my uses, I haven't had to pass an Iterable value across a bind, even in monadic functions), and I find the iterator type packed instead of parameter to be more intuitive to work with.

But I'm not super attached to the exact type here if there's good reason to use others.

[kmill]

While it might be more intuitive for you, do you want to be duplicating pre-existing API? If Iterable exists, I think at the least it should be packaging up ToStream and Stream into a single bundle.

There's also the rule of thumb we've learned in mathlib, which is that type fields in structures/classes are usually not a great idea, though maybe it's justified here because you're specifically wanting to hide the iterator type.

(I know this PR is in draft status -- I hope I'm not being too severe with this review! I just want to help you make sure your developments are in line with the rest of the library.)

[JamesGallicchio]

Iterable was intended to compete with the ToStream API, yeah. At one point I had some relationship between Iterable and ToStream (I think the former gave an instance of the latter?) which can of course be added back.

I think the reason why the type field works with Iterable is that they almost always appear as transitory, compile-time constants with relatively clean definitional equalities. Consumers of Iterable never care what the iterator type is, since the only thing you can do is apply step.

The Fold based API in leancolls is much more fleshed out than the Iterable API, so having early feedback here is helpful.

[joehendrix]

Close for inactivity. Reopen if needed.