# Documentation

Mathlib.Control.Fold

# List folds generalized to Traversable#

Informally, we can think of foldl as a special case of traverse where we do not care about the reconstructed data structure and, in a state monad, we care about the final state.

The obvious way to define foldl would be to use the state monad but it is nicer to reason about a more abstract interface with foldMap as a primitive and foldMap_hom as a defining property.

def foldMap {α ω} [One ω] [Mul ω] (f : α → ω) : t α → ω := ...

lemma foldMap_hom (α β)
[Monoid α] [Monoid β] (f : α →* β)
(g : γ → α) (x : t γ) :
f (foldMap g x) = foldMap (f ∘ g) x :=
...


foldMap uses a monoid ω to accumulate a value for every element of a data structure and foldMap_hom uses a monoid homomorphism to substitute the monoid used by foldMap. The two are sufficient to define foldl, foldr and toList. toList permits the formulation of specifications in terms of operations on lists.

Each fold function can be defined using a specialized monoid. toList uses a free monoid represented as a list with concatenation while foldl uses endofunctions together with function composition.

The definition through monoids uses traverse together with the applicative functor const m (where m is the monoid). As an implementation, const guarantees that no resource is spent on reconstructing the structure during traversal.

A special class could be defined for foldable, similarly to Haskell, but the author cannot think of instances of foldable that are not also Traversable.

@[reducible]
def Monoid.Foldl (α : Type u) :

For a list, foldl f x [y₀,y₁] reduces as follows:

calc  foldl f x [y₀,y₁]
= foldl f (f x y₀) [y₁]      : rfl
... = foldl f (f (f x y₀) y₁) [] : rfl
... = f (f x y₀) y₁              : rfl


with

f : α → β → α
x : α
[y₀,y₁] : List β


We can view the above as a composition of functions:

... = f (f x y₀) y₁              : rfl
... = flip f y₁ (flip f y₀ x)    : rfl
... = (flip f y₁ ∘ flip f y₀) x  : rfl


We can use traverse and const to construct this composition:

