mathlib documentation

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 fold_map as a primitive and fold_map_hom as a defining property.

def fold_map {α ω} [has_one ω] [has_mul ω] (f : α  ω) : t α  ω := ...

lemma fold_map_hom (α β)
  [monoid α] [monoid β] (f : α  β) [is_monoid_hom f]
  (g : γ  α) (x : t γ) :
  f (fold_map g x) = fold_map (f  g) x :=
...

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

Each fold function can be defined using a specialized monoid. to_list 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.

def monoid.foldl  :
Type uType 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.

Equations
def monoid.foldl.mk {α : Type u} :
(α → α)monoid.foldl α

Equations
def monoid.foldl.get {α : Type u} :
monoid.foldl αα → α

Equations
def monoid.foldl.of_free_monoid {α β : Type u} :
(β → α → β)free_monoid αmonoid.foldl β

Equations
def monoid.foldr  :
Type uType u

Equations
def monoid.foldr.mk {α : Type u} :
(α → α)monoid.foldr α

Equations
def monoid.foldr.get {α : Type u} :
monoid.foldr αα → α

Equations
def monoid.foldr.of_free_monoid {α β : Type u} :
(α → β → β)free_monoid αmonoid.foldr β

Equations
def monoid.mfoldl (m : Type uType u) [monad m] :
Type uType u

Equations
def monoid.mfoldl.mk {m : Type uType u} [monad m] {α : Type u} :
(α → m α)monoid.mfoldl m α

Equations
def monoid.mfoldl.get {m : Type uType u} [monad m] {α : Type u} :
monoid.mfoldl m αα → m α

Equations
def monoid.mfoldl.of_free_monoid {m : Type uType u} [monad m] {α β : Type u} :
(β → α → m β)free_monoid αmonoid.mfoldl m β

Equations
def monoid.mfoldr (m : Type uType u) [monad m] :
Type uType u

Equations
def monoid.mfoldr.mk {m : Type uType u} [monad m] {α : Type u} :
(α → m α)monoid.mfoldr m α

Equations
def monoid.mfoldr.get {m : Type uType u} [monad m] {α : Type u} :
monoid.mfoldr m αα → m α

Equations
def monoid.mfoldr.of_free_monoid {m : Type uType u} [monad m] {α β : Type u} :
(α → β → m β)free_monoid αmonoid.mfoldr m β

Equations
def traversable.fold_map {t : Type uType u} [traversable t] {α ω : Type u} [has_one «ω»] [has_mul «ω»] :
(α → «ω»)t α → «ω»

Equations
def traversable.foldl {α β : Type u} {t : Type uType u} [traversable t] :
(α → β → α)α → t β → α

Equations
def traversable.foldr {α β : Type u} {t : Type uType u} [traversable t] :
(α → β → β)β → t α → β

Equations
def traversable.to_list {α : Type u} {t : Type uType u} [traversable t] :
t αlist α

Conceptually, to_list collects all the elements of a collection in a list. This idea is formalized by

lemma to_list_spec (x : t α) : to_list x = fold_map free_monoid.mk x.

The definition of to_list is based on foldl and list.cons for speed. It is faster than using fold_map free_monoid.mk because, by using foldl and list.cons, each insertion is done in constant time. As a consequence, to_list performs in linear.

On the other hand, fold_map free_monoid.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.

Equations
def traversable.length {α : Type u} {t : Type uType u} [traversable t] :
t α

Equations
def traversable.mfoldl {α β : Type u} {t : Type uType u} [traversable t] {m : Type uType u} [monad m] :
(α → β → m α)α → t βm α

Equations
def traversable.mfoldr {α β : Type u} {t : Type uType u} [traversable t] {m : Type uType u} [monad m] :
(α → β → m β)β → t αm β

Equations
def traversable.map_fold {α β : Type u} [monoid α] [monoid β] (f : α → β) [is_monoid_hom f] :

Equations
def traversable.free.mk {α : Type u} :
α → free_monoid α

Equations
def traversable.free.map {α β : Type u} :
(α → β)free_monoid αfree_monoid β

Equations
theorem traversable.free.map_eq_map {α β : Type u} (f : α → β) (xs : list α) :

@[instance]
def traversable.is_monoid_hom {α β : Type u} (f : α → β) :

@[instance]
def traversable.fold_foldl {α β : Type u} (f : β → α → β) :

theorem traversable.foldl.unop_of_free_monoid {α β : Type u} (f : β → α → β) (xs : free_monoid α) (a : β) :

@[instance]
def traversable.fold_foldr {α β : Type u} (f : α → β → β) :

