Bird–Wadler duality of list folds

In their 1988 book Introduction to Functional Programming [BW88], Richard Bird and Philip Wadler stated three duality theorems between foldl and foldr. Denoting the combining function as f, the theorems are:

1. If α = β and f is commutative and associative, l.foldl = l.foldr
2. If f is left-commutative, l.foldl = l.foldr
3. l.reverse.foldl = l.foldr and l.reverse.foldr = l.foldl

Note that f's type differs between Lean's foldl (β → α → β) and foldr (α → β → β), so flips need to be inserted judiciously. For the history behind this type difference see the appendix to [Dan23], which uses a version of foldl where f : α → β → β to derive among other things a slight generalisation of the first theorem:

1. If α = β, f is associative and a commutes with all x : α, l.foldl f a = l.foldr f a

Main declarations

• List.foldl_eq_foldr_of_commute, List.foldl_eq_foldr: first duality theorem.
• List.foldl_flip_eq_foldr, List.foldr_flip_eq_foldl: second duality theorem.

The third duality theorem is in the standard library under the names List.foldl_reverse, List.foldr_eq_foldl_reverse, List.foldr_reverse and List.foldl_eq_foldr_reverse.

theorem List.foldl_cons_nil {α : Type u_1} {l : List α} : foldl (flip cons) [] l = l.reverse

theorem List.foldl_cons_eq_apply_foldl {α : Type u_1} {β : Type u_2} {l : List α} {v : β → α → β} {a : α} {b : β} [hv : RightCommutative v] : foldl v b (a :: l) = v (foldl v b l) a

theorem List.foldr_cons_eq_foldr_apply {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β → β} {a : α} {b : β} [hf : LeftCommutative f] : foldr f b (a :: l) = foldr f (f a b) l

theorem List.foldl1_eq_foldr1 {α : Type u_1} {l : List α} {f : α → α → α} [ha : Std.Associative f] {a b : α} : f (foldl f a l) b = f a (foldr f b l)

theorem List.foldl_eq_foldr_of_commute {α : Type u_1} {l : List α} {a : α} {f : α → α → α} [Std.Associative f] (ha : ∀ (x : α), f a x = f x a) : foldl f a l = foldr f a l

First Bird–Wadler duality theorem.

theorem List.foldl_eq_foldr {α : Type u_1} {l : List α} {a : α} {f : α → α → α} [hf : Std.Commutative f] [Std.Associative f] : foldl f a l = foldr f a l

First Bird–Wadler duality theorem for commutative functions.

theorem List.foldl_flip_eq_foldr {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β → β} {b : β} [LeftCommutative f] : foldl (flip f) b l = foldr f b l

Second Bird–Wadler duality theorem.

theorem List.foldr_flip_eq_foldl {α : Type u_1} {β : Type u_2} {l : List α} {v : β → α → β} {b : β} [RightCommutative v] : foldr (flip v) b l = foldl v b l

Second Bird–Wadler duality theorem.

@[deprecated List.foldl_cons_eq_apply_foldl (since := "2026-04-02")]

theorem List.foldl_eq_of_comm' {α : Type u_1} {β : Type u_2} {l : List α} {v : β → α → β} {a : α} {b : β} [hv : RightCommutative v] : foldl v b (a :: l) = v (foldl v b l) a

Alias of List.foldl_cons_eq_apply_foldl.

@[deprecated List.foldr_cons_eq_foldr_apply (since := "2026-04-02")]

theorem List.foldr_eq_of_comm' {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β → β} {a : α} {b : β} [hf : LeftCommutative f] : foldr f b (a :: l) = foldr f (f a b) l

Alias of List.foldr_cons_eq_foldr_apply.

@[deprecated List.foldr_flip_eq_foldl (since := "2026-04-02")]

theorem List.foldl_eq_foldr' {α : Type u_1} {β : Type u_2} {l : List α} {v : β → α → β} {b : β} [RightCommutative v] : foldr (flip v) b l = foldl v b l

Alias of List.foldr_flip_eq_foldl.

---

Second Bird–Wadler duality theorem.

@[deprecated List.foldl_cons_eq_apply_foldl (since := "2026-04-02")]

theorem List.foldl_eq_of_comm_of_assoc {α : Type u_1} {β : Type u_2} {l : List α} {v : β → α → β} {a : α} {b : β} [hv : RightCommutative v] : foldl v b (a :: l) = v (foldl v b l) a

Alias of List.foldl_cons_eq_apply_foldl.

@[deprecated List.foldl1_eq_foldr1 (since := "2026-04-02")]

theorem List.foldl_op_eq_op_foldr_assoc {α : Type u_1} {l : List α} {f : α → α → α} [ha : Std.Associative f] {a b : α} : f (foldl f a l) b = f a (foldr f b l)

Alias of List.foldl1_eq_foldr1.

@[deprecated List.foldl_cons_eq_apply_foldl (since := "2026-04-02")]

theorem List.foldl_assoc_comm_cons {α : Type u_1} {β : Type u_2} {l : List α} {v : β → α → β} {a : α} {b : β} [hv : RightCommutative v] : foldl v b (a :: l) = v (foldl v b l) a

Alias of List.foldl_cons_eq_apply_foldl.