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 def monoid.foldl.mk {α : Type u} (f : α → α) : Equations def monoid.foldl.get {α : Type u} (x : monoid.foldl α) : α → α Equations def monoid.foldl.of_free_monoid {α β : Type u} (f : β → α → β) (xs : free_monoid α) : Equations def monoid.foldr (α : Type u) : Type u Equations def monoid.foldr.mk {α : Type u} (f : α → α) : Equations def monoid.foldr.get {α : Type u} (x : monoid.foldr α) : α → α Equations def monoid.foldr.of_free_monoid {α β : Type u} (f : α → β → β) (xs : free_monoid α) : Equations def monoid.mfoldl (m : Type uType u) [monad m] (α : Type u) : Type u Equations def monoid.mfoldl.mk {m : Type uType u} [monad m] {α : Type u} (f : α → m α) : Equations def monoid.mfoldl.get {m : Type uType u} [monad m] {α : Type u} (x : α) : α → m α Equations def monoid.mfoldl.of_free_monoid {m : Type uType u} [monad m] {α β : Type u} (f : β → α → m β) (xs : free_monoid α) : Equations def monoid.mfoldr (m : Type uType u) [monad m] (α : Type u) : Type u Equations def monoid.mfoldr.mk {m : Type uType u} [monad m] {α : Type u} (f : α → m α) : Equations def monoid.mfoldr.get {m : Type uType u} [monad m] {α : Type u} (x : α) : α → m α Equations def monoid.mfoldr.of_free_monoid {m : Type uType u} [monad m] {α β : Type u} (f : α → β → m β) (xs : free_monoid α) : Equations def traversable.fold_map {t : Type uType u} [traversable t] {α ω : Type u} [has_one «ω»] [has_mul «ω»] (f : α → «ω») : t α → «ω» Equations def traversable.foldl {α β : Type u} {t : Type uType u} [traversable t] (f : α → β → α) (x : α) (xs : t β) : α Equations def traversable.foldr {α β : Type u} {t : Type uType u} [traversable t] (f : α → β → β) (x : β) (xs : 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] (xs : t α) : Equations def traversable.mfoldl {α β : Type u} {t : Type uType u} [traversable t] {m : Type uType u} [monad m] (f : α → β → m α) (x : α) (xs : t β) : m α Equations def traversable.mfoldr {α β : Type u} {t : Type uType u} [traversable t] {m : Type uType u} [monad m] (f : α → β → m β) (x : β) (xs : t α) : m β Equations def traversable.map_fold {α β : Type u} [monoid α] [monoid β] {f : α → β} (hf : is_monoid_hom f) : Equations def traversable.free.mk {α : Type u} : α → Equations def traversable.free.map {α β : Type u} (f : α → β) : Equations theorem traversable.free.map_eq_map {α β : Type u} (f : α → β) (xs : list α) : f <$> xs =
theorem traversable.free.map.is_monoid_hom {α β : Type u} (f : α → β) :
theorem traversable.fold_foldl {α β : Type u} (f : β → α → β) :
theorem traversable.foldl.unop_of_free_monoid {α β : Type u} (f : β → α → β) (xs : free_monoid α) (a : β) :
= a xs
theorem traversable.fold_foldr {α β : Type u} (f : α → β → β) :
@[simp]
theorem traversable.mfoldl.unop_of_free_monoid {α β : Type u} (m : Type uType u) [monad m] (f : β → α → m β) (xs : free_monoid α) (a : β) :
= a xs
theorem traversable.fold_mfoldl {α β : Type u} (m : Type uType u) [monad m] (f : β → α → m β) :
theorem traversable.fold_mfoldr {α β : Type u} (m : Type uType u) [monad m] (f : α → β → m β) :
theorem traversable.fold_map_hom {α β γ : Type u} {t : Type uType u} [traversable t] [monoid α] [monoid β] {f : α → β} (hf : is_monoid_hom f) (g : γ → α) (x : t γ) :
theorem traversable.fold_map_hom_free {α β : Type u} {t : Type uType u} [traversable t] [monoid β] {f : → β} (hf : is_monoid_hom f) (x : t α) :
theorem traversable.fold_mfoldl_cons {α β : Type u} {m : Type uType u} [monad m] (f : α → β → m α) (x : β) (y : α) :
y = f y x
theorem traversable.fold_mfoldr_cons {α β : Type u} {m : Type uType u} [monad m] (f : β → α → m α) (x : β) (y : α) :
y = f x y
@[simp]
theorem traversable.foldl.of_free_monoid_comp_free_mk {α β : Type u} (f : α → β → α) :
@[simp]
theorem traversable.foldr.of_free_monoid_comp_free_mk {α β : Type u} (f : β → α → α) :
@[simp]
theorem traversable.mfoldl.of_free_monoid_comp_free_mk {α β : Type u} {m : Type uType u} [monad m] (f : α → β → m α) :
@[simp]
theorem traversable.mfoldr.of_free_monoid_comp_free_mk {α β : Type u} {m : Type uType u} [monad m] (f : β → α → m α) :
theorem traversable.to_list_spec {α : Type u} {t : Type uType u} [traversable t] (xs : t α) :
theorem traversable.fold_map_map {α β γ : Type u} {t : Type uType u} [traversable t] [monoid γ] (f : α → β) (g : β → γ) (xs : t α) :
(f <$> xs) = traversable.fold_map (g f) xs theorem traversable.foldl_to_list {α β : Type u} {t : Type uType u} [traversable t] (f : α → β → α) (xs : t β) (x : α) : xs = x theorem traversable.foldr_to_list {α β : Type u} {t : Type uType u} [traversable t] (f : α → β → β) (xs : t α) (x : β) : xs = x theorem traversable.to_list_map {α β : Type u} {t : Type uType u} [traversable t] (f : α → β) (xs : t α) : @[simp] theorem traversable.foldl_map {α β γ : Type u} {t : Type uType u} [traversable t] (g : β → γ) (f : α → γ → α) (a : α) (l : t β) : (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] (g : β → γ) (f : γ → α → α) (a : α) (l : t β) :
(g <$> l) = traversable.foldr (f g) a l @[simp] theorem traversable.to_list_eq_self {α : Type u} {xs : list α} : = xs theorem traversable.length_to_list {α : Type u} {t : Type uType u} [traversable t] {xs : t α} : theorem traversable.mfoldl_to_list {α β : Type u} {t : Type uType u} [traversable t] {m : Type uType u} [monad m] {f : α → β → m α} {x : α} {xs : t β} : xs = x theorem traversable.mfoldr_to_list {α β : Type u} {t : Type uType u} [traversable t] {m : Type uType u} [monad m] (f : α → β → m β) (x : β) (xs : t α) : xs = x @[simp] theorem traversable.mfoldl_map {α β γ : Type u} {t : Type uType u} [traversable t] {m : Type uType u} [monad m] (g : β → γ) (f : α → γ → m α) (a : α) (l : t β) : (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] {m : Type uType u} [monad m] (g : β → γ) (f : γ → α → m α) (a : α) (l : t β) :
(g <\$> l) = traversable.mfoldr (f g) a l