@[simp]
theorem traversable.mfoldl.unop_of_free_monoid {α β : Type u} (m : Type uType u) [monad m] [is_lawful_monad m] (f : β → α → m β) (xs : free_monoid α) (a : β) :

@[instance]
def traversable.fold_mfoldl {α β : Type u} (m : Type uType u) [monad m] [is_lawful_monad m] (f : β → α → m β) :

@[instance]
def traversable.fold_mfoldr {α β : Type u} (m : Type uType u) [monad m] [is_lawful_monad m] (f : α → β → m β) :

theorem traversable.fold_map_hom {α β γ : Type u} {t : Type uType u} [traversable t] [is_lawful_traversable t] [monoid α] [monoid β] (f : α → β) [is_monoid_hom f] (g : γ → α) (x : t γ) :

theorem traversable.fold_map_hom_free {α β : Type u} {t : Type uType u} [traversable t] [is_lawful_traversable t] [monoid β] (f : free_monoid α → β) [is_monoid_hom f] (x : t α) :

theorem traversable.fold_mfoldl_cons {α β : Type u} {m : Type uType u} [monad m] [is_lawful_monad m] (f : α → β → m α) (x : β) (y : α) :

theorem traversable.fold_mfoldr_cons {α β : Type u} {m : Type uType u} [monad m] [is_lawful_monad m] (f : β → α → m α) (x : β) (y : α) :

@[simp]
theorem traversable.mfoldl.of_free_monoid_comp_free_mk {α β : Type u} {m : Type uType u} [monad m] [is_lawful_monad m] (f : α → β → m α) :

@[simp]
theorem traversable.mfoldr.of_free_monoid_comp_free_mk {α β : Type u} {m : Type uType u} [monad m] [is_lawful_monad m] (f : β → α → m α) :

theorem traversable.to_list_spec {α : Type u} {t : Type uType u} [traversable t] [is_lawful_traversable t] (xs : t α) :

theorem traversable.fold_map_map {α β γ : Type u} {t : Type uType u} [traversable t] [is_lawful_traversable t] [monoid γ] (f : α → β) (g : β → γ) (xs : t α) :

theorem traversable.foldl_to_list {α β : Type u} {t : Type uType u} [traversable t] [is_lawful_traversable t] (f : α → β → α) (xs : t β) (x : α) :

theorem traversable.foldr_to_list {α β : Type u} {t : Type uType u} [traversable t] [is_lawful_traversable t] (f : α → β → β) (xs : t α) (x : β) :

theorem traversable.to_list_map {α β : Type u} {t : Type uType u} [traversable t] [is_lawful_traversable t] (f : α → β) (xs : t α) :

@[simp]
theorem traversable.foldl_map {α β γ : Type u} {t : Type uType u} [traversable t] [is_lawful_traversable t] (g : β → γ) (f : α → γ → α) (a : α) (l : t β) :
traversable.foldl f a (g <$> l) = traversable.foldl (λ (x : α) (y : β), f x (g y)) a l

@[simp]
theorem traversable.foldr_map {α β γ : Type u} {t : Type uType u} [traversable t] [is_lawful_traversable t] (g : β → γ) (f : γ → α → α) (a : α) (l : t β) :

@[simp]
theorem traversable.to_list_eq_self {α : Type u} {xs : list α} :

theorem traversable.length_to_list {α : Type u} {t : Type uType u} [traversable t] [is_lawful_traversable t] {xs : t α} :

theorem traversable.mfoldl_to_list {α β : Type u} {t : Type uType u} [traversable t] [is_lawful_traversable t] {m : Type uType u} [monad m] [is_lawful_monad m] {f : α → β → m α} {x : α} {xs : t β} :

theorem traversable.mfoldr_to_list {α β : Type u} {t : Type uType u} [traversable t] [is_lawful_traversable t] {m : Type uType u} [monad m] [is_lawful_monad m] (f : α → β → m β) (x : β) (xs : t α) :

@[simp]
theorem traversable.mfoldl_map {α β γ : Type u} {t : Type uType u} [traversable t] [is_lawful_traversable t] {m : Type uType u} [monad m] [is_lawful_monad m] (g : β → γ) (f : α → γ → m α) (a : α) (l : t β) :
traversable.mfoldl f a (g <$> l) = traversable.mfoldl (λ (x : α) (y : β), f x (g y)) a l

@[simp]
theorem traversable.mfoldr_map {α β γ : Type u} {t : Type uType u} [traversable t] [is_lawful_traversable t] {m : Type uType u} [monad m] [is_lawful_monad m] (g : β → γ) (f : γ → α → m α) (a : α) (l : t β) :