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 : α →* β)
(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:
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 = mul_opposite.unop x
Equations
- monoid.foldl.of_free_monoid f = {to_fun := λ (xs : free_monoid α), mul_opposite.op (flip (list.foldl f) xs), map_one' := _, map_mul' := _}
Equations
Equations
- monoid.foldr.mk f = f
Equations
- monoid.foldr.of_free_monoid f = {to_fun := λ (xs : free_monoid α), flip (list.foldr f) xs, map_one' := _, map_mul' := _}
Equations
Equations
Equations
- x.get = mul_opposite.unop x
Equations
- monoid.mfoldl.of_free_monoid f = {to_fun := λ (xs : free_monoid α), mul_opposite.op (flip (list.mfoldl f) xs), map_one' := _, map_mul' := _}
Equations
Equations
- monoid.mfoldr.mk f = f
Equations
- monoid.mfoldr.of_free_monoid f = {to_fun := λ (xs : free_monoid α), flip (list.mfoldr f) xs, map_one' := _, map_mul' := _}
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' := _}