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.

source
@[reducible]
def monoid.foldl (α : Type u) :
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
source
def monoid.foldl.mk {α : Type u} (f : α → α) :
monoid.foldl α
Equations
source
def monoid.foldl.get {α : Type u} (x : monoid.foldl α) :
α → α
Equations
source
@[simp]
theorem monoid.foldl.of_free_monoid_apply {α β : Type u} (f : β → α → β) (xs : free_monoid α) :
⇑(monoid.foldl.of_free_monoid f) xs = mul_opposite.op (flip (list.foldl f) (⇑free_monoid.to_list xs))
source
def monoid.foldl.of_free_monoid {α β : Type u} (f : β → α → β) :
free_monoid α →* monoid.foldl β
Equations
source
@[reducible]
def monoid.foldr (α : Type u) :
Type u
Equations
source
def monoid.foldr.mk {α : Type u} (f : α → α) :
monoid.foldr α
Equations
source
def monoid.foldr.get {α : Type u} (x : monoid.foldr α) :
α → α
Equations
source
def monoid.foldr.of_free_monoid {α β : Type u} (f : α → β → β) :
free_monoid α →* monoid.foldr β
Equations
source
@[simp]
theorem monoid.foldr.of_free_monoid_apply {α β : Type u} (f : α → β → β) (xs : free_monoid α) (ᾰ : β) :
⇑(monoid.foldr.of_free_monoid f) xs ᾰ = flip (list.foldr f) (⇑free_monoid.to_list xs) ᾰ
source
@[reducible]
def monoid.mfoldl (m : Type u → Type u) [monad m] (α : Type u) :
Type u
Equations
source
def monoid.mfoldl.mk {m : Type u → Type u} [monad m] {α : Type u} (f : α → m α) :
monoid.mfoldl m α
Equations
source
def monoid.mfoldl.get {m : Type u → Type u} [monad m] {α : Type u} (x : monoid.mfoldl m α) :
α → m α
Equations
source
def monoid.mfoldl.of_free_monoid {m : Type u → Type u} [monad m] {α β : Type u} [is_lawful_monad m] (f : β → α → m β) :
free_monoid α →* monoid.mfoldl m β
Equations
source
@[simp]
theorem monoid.mfoldl.of_free_monoid_apply {m : Type u → Type u} [monad m] {α β : Type u} [is_lawful_monad m] (f : β → α → m β) (xs : free_monoid α) :
⇑(monoid.mfoldl.of_free_monoid f) xs = mul_opposite.op (flip (list.mfoldl f) (⇑free_monoid.to_list xs))
source
@[reducible]
def monoid.mfoldr (m : Type u → Type u) [monad m] (α : Type u) :
Type u
Equations
source
def monoid.mfoldr.mk {m : Type u → Type u} [monad m] {α : Type u} (f : α → m α) :
monoid.mfoldr m α
Equations
source
def monoid.mfoldr.get {m : Type u → Type u} [monad m] {α : Type u} (x : monoid.mfoldr m α) :
α → m α
Equations
source
@[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 β) :
⇑(monoid.mfoldr.of_free_monoid f) xs ᾰ = flip (list.mfoldr f) (⇑free_monoid.to_list xs) ᾰ
source
def monoid.mfoldr.of_free_monoid {m : Type u → Type u} [monad m] {α β : Type u} [is_lawful_monad m] (f : α → β → m β) :
free_monoid α →* monoid.mfoldr m β
Equations
source
def traversable.fold_map {t : Type u → Type u} [traversable t] {α ω : Type u} [has_one ω] [has_mul ω] (f : α → ω) :
t α → ω
Equations
source
def traversable.foldl {α β : Type u} {t : Type u → Type u} [traversable t] (f : α → β → α) (x : α) (xs : t β) :
α
Equations
source
def traversable.foldr {α β : Type u} {t : Type u → Type u} [traversable t] (f : α → β → β) (x : β) (xs : t α) :
β
Equations
source
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
source
def traversable.length {α : Type u} {t : Type u → Type u} [traversable t] (xs : t α) :
ℕ
Equations
source
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
source
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
source
def traversable.map_fold {α β : Type u} [monoid α] [monoid β] (f : α →* β) :
applicative_transformation (functor.const α) (functor.const β)
Equations
source
theorem traversable.free.map_eq_map {α β : Type u} (f : α → β) (xs : list α) :
f <$> xs = ⇑free_monoid.to_list (⇑(free_monoid.map f) (⇑free_monoid.of_list xs))
source
theorem traversable.foldl.unop_of_free_monoid {α β : Type u} (f : β → α → β) (xs : free_monoid α) (a : β) :
mul_opposite.unop (⇑(monoid.foldl.of_free_monoid f) xs) a = list.foldl f a (⇑free_monoid.to_list xs)
source
theorem traversable.fold_map_hom {α β γ : Type u} {t : Type u → Type u} [traversable t] [is_lawful_traversable t] [monoid α] [monoid β] (f : α →* β) (g : γ → α) (x : t γ) :
⇑f (traversable.fold_map g x) = traversable.fold_map (⇑f ∘ g) x
source
theorem traversable.fold_map_hom_free {α β : Type u} {t : Type u → Type u} [traversable t] [is_lawful_traversable t] [monoid β] (f : free_monoid α →* β) (x : t α) :
⇑f (traversable.fold_map free_monoid.of x) = traversable.fold_map (⇑f ∘ free_monoid.of) x
source
@[simp]
theorem traversable.foldl.of_free_monoid_comp_of {α β : Type u} (f : α → β → α) :
⇑(monoid.foldl.of_free_monoid f) ∘ free_monoid.of = monoid.foldl.mk ∘ flip f
source
@[simp]
theorem traversable.foldr.of_free_monoid_comp_of {α β : Type u} (f : β → α → α) :
⇑(monoid.foldr.of_free_monoid f) ∘ free_monoid.of = monoid.foldr.mk ∘ f
source
@[simp]
theorem traversable.mfoldl.of_free_monoid_comp_of {α β : Type u} {m : Type u → Type u} [monad m] [is_lawful_monad m] (f : α → β → m α) :
⇑(monoid.mfoldl.of_free_monoid f) ∘ free_monoid.of = monoid.mfoldl.mk ∘ flip f
source
@[simp]
theorem traversable.mfoldr.of_free_monoid_comp_of {α β : Type u} {m : Type u → Type u} [monad m] [is_lawful_monad m] (f : β → α → m α) :
⇑(monoid.mfoldr.of_free_monoid f) ∘ free_monoid.of = monoid.mfoldr.mk ∘ f
source
theorem traversable.to_list_spec {α : Type u} {t : Type u → Type u} [traversable t] [is_lawful_traversable t] (xs : t α) :
traversable.to_list xs = ⇑free_monoid.to_list (traversable.fold_map free_monoid.of xs)
source
theorem traversable.fold_map_map {α β γ : Type u} {t : Type u → Type u} [traversable t] [is_lawful_traversable t] [monoid γ] (f : α → β) (g : β → γ) (xs : t α) :
traversable.fold_map g (f <$> xs) = traversable.fold_map (g ∘ f) xs
source
theorem traversable.foldl_to_list {α β : Type u} {t : Type u → Type u} [traversable t] [is_lawful_traversable t] (f : α → β → α) (xs : t β) (x : α) :
traversable.foldl f x xs = list.foldl f x (traversable.to_list xs)
source
theorem traversable.foldr_to_list {α β : Type u} {t : Type u → Type u} [traversable t] [is_lawful_traversable t] (f : α → β → β) (xs : t α) (x : β) :
traversable.foldr f x xs = list.foldr f x (traversable.to_list xs)
source
theorem traversable.to_list_map {α β : Type u} {t : Type u → Type u} [traversable t] [is_lawful_traversable t] (f : α → β) (xs : t α) :
traversable.to_list (f <$> xs) = f <$> traversable.to_list xs
source
@[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
source
@[simp]
theorem traversable.foldr_map {α β γ : Type u} {t : Type u → Type u} [traversable t] [is_lawful_traversable t] (g : β → γ) (f : γ → α → α) (a : α) (l : t β) :
traversable.foldr f a (g <$> l) = traversable.foldr (f ∘ g) a l
source
@[simp]
theorem traversable.to_list_eq_self {α : Type u} {xs : list α} :
traversable.to_list xs = xs
source
theorem traversable.length_to_list {α : Type u} {t : Type u → Type u} [traversable t] [is_lawful_traversable t] {xs : t α} :
traversable.length xs = (traversable.to_list xs).length
source
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 β} :
traversable.mfoldl f x xs = list.mfoldl f x (traversable.to_list xs)
source
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 α) :
traversable.mfoldr f x xs = list.mfoldr f x (traversable.to_list xs)
source
@[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
source
@[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 β) :
traversable.mfoldr f a (g <$> l) = traversable.mfoldr (f ∘ g) a l