Traversable.foldMap_hom_free
theorem Traversable.foldMap_hom_free :
∀ {α β : Type u} {t : Type u → Type u} [inst : Traversable t] [inst_1 : LawfulTraversable t] [inst_2 : Monoid β]
(f : FreeMonoid α →* β) (x : t α),
f (Traversable.foldMap FreeMonoid.of x) = Traversable.foldMap (⇑f ∘ FreeMonoid.of) x
The theorem `Traversable.foldMap_hom_free` states that for any types `α` and `β`, and a type `t` that is an instance of `Traversable`, if `t` is also `LawfulTraversable` and `β` is a `Monoid`, and `f` is a Monoid homomorphism from `FreeMonoid α` to `β`, and `x` is of type `t α`, then applying `f` to the result of `Traversable.foldMap` of `FreeMonoid.of` and `x` is equivalent to applying `Traversable.foldMap` to the composition of `f` and `FreeMonoid.of` and `x`. Here, `Traversable.foldMap` is a function that combines all data in a traversable structure by using a supplied function, and `FreeMonoid.of` is a function that converts an element to a free monoid over its type.
In simpler terms, this theorem shows a relationship between the folding and mapping operations in a free monoid and a monoid, which says that you can either first map and then fold, or first fold and then map, and the result will be the same. This is a property of monoids and how they interact with traversable structures.
More concisely: For any `Traversable t`, `Monoid β`, `LawfulTraversable t`, Monoid homomorphism `f` from `FreeMonoid α` to `β`, and `x` of type `t α`, `Traversable.foldMap (f . FreeMonoid.of) x = Traversable.foldMap (FreeMonoid.of) x . f`.
|
Traversable.toList_spec
theorem Traversable.toList_spec :
∀ {α : Type u} {t : Type u → Type u} [inst : Traversable t] [inst_1 : LawfulTraversable t] (xs : t α),
Traversable.toList xs = FreeMonoid.toList (Traversable.foldMap FreeMonoid.of xs)
The theorem `Traversable.toList_spec` states that for any type `α`, any traversable type constructor `t`, any instance `inst` of `t` being traversable, any lawful traversable `inst_1` of `t`, and any `xs` of type `t α`, the operation of converting `xs` to a list using `Traversable.toList` is equivalent to first applying `FreeMonoid.of` to each element of `xs` using `Traversable.foldMap`, converting the resulting `FreeMonoid α` to a list, and then applying `FreeMonoid.toList`. In short, it establishes the equivalence between two different ways of converting a traversable structure into a list.
More concisely: For any traversable type constructor `t`, any instance `inst` of `t` being traversable, any lawful traversable `inst_1` of `t`, and any `xs` of type `t α`, `Traversable.toList xs` is equivalent to `FreeMonoid.toList (Traversable.foldMap (FreeMonoid.of) xs)`.
|
Traversable.foldMap_map
theorem Traversable.foldMap_map :
∀ {α β γ : Type u} {t : Type u → Type u} [inst : Traversable t] [inst_1 : LawfulTraversable t] [inst_2 : Monoid γ]
(f : α → β) (g : β → γ) (xs : t α), Traversable.foldMap g (f <$> xs) = Traversable.foldMap (g ∘ f) xs
The theorem `Traversable.foldMap_map` states that for any types `α`, `β`, and `γ`, and any traversable structure `t` of type `Type u → Type u`, if we have a lawful traversable instance for `t` and a monoid structure for `γ`, then for any functions `f : α → β` and `g : β → γ`, and any traversable structure `xs` of type `t α`, applying `f` to `xs` (denoted as `f <$> xs`), then folding with function `g` (i.e., `Traversable.foldMap g (f <$> xs)`) is the same as folding with the composition of `g` and `f` (i.e., `Traversable.foldMap (g ∘ f) xs`). In other words, the theorem expresses a kind of distributivity of the `foldMap` operation over the function application, which is a fundamental property in the area of functional programming and type theory.
More concisely: For any traversable type `t`, monoid `γ`, and functions `f : α → β` and `g : β → γ`, given lawful traversable instances for `t` and `γ`, `Traversable.foldMap (g ∘ f) xs` equals `Traversable.foldMap g (f <$> xs)` for any traversable structure `xs` of type `t α`.
|