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 foldMap as a primitive and foldMap_hom as a defining property.

def foldMap {α ω} [One ω] [Mul ω] (f : α → ω) : t α → ω := ...

lemma foldMap_hom (α β)
  [Monoid α] [Monoid β] (f : α →* β)
  (g : γ → α) (x : t γ) :
  f (foldMap g x) = foldMap (f ∘ g) x :=
...

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

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

def Monoid.Foldl.mk {α : Type u} (f : α → α) : Monoid.Foldl α

def Monoid.Foldl.get {α : Type u} (x : Monoid.Foldl α) : α → α

@[simp]

theorem Monoid.Foldl.ofFreeMonoid_apply {α : Type u} {β : Type u} (f : β → α → β) (xs : FreeMonoid α) : ↑(Monoid.Foldl.ofFreeMonoid f) xs = MulOpposite.op (flip (List.foldl f) (↑FreeMonoid.toList xs))

def Monoid.Foldl.ofFreeMonoid {α : Type u} {β : Type u} (f : β → α → β) : FreeMonoid α →* Monoid.Foldl β

@[reducible]

def Monoid.Foldr (α : Type u) : Type u

def Monoid.Foldr.mk {α : Type u} (f : α → α) : Monoid.Foldr α

def Monoid.Foldr.get {α : Type u} (x : Monoid.Foldr α) : α → α

@[simp]

theorem Monoid.Foldr.ofFreeMonoid_apply {α : Type u} {β : Type u} (f : α → β → β) (xs : FreeMonoid α) : ∀ (a : β), ↑(Monoid.Foldr.ofFreeMonoid f) xs a = flip (List.foldr f) (↑FreeMonoid.toList xs) a

def Monoid.Foldr.ofFreeMonoid {α : Type u} {β : Type u} (f : α → β → β) : FreeMonoid α →* Monoid.Foldr β

@[reducible]

def Monoid.foldlM (m : Type u → Type u) [Monad m] (α : Type u) : Type u

def Monoid.foldlM.mk {m : Type u → Type u} [Monad m] {α : Type u} (f : α → m α) : Monoid.foldlM m α

def Monoid.foldlM.get {m : Type u → Type u} [Monad m] {α : Type u} (x : Monoid.foldlM m α) : α → m α

@[simp]

theorem Monoid.foldlM.ofFreeMonoid_apply {m : Type u → Type u} [Monad m] {α : Type u} {β : Type u} [LawfulMonad m] (f : β → α → m β) (xs : FreeMonoid α) : ↑(Monoid.foldlM.ofFreeMonoid f) xs = MulOpposite.op (flip (List.foldlM f) (↑FreeMonoid.toList xs))

def Monoid.foldlM.ofFreeMonoid {m : Type u → Type u} [Monad m] {α : Type u} {β : Type u} [LawfulMonad m] (f : β → α → m β) : FreeMonoid α →* Monoid.foldlM m β

@[reducible]

def Monoid.foldrM (m : Type u → Type u) [Monad m] (α : Type u) : Type u

def Monoid.foldrM.mk {m : Type u → Type u} [Monad m] {α : Type u} (f : α → m α) : Monoid.foldrM m α

def Monoid.foldrM.get {m : Type u → Type u} [Monad m] {α : Type u} (x : Monoid.foldrM m α) : α → m α

@[simp]

theorem Monoid.foldrM.ofFreeMonoid_apply {m : Type u → Type u} [Monad m] {α : Type u} {β : Type u} [LawfulMonad m] (f : α → β → m β) (xs : FreeMonoid α) : ∀ (a : CategoryTheory.KleisliCat.mk m β), ↑(Monoid.foldrM.ofFreeMonoid f) xs a = flip (List.foldrM f) (↑FreeMonoid.toList xs) a

def Monoid.foldrM.ofFreeMonoid {m : Type u → Type u} [Monad m] {α : Type u} {β : Type u} [LawfulMonad m] (f : α → β → m β) : FreeMonoid α →* Monoid.foldrM m β

def Traversable.foldMap {t : Type u → Type u} [Traversable t] {α : Type u} {ω : Type u} [One ω] [Mul ω] (f : α → ω) : t α → ω

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

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

def Traversable.toList {α : Type u} {t : Type u → Type u} [Traversable t] : t α → List α

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

lemma toList_spec (x : t α) : toList x = foldMap FreeMonoid.mk x.

The definition of toList is based on foldl and List.cons for speed. It is faster than using foldMap FreeMonoid.mk because, by using foldl and List.cons, each insertion is done in constant time. As a consequence, toList performs in linear.

On the other hand, foldMap FreeMonoid.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.

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

def Traversable.foldlm {α : Type u} {β : Type u} {t : Type u → Type u} [Traversable t] {m : Type u → Type u} [Monad m] (f : α → β → m α) (x : α) (xs : t β) : m α

def Traversable.foldrm {α : Type u} {β : Type u} {t : Type u → Type u} [Traversable t] {m : Type u → Type u} [Monad m] (f : α → β → m β) (x : β) (xs : t α) : m β

def Traversable.mapFold {α : Type u} {β : Type u} [Monoid α] [Monoid β] (f : α →* β) : ApplicativeTransformation (Functor.Const α) (Functor.Const β)

theorem Traversable.Free.map_eq_map {α : Type u} {β : Type u} (f : α → β) (xs : List α) : f <$> xs = ↑FreeMonoid.toList (↑(FreeMonoid.map f) (↑FreeMonoid.ofList xs))

theorem Traversable.foldl.unop_ofFreeMonoid {α : Type u} {β : Type u} (f : β → α → β) (xs : FreeMonoid α) (a : β) : MulOpposite.unop (CategoryTheory.End β) (↑(Monoid.Foldl.ofFreeMonoid f) xs) a = List.foldl f a (↑FreeMonoid.toList xs)

