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.

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.