Search code examples
haskellfunctional-programmingfoldidrisdependent-type

Idris `foldl` default implementation


interface Foldable t where
  foldr : (func : elem -> acc -> acc) -> (init : acc) -> (input : t elem) -> acc
  foldl : (func : acc -> elem -> acc) -> (init : acc) -> (input : t elem) -> acc
  foldl f z t = foldr (flip (.) . flip f) id t z

What does foldr (flip (.) . flip f) id t z mean here?
And is there another way to implement foldl using foldr?
Thanks for answering.


Solution

  • The first argument in the foldl defined above could be turned into a lambda like this:

    \element -> (. (flip f element))
    -- or
    \element prevFun -> prevFun . flip f element
    -- or
    \element prevFun next -> prevFun $ f next element
    

    Let's take an example where you want to fold left over a list [a, b, c]. You want your end result to be f (f (f z a) b) c), where z is the accumulator.

    In the first iteration, the first argument would be c and the second id. Thus, the result would be id . flip f c, or just flip f c (since id . f is simply f, as @chepner pointed out).

    The second iteration would result in flip f c . flip f b, and after that you would get flip f c . flip f b . flip f a (basically, adding a . flip f x for every next element x.

    This expands to:

    acc -> flip f c (flip f b (flip f a acc))
    -- or
    acc -> flip f c (flip f b (f acc a))
    -- or
    acc -> f (f (f acc a) b) c)
    

    Et voila! We have a function that takes an accumulator acc, and returns the result of foldl f acc t, so we simply apply that to z, the actual accumulator.