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
.
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
.
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
Instances For
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.