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.
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
Equations
Equations
- x.get = opposite.unop x
Equations
- monoid.foldl.of_free_monoid f xs = opposite.op (flip (list.foldl f) xs)
Equations
- monoid.foldr.mk f = f
Equations
- monoid.foldr.of_free_monoid f xs = flip (list.foldr f) xs
Equations
Equations
Equations
- x.get = opposite.unop x
Equations
- monoid.mfoldl.of_free_monoid f xs = opposite.op (flip (list.mfoldl f) xs)
Equations
Equations
- monoid.mfoldr.mk f = f
Equations
- monoid.mfoldr.of_free_monoid f xs = flip (list.mfoldr f) xs
Equations
Equations
- traversable.foldl f x xs = (traversable.fold_map (monoid.foldl.mk ∘ flip f) xs).get x
Equations
- traversable.foldr f x xs = (traversable.fold_map (monoid.foldr.mk ∘ f) xs).get x
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
Equations
- traversable.length xs = (traversable.foldl (λ (l : ulift ℕ) (_x : α), {down := l.down + 1}) {down := 0} xs).down
Equations
- traversable.mfoldl f x xs = (traversable.fold_map (monoid.mfoldl.mk ∘ flip f) xs).get x
Equations
- traversable.mfoldr f x xs = (traversable.fold_map (monoid.mfoldr.mk ∘ f) xs).get x
Equations
- traversable.map_fold f = {app := λ (x : Type u_1), f, preserves_pure' := _, preserves_seq' := _}
Equations
Equations
Equations
- _ = _
Equations
- _ = _
Equations
- _ = _