Documentation

Mathlib.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 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, inline]
abbrev 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 (fun y ↦ const.mk' (flip f y)) [y₀,y₁]) x
     = const.run ((::) <$> const.mk' (flip f y₀) <*>
         traverse (fun y ↦ const.mk' (flip f y)) [y₁]) x
...  = const.run ((::) <$> const.mk' (flip f y₀) <*>
         ( (::) <$> const.mk' (flip f y₁) <*> traverse (fun 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
Instances For
    def Monoid.Foldl.mk {α : Type u} (f : αα) :
    Equations
    Instances For
      def Monoid.Foldl.get {α : Type u} (x : Monoid.Foldl α) :
      αα
      Equations
      Instances For
        @[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 : βαβ) :
        Equations
        Instances For
          @[reducible, inline]
          abbrev Monoid.Foldr (α : Type u) :
          Equations
          Instances For
            def Monoid.Foldr.mk {α : Type u} (f : αα) :
            Equations
            Instances For
              def Monoid.Foldr.get {α : Type u} (x : Monoid.Foldr α) :
              αα
              Equations
              • x.get = x
              Instances For
                @[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 : αββ) :
                Equations
                Instances For
                  @[reducible, inline]
                  abbrev Monoid.foldlM (m : Type u → Type u) [Monad m] (α : Type u) :
                  Equations
                  Instances For
                    def Monoid.foldlM.mk {m : Type u → Type u} [Monad m] {α : Type u} (f : αm α) :
                    Equations
                    Instances For
                      def Monoid.foldlM.get {m : Type u → Type u} [Monad m] {α : Type u} (x : Monoid.foldlM m α) :
                      αm α
                      Equations
                      Instances For
                        @[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 β) :
                        Equations
                        Instances For
                          @[reducible, inline]
                          abbrev Monoid.foldrM (m : Type u → Type u) [Monad m] (α : Type u) :
                          Equations
                          Instances For
                            def Monoid.foldrM.mk {m : Type u → Type u} [Monad m] {α : Type u} (f : αm α) :
                            Equations
                            Instances For
                              def Monoid.foldrM.get {m : Type u → Type u} [Monad m] {α : Type u} (x : Monoid.foldrM m α) :
                              αm α
                              Equations
                              • x.get = x
                              Instances For
                                @[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 β) :
                                Equations
                                Instances For
                                  def Traversable.foldMap {t : Type u → Type u} [Traversable t] {α : Type u} {ω : Type u} [One ω] [Mul ω] (f : αω) :
                                  t αω
                                  Equations
                                  Instances For
                                    def Traversable.foldl {α : Type u} {β : Type u} {t : Type u → Type u} [Traversable t] (f : αβα) (x : α) (xs : t β) :
                                    α
                                    Equations
                                    Instances For
                                      def Traversable.foldr {α : Type u} {β : Type u} {t : Type u → Type u} [Traversable t] (f : αββ) (x : β) (xs : t α) :
                                      β
                                      Equations
                                      Instances For
                                        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.

                                        Equations
                                        Instances For
                                          def Traversable.length {α : Type u} {t : Type u → Type u} [Traversable t] (xs : t α) :
                                          Equations
                                          Instances For
                                            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 α
                                            Equations
                                            Instances For
                                              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 β
                                              Equations
                                              Instances For
                                                def Traversable.mapFold {α : Type u} {β : Type u} [Monoid α] [Monoid β] (f : α →* β) :
                                                Equations
                                                Instances For
                                                  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 ((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 γ) :
                                                  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 α) :
                                                  theorem Traversable.foldl_toList {α : Type u} {β : Type u} {t : Type u → Type u} [Traversable t] [LawfulTraversable t] (f : αβα) (xs : t β) (x : α) :
                                                  theorem Traversable.foldr_toList {α : Type u} {β : Type u} {t : Type u → Type u} [Traversable t] [LawfulTraversable t] (f : αββ) (xs : t α) (x : β) :
                                                  theorem Traversable.toList_map {α : Type u} {β : Type u} {t : Type u → Type u} [Traversable t] [LawfulTraversable t] (f : αβ) (xs : t α) :
                                                  @[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 β) :
                                                  @[simp]
                                                  theorem Traversable.toList_eq_self {α : Type u} {xs : List α} :
                                                  theorem Traversable.length_toList {α : Type u} {t : Type u → Type u} [Traversable t] [LawfulTraversable t] {xs : t α} :
                                                  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 β} :
                                                  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 α) :
                                                  @[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 β) :