calc   const.run (traverse (λ y, const.mk' (flip f y)) [y₀,y₁]) x
= const.run ((::) <$> const.mk' (flip f y₀) <*> traverse (λ y, const.mk' (flip f y)) [y₁]) x ... = const.run ((::) <$> const.mk' (flip f y₀) <*>
( (::) <$> const.mk' (flip f y₁) <*> traverse (λ y, const.mk' (flip f y)) [] )) x ... = const.run ((::) <$> const.mk' (flip f y₀) <*>
( (::) <$> const.mk' (flip f y₁) <*> pure [] )) x ... = const.run ( ((::) <$> const.mk' (flip f y₁) <*> pure []) ∘
((::) <$> const.mk' (flip f y₀)) ) x ... = const.run ( const.mk' (flip f y₁) ∘ const.mk' (flip f y₀) ) x ... = const.run ( flip f y₁ ∘ flip f y₀ ) x ... = f (f x y₀) y₁  And this is how const turns a monoid into an applicative functor and how the monoid of endofunctions define Foldl. Instances For def Monoid.Foldl.mk {α : Type u} (f : αα) : Instances For def Monoid.Foldl.get {α : Type u} (x : ) : αα Instances For @[simp] theorem Monoid.Foldl.ofFreeMonoid_apply {α : Type u} {β : Type u} (f : βαβ) (xs : ) : ↑() xs = MulOpposite.op (flip () (FreeMonoid.toList xs)) def Monoid.Foldl.ofFreeMonoid {α : Type u} {β : Type u} (f : βαβ) : Instances For @[reducible] def Monoid.Foldr (α : Type u) : Instances For def Monoid.Foldr.mk {α : Type u} (f : αα) : Instances For def Monoid.Foldr.get {α : Type u} (x : ) : αα Instances For @[simp] theorem Monoid.Foldr.ofFreeMonoid_apply {α : Type u} {β : Type u} (f : αββ) (xs : ) : ∀ (a : β), ↑() xs a = flip () (FreeMonoid.toList xs) a def Monoid.Foldr.ofFreeMonoid {α : Type u} {β : Type u} (f : αββ) : Instances For @[reducible] def Monoid.foldlM (m : Type u → Type u) [] (α : Type u) : Instances For def Monoid.foldlM.mk {m : Type u → Type u} [] {α : Type u} (f : αm α) : Instances For def Monoid.foldlM.get {m : Type u → Type u} [] {α : Type u} (x : ) : αm α Instances For @[simp] theorem Monoid.foldlM.ofFreeMonoid_apply {m : Type u → Type u} [] {α : Type u} {β : Type u} [] (f : βαm β) (xs : ) : ↑() xs = MulOpposite.op (flip () (FreeMonoid.toList xs)) def Monoid.foldlM.ofFreeMonoid {m : Type u → Type u} [] {α : Type u} {β : Type u} [] (f : βαm β) : Instances For @[reducible] def Monoid.foldrM (m : Type u → Type u) [] (α : Type u) : Instances For def Monoid.foldrM.mk {m : Type u → Type u} [] {α : Type u} (f : αm α) : Instances For def Monoid.foldrM.get {m : Type u → Type u} [] {α : Type u} (x : ) : αm α Instances For @[simp] theorem Monoid.foldrM.ofFreeMonoid_apply {m : Type u → Type u} [] {α : Type u} {β : Type u} [] (f : αβm β) (xs : ) : ∀ (a : ), ↑() xs a = flip () (FreeMonoid.toList xs) a def Monoid.foldrM.ofFreeMonoid {m : Type u → Type u} [] {α : Type u} {β : Type u} [] (f : αβm β) : Instances For def Traversable.foldMap {t : Type u → Type u} [] {α : Type u} {ω : Type u} [One ω] [Mul ω] (f : αω) : t αω Instances For def Traversable.foldl {α : Type u} {β : Type u} {t : Type u → Type u} [] (f : αβα) (x : α) (xs : t β) : α Instances For def Traversable.foldr {α : Type u} {β : Type u} {t : Type u → Type u} [] (f : αββ) (x : β) (xs : t α) : β Instances For def Traversable.toList {α : Type u} {t : Type u → Type u} [] : t αList α Conceptually, toList collects all the elements of a collection in a list. This idea is formalized by lemma toList_spec (x : t α) : toList x = foldMap FreeMonoid.mk x. The definition of toList is based on foldl and List.cons for speed. It is faster than using foldMap FreeMonoid.mk because, by using foldl and List.cons, each insertion is done in constant time. As a consequence, toList performs in linear. On the other hand, foldMap FreeMonoid.mk creates a singleton list around each element and concatenates all the resulting lists. In xs ++ ys, concatenation takes a time proportional to length xs. Since the order in which concatenation is evaluated is unspecified, nothing prevents each element of the traversable to be appended at the end xs ++ [x] which would yield a O(n²) run time. Instances For def Traversable.length {α : Type u} {t : Type u → Type u} [] (xs : t α) : Instances For def Traversable.foldlm {α : Type u} {β : Type u} {t : Type u → Type u} [] {m : Type u → Type u} [] (f : αβm α) (x : α) (xs : t β) : m α Instances For def Traversable.foldrm {α : Type u} {β : Type u} {t : Type u → Type u} [] {m : Type u → Type u} [] (f : αβm β) (x : β) (xs : t α) : m β Instances For def Traversable.mapFold {α : Type u} {β : Type u} [] [] (f : α →* β) : Instances For theorem Traversable.Free.map_eq_map {α : Type u} {β : Type u} (f : αβ) (xs : List α) : f <$> xs = FreeMonoid.toList (↑() (FreeMonoid.ofList xs))
theorem Traversable.foldl.unop_ofFreeMonoid {α : Type u} {β : Type u} (f : βαβ) (xs : ) (a : β) :
MulOpposite.unop () (↑() xs) a = List.foldl f a (FreeMonoid.toList xs)
theorem Traversable.foldMap_hom {α : Type u} {β : Type u} {γ : Type u} {t : Type u → Type u} [] [] [] (f : α →* β) (g : γα) (x : t γ) :
f () = Traversable.foldMap (f g) x
theorem Traversable.foldMap_hom_free {α : Type u} {β : Type u} {t : Type u → Type u} [] [] (f : →* β) (x : t α) :
f (Traversable.foldMap FreeMonoid.of x) = Traversable.foldMap (f FreeMonoid.of) x
@[simp]
theorem Traversable.foldl.ofFreeMonoid_comp_of {α : Type u} {β : Type u} (f : αβα) :
FreeMonoid.of = Monoid.Foldl.mk flip f
@[simp]
theorem Traversable.foldr.ofFreeMonoid_comp_of {α : Type u} {β : Type u} (f : βαα) :
FreeMonoid.of = Monoid.Foldr.mk f
@[simp]
theorem Traversable.foldlm.ofFreeMonoid_comp_of {α : Type u} {β : Type u} {m : Type u → Type u} [] [] (f : αβm α) :
FreeMonoid.of = Monoid.foldlM.mk flip f
@[simp]
theorem Traversable.foldrm.ofFreeMonoid_comp_of {α : Type u} {β : Type u} {m : Type u → Type u} [] [] (f : βαm α) :
FreeMonoid.of = Monoid.foldrM.mk f
theorem Traversable.toList_spec {α : Type u} {t : Type u → Type u} [] (xs : t α) :
= FreeMonoid.toList (Traversable.foldMap FreeMonoid.of xs)
theorem Traversable.foldMap_map {α : Type u} {β : Type u} {γ : Type u} {t : Type u → Type u} [] [] (f : αβ) (g : βγ) (xs : t α) :
theorem Traversable.foldl_toList {α : Type u} {β : Type u} {t : Type u → Type u} [] (f : αβα) (xs : t β) (x : α) :
= List.foldl f x ()
theorem Traversable.foldr_toList {α : Type u} {β : Type u} {t : Type u → Type u} [] (f : αββ) (xs : t α) (x : β) :
= List.foldr f x ()
theorem Traversable.toList_map {α : Type u} {β : Type u} {t : Type u → Type u} [] (f : αβ) (xs : t α) :
@[simp]
theorem Traversable.foldl_map {α : Type u} {β : Type u} {γ : Type u} {t : Type u → Type u} [] (g : βγ) (f : αγα) (a : α) (l : t β) :
Traversable.foldl f a (g <$> l) = Traversable.foldl (fun x y => f x (g y)) a l @[simp] theorem Traversable.foldr_map {α : Type u} {β : Type u} {γ : Type u} {t : Type u → Type u} [] (g : βγ) (f : γαα) (a : α) (l : t β) : @[simp] theorem Traversable.toList_eq_self {α : Type u} {xs : List α} : = xs theorem Traversable.length_toList {α : Type u} {t : Type u → Type u} [] {xs : t α} : theorem Traversable.foldlm_toList {α : Type u} {β : Type u} {t : Type u → Type u} [] {m : Type u → Type u} [] [] {f : αβm α} {x : α} {xs : t β} : = theorem Traversable.foldrm_toList {α : Type u} {β : Type u} {t : Type u → Type u} [] {m : Type u → Type u} [] [] (f : αβm β) (x : β) (xs : t α) : = @[simp] theorem Traversable.foldlm_map {α : Type u} {β : Type u} {γ : Type u} {t : Type u → Type u} [] {m : Type u → Type u} [] [] (g : βγ) (f : αγm α) (a : α) (l : t β) : Traversable.foldlm f a (g <$> l) = Traversable.foldlm (fun x y => f x (g y)) a l
@[simp]
theorem Traversable.foldrm_map {α : Type u} {β : Type u} {γ : Type u} {t : Type u → Type u} [] {m : Type u → Type u} [] [] (g : βγ) (f : γαm α) (a : α) (l : t β) :