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 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

monoid.foldl α = (category_theory.End α)ᵒᵖ

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

monoid.foldl α

Equations

monoid.foldl.mk f = opposite.op f

def monoid.foldl.get {α : Type u} (x : monoid.foldl α) (a : α) :

α

Equations

x.get = opposite.unop x

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

monoid.foldl β

Equations

monoid.foldl.of_free_monoid f xs = opposite.op (flip (list.foldl f) xs)

def monoid.foldr (α : Type u) :

Type u

Equations

monoid.foldr α = category_theory.End α

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

monoid.foldr α

Equations

monoid.foldr.mk f = f

def monoid.foldr.get {α : Type u} (x : monoid.foldr α) (a : α) :

α

Equations

x.get = x

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

monoid.foldr β

Equations

monoid.foldr.of_free_monoid f xs = flip (list.foldr f) xs

def monoid.mfoldl (m : Type u → Type u) [monad m] (α : Type u) :

Type u

Equations

monoid.mfoldl m α = (category_theory.End (category_theory.Kleisli.mk m α))ᵒᵖ

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

monoid.mfoldl m α

Equations

monoid.mfoldl.mk f = opposite.op f

def monoid.mfoldl.get {m : Type u → Type u} [monad m] {α : Type u} (x : monoid.mfoldl m α) (a : α) :

m α

Equations

x.get = opposite.unop x

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

monoid.mfoldl m β

Equations

monoid.mfoldl.of_free_monoid f xs = opposite.op (flip (mfoldl f) xs)

def monoid.mfoldr (m : Type u → Type u) [monad m] (α : Type u) :

Type u

Equations

monoid.mfoldr m α = category_theory.End (category_theory.Kleisli.mk m α)

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

monoid.mfoldr m α

Equations

monoid.mfoldr.mk f = f

def monoid.mfoldr.get {m : Type u → Type u} [monad m] {α : Type u} (x : monoid.mfoldr m α) (a : α) :

m α

Equations

x.get = x

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

monoid.mfoldr m β

Equations

monoid.mfoldr.of_free_monoid f xs = flip (list.mfoldr f) xs

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

«ω»

Equations

traversable.fold_map f = traverse (functor.const.mk' ∘ f)

def traversable.foldl {α β : Type u} {t : Type u → Type u} [traversable t] (f : α → β → α) (x : α) (xs : t β) :

α

Equations

traversable.foldl f x xs = (traversable.fold_map (monoid.foldl.mk ∘ flip f) xs).get x

def traversable.foldr {α β : Type u} {t : Type u → Type u} [traversable t] (f : α → β → β) (x : β) (xs : t α) :

β

Equations

traversable.foldr f x xs = (traversable.fold_map (monoid.foldr.mk ∘ f) xs).get x

def traversable.to_list {α : Type u} {t : Type u → Type u} [traversable t] (a : t α) :

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

traversable.to_list = list.reverse ∘ traversable.foldl (flip list.cons) list.nil

def traversable.length {α : Type u} {t : Type u → Type u} [traversable t] (xs : t α) :

Equations

traversable.length xs = (traversable.foldl (λ (l : ulift ℕ) (_x : α), {down := l.down + 1}) {down := 0} xs).down

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

traversable.mfoldl f x xs = (traversable.fold_map (monoid.mfoldl.mk ∘ flip f) xs).get x

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

traversable.mfoldr f x xs = (traversable.fold_map (monoid.mfoldr.mk ∘ f) xs).get x

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

applicative_transformation (functor.const α) (functor.const β)

Equations

traversable.map_fold f = {app := λ (x : Type u_1), f, preserves_pure' := _, preserves_seq' := _}

def traversable.free.mk {α : Type u} (a : α) :

Equations

traversable.free.mk = list.ret

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

Equations

traversable.free.map f = list.map f

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

f <$> xs = traversable.free.map f xs

@[instance]

def traversable.is_monoid_hom {α β : Type u} (f : α → β) :

is_monoid_hom (traversable.free.map f)

@[instance]

def traversable.fold_foldl {α β : Type u} (f : β → α → β) :

is_monoid_hom (monoid.foldl.of_free_monoid f)

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

opposite.unop (monoid.foldl.of_free_monoid f xs) a = list.foldl f a xs

@[instance]

def traversable.fold_foldr {α β : Type u} (f : α → β → β) :

is_monoid_hom (monoid.foldr.of_free_monoid f)

@[simp]

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

opposite.unop (monoid.mfoldl.of_free_monoid f xs) a = mfoldl f a xs

@[instance]

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

is_monoid_hom (monoid.mfoldl.of_free_monoid f)

@[instance]

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

is_monoid_hom (monoid.mfoldr.of_free_monoid f)

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

f (traversable.fold_map g x) = traversable.fold_map (f ∘ g) x

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

f (traversable.fold_map traversable.free.mk x) = traversable.fold_map (f ∘ traversable.free.mk) x

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

mfoldl f y (traversable.free.mk x) = f y x

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

list.mfoldr f y (traversable.free.mk x) = f x y

@[simp]

theorem traversable.foldl.of_free_monoid_comp_free_mk {α β : Type u} (f : α → β → α) :

monoid.foldl.of_free_monoid f ∘ traversable.free.mk = monoid.foldl.mk ∘ flip f

@[simp]

theorem traversable.foldr.of_free_monoid_comp_free_mk {α β : Type u} (f : β → α → α) :

monoid.foldr.of_free_monoid f ∘ traversable.free.mk = monoid.foldr.mk ∘ f

@[simp]

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

monoid.mfoldl.of_free_monoid f ∘ traversable.free.mk = monoid.mfoldl.mk ∘ flip f

@[simp]

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

monoid.mfoldr.of_free_monoid f ∘ traversable.free.mk = monoid.mfoldr.mk ∘ f

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

traversable.to_list xs = traversable.fold_map traversable.free.mk xs

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

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)

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)

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

@[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 β) :

traversable.foldr f a (g <$> l) = traversable.foldr (f ∘ g) a l

@[simp]

theorem traversable.to_list_eq_self {α : Type u} {xs : list α} :

traversable.to_list xs = xs

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

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 = mfoldl f x (traversable.to_list xs)

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)

@[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 β) :

traversable.mfoldr f a (g <$> l) = traversable.mfoldr (f ∘ g) a l