feat(category/fold): foldl and foldr for traversable structures

[cipher1024]

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

For reviewers: code review check list

[rwbarton]

Could we get a brief top-level overview comment for users? In particular, the first half or so of the file is internal implementation stuff--possibly confusing for someone who wants to understand what the module is for.

list_foldl_eq could be generalized (in view of list.to_list_eq_self) to traversable.foldl f x xs = list.foldl f x (traversable.to_list xs), right? And the same for foldr.

[cipher1024]

Good catch, thanks! I also forgot the copyright statement. What do you think of:

`foldl` and `foldr` generalized to any `traversable` collection. 

For the generalization, I'm not sure which direction to go because we could also rewrite most of the foldl / foldr lemmas to make them about any traversable collection. The downside is that foldl and foldr now require more modules to reason about. With regards to your comment, the generalization would be needed if we want to translate a theorem about traversable.foldl into one about list.foldl so that the list lemmas can be used.

[rwbarton]

I'm not sure exactly what the uses of such lemmas would look like, but my guess is that it would generally be easier to turn everything into lists and then apply list lemmas. What kind of lemmas for traversable.foldl did you have in mind? The ones I can think of involve some extra operations on lists like cons, which aren't available for an arbitrary traversable. For a particular traversable instance where such extra operations are available you could add lemmas about the behavior of those operations under to_list.

By the way, one other lemma that would probably be useful is that to_list is a natural transformation, i.e., it commutes with map.

[cipher1024]

You might be right about turning everything into lists. Especially since I'm starting to doubt that the generalization is provable. One idea is to to use the composition law but it involves two transformations applied on the same structure of type t but with foldl_to_list the structure is changing half-way. Maybe I'll get more luck with the naturality law.

The ones I can think of involve some extra operations on lists like cons, which aren't available for an arbitrary traversable. For a particular traversable instance where such extra operations are available you could add lemmas about the behavior of those operations under to_list.

Me too. The problem with having a type class for cons is that its applicability is limited to lists and list-like structures: no prod, no sum, no option, no vector or array. Maybe adding a requirement about injectivity of to_list could already help us.

[cipher1024]

@rwbarton I've started proving that to_list and map commute using the naturality of traversable but I'm getting nowhere. Now I'm starting to look in the direction of quotient types but I don't I'd check in here before I go down that rabbit hole. Do you have any advice?

[rwbarton]

I guess the problem stems from the fact that α → α is not functorial in α, so you can't get an applicative transformation of the shape you want.

Maybe a first question to ask is: do you have a good sense of the operational behavior of foldl and foldr? Is it possible to make one of them (I guess foldl) operate in O(1) space at least some of the time (for list for example)? That might influence the implementation.

[cipher1024]

I believe I have a somewhat good intuition of the operational behavior at least of foldl. It's basically a state monad without return value so it should only use enough memory to store one state.

foldr is very similar but I don't know if it can benefit from the same optimizations as foldl because foldr is basically a state monad without result and run backwards.

[rwbarton]

Sorry, the first part of my previous comment didn't make much sense. Let me try again.

traversable.foldl and traversable.foldr should have their own naturality laws, which should follow directly from traverse_map. Then I think traversable.to_list is basically defined as reverse of traversable.foldl applied to something, so the naturality law for to_list should follow.

Then the other thing one would like to know is that traversable.foldl can in turn be defined in terms of to_list. I will think a little more about that one.

[cipher1024]

Ok, I proved it and it's kind of anticlimactic: I'm using the following applicative:

def fold (α : Type u) (β : Type v) := list α

[cipher1024]

What does the naturality laws of traversable.foldl and traversable.foldr look like?

[rwbarton]

Yes, you can also do it that way and then prove it is equal to the original by using the naturality law (using an applicative transformation from const (list a) to const (list a -> list a)).

[rwbarton]

What does the naturality laws of traversable.foldl and traversable.foldr look like?

Like the list versions.