theorem Traversable.foldMap_hom {α : Type u} {β : Type u} {γ : Type u} {t : Type u → Type u} [Traversable t] [LawfulTraversable t] [Monoid α] [Monoid β] (f : α →* β) (g : γ → α) (x : t γ) : ↑f (Traversable.foldMap g x) = Traversable.foldMap (↑f ∘ g) x

theorem Traversable.foldMap_hom_free {α : Type u} {β : Type u} {t : Type u → Type u} [Traversable t] [LawfulTraversable t] [Monoid β] (f : FreeMonoid α →* β) (x : t α) : ↑f (Traversable.foldMap FreeMonoid.of x) = Traversable.foldMap (↑f ∘ FreeMonoid.of) x

@[simp]

theorem Traversable.foldl.ofFreeMonoid_comp_of {α : Type u} {β : Type u} (f : α → β → α) : ↑(Monoid.Foldl.ofFreeMonoid f) ∘ FreeMonoid.of = Monoid.Foldl.mk ∘ flip f

@[simp]

theorem Traversable.foldr.ofFreeMonoid_comp_of {α : Type u} {β : Type u} (f : β → α → α) : ↑(Monoid.Foldr.ofFreeMonoid f) ∘ FreeMonoid.of = Monoid.Foldr.mk ∘ f

@[simp]

theorem Traversable.foldlm.ofFreeMonoid_comp_of {α : Type u} {β : Type u} {m : Type u → Type u} [Monad m] [LawfulMonad m] (f : α → β → m α) : ↑(Monoid.foldlM.ofFreeMonoid f) ∘ FreeMonoid.of = Monoid.foldlM.mk ∘ flip f

@[simp]

theorem Traversable.foldrm.ofFreeMonoid_comp_of {α : Type u} {β : Type u} {m : Type u → Type u} [Monad m] [LawfulMonad m] (f : β → α → m α) : ↑(Monoid.foldrM.ofFreeMonoid f) ∘ FreeMonoid.of = Monoid.foldrM.mk ∘ f

theorem Traversable.toList_spec {α : Type u} {t : Type u → Type u} [Traversable t] [LawfulTraversable t] (xs : t α) : Traversable.toList xs = ↑FreeMonoid.toList (Traversable.foldMap FreeMonoid.of xs)

theorem Traversable.foldMap_map {α : Type u} {β : Type u} {γ : Type u} {t : Type u → Type u} [Traversable t] [LawfulTraversable t] [Monoid γ] (f : α → β) (g : β → γ) (xs : t α) : Traversable.foldMap g (f <$> xs) = Traversable.foldMap (g ∘ f) xs

theorem Traversable.foldl_toList {α : Type u} {β : Type u} {t : Type u → Type u} [Traversable t] [LawfulTraversable t] (f : α → β → α) (xs : t β) (x : α) : Traversable.foldl f x xs = List.foldl f x (Traversable.toList xs)

theorem Traversable.foldr_toList {α : Type u} {β : Type u} {t : Type u → Type u} [Traversable t] [LawfulTraversable t] (f : α → β → β) (xs : t α) (x : β) : Traversable.foldr f x xs = List.foldr f x (Traversable.toList xs)

theorem Traversable.toList_map {α : Type u} {β : Type u} {t : Type u → Type u} [Traversable t] [LawfulTraversable t] (f : α → β) (xs : t α) : Traversable.toList (f <$> xs) = f <$> Traversable.toList xs

@[simp]

theorem Traversable.foldl_map {α : Type u} {β : Type u} {γ : Type u} {t : Type u → Type u} [Traversable t] [LawfulTraversable t] (g : β → γ) (f : α → γ → α) (a : α) (l : t β) : Traversable.foldl f a (g <$> l) = Traversable.foldl (fun x y => f x (g y)) a l

@[simp]

theorem Traversable.foldr_map {α : Type u} {β : Type u} {γ : Type u} {t : Type u → Type u} [Traversable t] [LawfulTraversable t] (g : β → γ) (f : γ → α → α) (a : α) (l : t β) : Traversable.foldr f a (g <$> l) = Traversable.foldr (f ∘ g) a l

@[simp]

theorem Traversable.toList_eq_self {α : Type u} {xs : List α} : Traversable.toList xs = xs

theorem Traversable.length_toList {α : Type u} {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {xs : t α} : Traversable.length xs = List.length (Traversable.toList xs)

theorem Traversable.foldlm_toList {α : Type u} {β : Type u} {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {m : Type u → Type u} [Monad m] [LawfulMonad m] {f : α → β → m α} {x : α} {xs : t β} : Traversable.foldlm f x xs = List.foldlM f x (Traversable.toList xs)

theorem Traversable.foldrm_toList {α : Type u} {β : Type u} {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {m : Type u → Type u} [Monad m] [LawfulMonad m] (f : α → β → m β) (x : β) (xs : t α) : Traversable.foldrm f x xs = List.foldrM f x (Traversable.toList xs)

@[simp]

theorem Traversable.foldlm_map {α : Type u} {β : Type u} {γ : Type u} {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {m : Type u → Type u} [Monad m] [LawfulMonad m] (g : β → γ) (f : α → γ → m α) (a : α) (l : t β) : Traversable.foldlm f a (g <$> l) = Traversable.foldlm (fun x y => f x (g y)) a l

@[simp]

theorem Traversable.foldrm_map {α : Type u} {β : Type u} {γ : Type u} {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {m : Type u → Type u} [Monad m] [LawfulMonad m] (g : β → γ) (f : γ → α → m α) (a : α) (l : t β) : Traversable.foldrm f a (g <$> l) = Traversable.foldrm (f ∘ g) a l