mathlib3 documentation

control.fold

List folds generalized to traversable #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : α →* β)
  (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.

@[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.

Equations
def monoid.foldl.mk {α : Type u} (f : α α) :
Equations
def monoid.foldl.get {α : Type u} (x : monoid.foldl α) :
α α
Equations
@[reducible]
def monoid.foldr (α : Type u) :
Equations
def monoid.foldr.mk {α : Type u} (f : α α) :
Equations
def monoid.foldr.get {α : Type u} (x : monoid.foldr α) :
α α
Equations
@[simp]
theorem monoid.foldr.of_free_monoid_apply {α β : Type u} (f : α β β) (xs : free_monoid α) (ᾰ : β) :
@[reducible]
def monoid.mfoldl (m : Type u Type u) [monad m] (α : Type u) :
Equations
def monoid.mfoldl.mk {m : Type u Type u} [monad m] {α : Type u} (f : α m α) :
Equations
def monoid.mfoldl.get {m : Type u Type u} [monad m] {α : Type u} (x : monoid.mfoldl m α) :
α m α
Equations
@[reducible]
def monoid.mfoldr (m : Type u Type u) [monad m] (α : Type u) :
Equations
def monoid.mfoldr.mk {m : Type u Type u} [monad m] {α : Type u} (f : α m α) :
Equations
def monoid.mfoldr.get {m : Type u Type u} [monad m] {α : Type u} (x : monoid.mfoldr m α) :
α m α
Equations
@[simp]
theorem monoid.mfoldr.of_free_monoid_apply {m : Type u Type u} [monad m] {α β : Type u} [is_lawful_monad m] (f : α β m β) (xs : free_monoid α) (ᾰ : category_theory.Kleisli.mk m β) :
def monoid.mfoldr.of_free_monoid {m : Type u Type u} [monad m] {α β : Type u} [is_lawful_monad m] (f : α β m β) :
Equations
def traversable.fold_map {t : Type u Type u} [traversable t] {α ω : Type u} [has_one ω] [has_mul ω] (f : α ω) :
t α ω
Equations
def traversable.foldl {α β : Type u} {t : Type u Type u} [traversable t] (f : α β α) (x : α) (xs : t β) :
α
Equations
def traversable.foldr {α β : Type u} {t : Type u Type u} [traversable t] (f : α β β) (x : β) (xs : t α) :
β
Equations
def traversable.to_list {α : Type u} {t : Type u Type 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 u Type u} [traversable t] (xs : t α) :
Equations
def traversable.mfoldl {α β : Type u} {t : Type u Type u} [traversable t] {m : Type u Type u} [monad m] (f : α β m α) (x : α) (xs : t β) :
m α
Equations
def traversable.mfoldr {α β : Type u} {t : Type u Type u} [traversable t] {m : Type u Type u} [monad m] (f : α β m β) (x : β) (xs : t α) :
m β
Equations
Equations
theorem traversable.fold_map_hom {α β γ : Type u} {t : Type u Type u} [traversable t] [is_lawful_traversable t] [monoid α] [monoid β] (f : α →* β) (g : γ α) (x : t γ) :
theorem traversable.fold_map_map {α β γ : Type u} {t : Type u Type u} [traversable t] [is_lawful_traversable t] [monoid γ] (f : α β) (g : β γ) (xs : t α) :
theorem traversable.foldl_to_list {α β : Type u} {t : Type u Type u} [traversable t] [is_lawful_traversable t] (f : α β α) (xs : t β) (x : α) :
theorem traversable.foldr_to_list {α β : Type u} {t : Type u Type u} [traversable t] [is_lawful_traversable t] (f : α β β) (xs : t α) (x : β) :
theorem traversable.to_list_map {α β : Type u} {t : Type u Type u} [traversable t] [is_lawful_traversable t] (f : α β) (xs : t α) :
@[simp]
theorem traversable.foldl_map {α β γ : Type u} {t : Type u Type 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 u Type 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.mfoldl_to_list {α β : Type u} {t : Type u Type u} [traversable t] [is_lawful_traversable t] {m : Type u Type u} [monad m] [is_lawful_monad m] {f : α β m α} {x : α} {xs : t β} :
theorem traversable.mfoldr_to_list {α β : Type u} {t : Type u Type u} [traversable t] [is_lawful_traversable t] {m : Type u Type u} [monad m] [is_lawful_monad m] (f : α β m β) (x : β) (xs : t α) :
@[simp]
theorem traversable.mfoldl_map {α β γ : Type u} {t : Type u Type u} [traversable t] [is_lawful_traversable t] {m : Type u Type 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 u Type u} [traversable t] [is_lawful_traversable t] {m : Type u Type u} [monad m] [is_lawful_monad m] (g : β γ) (f : γ α m α) (a : α) (l : t β) :