List folds generalized to
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
fold_map_hom as a defining property.
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
to_list permits the
formulation of specifications in terms of operations on lists.
Each fold function can be defined using a specialized
to_list uses a free monoid represented as a list with
foldl uses endofunctions together with function
The definition through monoids uses
traverse together with the
const m (where
m is the monoid). As an
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
For a list, foldl f x [y₀,y₁] reduces as follows:
f : α → β → α x : α [y₀,y₁] : list β
We can view the above as a composition of functions:
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
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
speed. It is faster than using
fold_map free_monoid.mk because, by
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.