Search code examples
haskellfoldproof

Why it is not possible to redefine (implement) foldr in terms of foldl


We have that foldl can be implemented in terms of foldr. This is explained in detail in A tutorial on the universality and expressiveness of fold. In the paper it is stated that:

In contrast, it is not possible to redefine fold in terms of foldl , due to the fact that foldl is strict in the tail of its list argument but fold is not.

However I fail to see how this constitutes a proof on the impossibility of defining foldr in terms of foldl (note that in the original paper fold is a synonym for foldr). I'm quite puzzled trying to understand how strictness plays a role here. Can somebody expand on this explanation?


Solution

  • In what follows, I will refer to fold as foldr (since that is what its is called in the Haskell standard libraries).


    Taking another look at the definition of foldl,

    foldl :: (β -> α -> β) -> β -> [α] -> β
    foldl f v [] = v
    foldl f v (x:xs) = foldl f (f v x) xs
    

    note that the base case requires the list argument to be [] - in all other cases the list is evaluated to WNHF and we recurse immediately using the tail of the list. That establishes the fact that foldl is strict in its (last) list argument.

    Now, we can write a version of foldr using foldl, but it will only work on lists of finite length. See this page for the motivation.

    foldr' :: (α -> β -> β) -> β -> [α] -> β
    foldr' f v xs = foldl (\g u x -> g (f u x)) id xs v 
    

    To see the problem, let's try to write a version of head which is total1 using a right fold.

    import Control.Applicative ((<|>))
    
    safeHead :: [α] -> Maybe α
    safeHead = foldr (\x y -> Just x <|> y) Nothing
    

    If we replace foldr with our foldl-based foldr', we are no longer able to find the head of an infinite list safeHead [1..]. Even if safeHead only needs to look at the first element of the list, the underlying foldl will try to traverse the whole infinite list.


    1 Such a function actually already exists in the Prelude, it is called listToMaybe