@[simp] theorem foldl_map (g : β → γ) (f : α → γ → α) (a : α) (l : list β) : foldl f a (map g l) = foldl (λx y, f x (g y)) a l :=
by revert a; induction l; intros; simp *

@[simp] theorem foldr_map (g : β → γ) (f : γ → α → α) (a : α) (l : list β) : foldr f a (map g l) = foldr (f ∘ g) a l :=
by revert a; induction l; intros; simp *

[cipher1024]

The foldl / foldr naturality laws were surprisingly easy. Now I'm trying to use them to prove the naturality of to_list and I get down to:

traverse ((foldl.lift ∘ flip (flip cons)) ∘ f) l nil = map f (traverse (foldl.lift ∘ flip (flip cons)) l nil)

which feels like a dead end. At first glance, map_traverse seems like it should help but the problem is that map f applies on a list, not the applicative. Any idea if any natural transformation could get us across the finish line?

[rwbarton]

I have the following idea for expressing traversable.foldl in terms of list.foldl and traversable.to_list. It seems possibly more complicated than necessary, but it seems like it might work. Define a new applicative by

structure both {α : Type u} {β : Type v} (f : α → β → α) :=
(one : α → α)
(two : list β)
(one_eq_two : ∀ a, one a = list.foldl f a two)

This has applicative morphisms to both α → α and list β. You should be able to construct a traversal which projects to, on the one hand, traversable.foldl, and on the other hand traversable.to_list. Then take the equality field one_eq_two of the result of applying traverse with that. Using the naturality laws, you can rewrite the left side to traversable.foldl and the right hand side to list.foldl applied to traversable.to_list.

I probably have some of the details wrong, but this approach seems like it might work.

[cipher1024]

hamster in wheel in brain running, running, running I think I can get some milage out of that. Thanks!

Do you suggest that this new applicative would be an intermediate value in the proof so that one can be the implementation and two can be at the core of the proof?

[rwbarton]

Nice!

I figured out what was bothering me about my both approach. Namely, both is isomorphic to just the two field, because the value of two determines the value of one. I think that that means that you should be able to write down applicative transformations (one for foldl, foldr) from list β to α → α which can also be used to describe traversable.foldl/traversable.foldr in terms of their corresponding to_list functions. Not sure whether that would simplify the proofs really.

[cipher1024]

Thanks for the hints @rwbarton, it worked! It's really beautiful too :)

[cipher1024]

I think that that means that you should be able to write down applicative transformations (one for foldl, foldr) from list β to α → α which can also be used to describe traversable.foldl/traversable.foldr in terms of their corresponding to_list functions.

I was wondering how much we could erase both but even though two characterizes the whole type, let's not forget that the type of both contains f which is essential for obtaining one from two

[cipher1024]

I take back what I said, I don't think f is essential for two to work properly. I have a few steps of converting from both f' to both f under two because of that. I think removing both will be an improvement.

[cipher1024]

It works! And removing both (actually both versions bothl and bothr which threatened to multiply further) cuts down 100 lines of proof out 311 :)

[cipher1024]

With these results in mind, I think a case could be made for a class foldable that has to_list, foldl, foldr, mfoldl and mfoldr with the laws I proved here. I don't have examples of types that are foldable but not traversable so I think I would leave out such a class for now.

[cipher1024]

@spl You are truly evil

[spl]

😕 Why?

[cipher1024]

I'm joking. Because your initial commit was worded as a massacre and now you're coming back for more??

But seriously, I'm truly grateful for these improvements.

[spl]

I'm joking. Because your initial commit was worded as a massacre and now you're coming back for more??

Ah. 😆 🔨🔪

But seriously, I'm truly grateful for these improvements.

I'm glad!

[spl]

This is looking good! I made a few cosmetic changes after @cipher1024. One thing I was wondering was if there was a way to unify the different types used for their applicative instances. I thought maybe something like this could help, but I'm not sure.

