Swapping the arguments of foldl's f

Stream: lean4

[Jeremy Tan]

The current definition of foldl is

def List.foldl {α : Type u} {β : Type v} (f : α → β → α) : (init : α) → List β → α
  | a, nil      => a
  | a, cons b l => foldl f (f a b) l

However, Olivier Danvy in his paper Folding left and right matters: Direct style, accumulators, and continuations argues that this is wrong and it should be

def List.foldl' {α : Type u} {β : Type v} (f : β → α → α) : (init : α) → List β → α
  | a, nil      => a
  | a, cons b l => foldl' f (f b a) l

The advantages of foldl' over foldl are listed in the paper:
image.png

I would like to replace foldl with foldl'. Shall we do it?

(Disclaimer: I am taking Danvy's module CS6217 Topics in Programming Languages and Software Engineering this semester at NUS.)

[Henrik Böving]

This seems like far too large of a breaking change in the eco system to pull off at this point, you'd have to change thousands and thousands of invocations.

[Jeremy Tan]

In that case, would it be possible to just add the foldl' function alongside and explain why Danvy prefers this?

[Robin Arnez]

I mean foldl' f is just foldl (flip f), right? This doesn't seem like we'd need a new definition

[Jeremy Tan]

Then why did my lecturer write that paper?

[Eric Wieser]

My guess is that point 1 of that paper is about providing the student with a better tool to remember which one is foldr and which is foldl

[Eric Wieser]

But we have docstrings to disambiguate that (or at least, we should)

[Eric Wieser]

Point 2 and 3 seem to be moot, because Lean is happy to generalize arguments behind the scenes when doing induction.

[Jeremy Tan]

Robin Arnez said:

I mean foldl' f is just foldl (flip f), right? This doesn't seem like we'd need a new definition

Right then

[Jeremy Tan]

Danvy's principal languages are Rocq, Scheme and OCaml, not Lean

[Jeremy Tan]

I decided to make a PR adding foldl' anyway, as foldf: lean4#12653

[Thomas Murrills]

Re: the actual reasoning for foldl': Interesting! I am not convinced by the first bullet applies for an eager language like lean, though. I would contend that in f (f (f init 1) 2) 3, it is f init 1 that's happening "first". I'm curious if the author is referring to a different notion of "order"; "evaluation order" may admittedly not be the intended order here.

I also think the current argument order for the argument to foldl nicely allows us to visualize the function as having accumulated the elements "behind" the current element when looking at the current element, left-to-right: visually, if f := fun acc x => ..., we're dealing with a picture like [ (acc), x, ...]. The elements prior to x appear to have been aggregated "in place" to acc, and so it "makes sense" that the argument acc comes before x.

The real benefits admittedly might be in the next two bullets, and I have not explored those myself. :)

[Jeremy Tan]

How do I fix this? I can't push to lean-pr-testing-12653
image.png

[Matt Diamond]

I don't think you linked to the right PR above

[Jeremy Tan]

Matt Diamond said:

I don't think you linked to the right PR above

Fixed

[Jeremy Tan]

The procedure for mathlib CI is no longer clear from the linked docs

[Jeremy Tan]

(PR has been downstreamed to #35713)

[Kim Morrison]

Jeremy Tan said:

The procedure for mathlib CI is no longer clear from the linked docs

@Jeremy Tan, is there a particular point where the docs are unclear? I'd like to improve these.

Yes, you can't push directly to lean-pr-testing-NNNN. I recommend making a PR to it, and pinging me (on Zulip).

[Jeremy Tan]

@Kim Morrison I do not think the docs say that you should make the mathlib adaptation PR on the nightly-testing repo. (Also, where do you make it for batteries?)