def const (α : Type u) (β : Type v) : Type u := α

[cipher1024]

This is something I thought about too. This is how it would be done in Haskell. It feels weird to have a multiplicative monoid instance for lists. It's a bit less weird for endofunctions though.

[spl]

Also, @cipher1024, could you add a few comments to the functor/applicative types? In particular, I think it would be good to note how the to_list traverse is inefficient and therefore not practically usable. That way, you don't have oblivious people like me coming along and doing stupid things. You could perhaps put a comment on the to_list function, too.

[cipher1024]

Yes, good idea!

[cipher1024]

We could use const (list a), const (endo b) and const (dual (endo b)) with proper monoid instances, similar to how I would do it in Haskell. But then, the comments you asked for would have nowhere to go.

[spl]

But then, the comments you asked for would have nowhere to go.

Even if they only went on the to_list function, which I assume would still be there?

[johoelzl]

@cipher1024 @rwbarton I tried to resolve this with the opposite PR #627 but now it fails at this point, obviously doesn't prove the laws for free

[rwbarton]

I can look into what's going on there, but this PR shouldn't be using the opposite category anyways. Instead it should be using the opposite monoid (#538).

[cipher1024]

@rwbarton Does that make a difference?

[rwbarton]

We might end up merging the opposite types. But the instances added in this PR have nothing to do with categories so they should not be in category_theory; they belong in algebra as in #538.

[rwbarton]

Is the renaming tests -> test intentional?

[rwbarton]

Also, if it is intentional, it is better to do this kind of renaming in a separate PR, merge it, and rebase this one. That way this PR will not accumulate conflicts with the renamed files as they are modified by other commits.

[cipher1024]

The renaming is intentional because leanpkg test runs those tests explicitly. Otherwise, I agree. Maybe I should split this PR into three PRs: rename tests, change category_theory and then everything about fold. How about that?

[rwbarton]

Sounds good. Note that I already put the examples -> instances change in #641, though the Travis build failed for some reason...

[johoelzl]

Yes, please split this PR into separate parts.

[cipher1024]

@rwbarton @johoelzl @spl : Now that the PR is skinnier, any thoughts?

[spl]

@cipher1024 I'm looking at it now. 💯 on the documentation and presentation!

I currently have just one small concern that has no bearing whatsoever on the acceptance of the PR. I really like the example proofs in the comments, but I don't really like that the example proofs are in comments 😉 because they are not checked. Is it appropriate for examples to be here, or is there another appropriate place for them?

[semorrison]

Properly checked examples sounds good to me. Someday we'll work out how to get a faster computer for Kenny. :-)

…

On Tue, Feb 5, 2019, 6:08 PM Sean Leather ***@***.*** wrote: @cipher1024 <https://github.com/cipher1024> I'm looking at it now. 💯 on the documentation and presentation! I currently have just one small concern that has no bearing whatsoever on the acceptance of the PR. I really like the example proofs in the comments, but I don't really like that the example proofs *are in* comments 😉 because they are not checked. Is it appropriate for examples to be here, or is there another appropriate place for them? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#376 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAdLBFNkXBNunPDU6dQ4OCXVMZSQatlcks5vKS3wgaJpZM4W9hBZ> .

[spl]

Just a few minor things.

[cipher1024]

I currently have just one small concern that has no bearing whatsoever on the acceptance of the PR. I really like the example proofs in the comments, but I don't really like that the example proofs are in comments 😉 because they are not checked. Is it appropriate for examples to be here, or is there another appropriate place for them?

I love the idea! Thanks for suggesting it. The only issue I have is that, if I make those into examples, they won't come up as part of foldl's docstring. Maybe I should duplicate them?

[cipher1024]

The last calculation in the docstring doesn't type check and I feel like what I have to do to get it to type check obscurs the ideas. I think I'm not going to add the examples. I'll remember the idea nonetheless and see if there's a nice way of applying it.

[johoelzl]

Let's finally merge this.