Could you trace how this Haskell foldl lambda function is working?

Question

myReverse :: [a] -> [a]
myReverse = foldl (\a x -> x:a) []

foldl is (a -> b -> a) -> a -> [b] -> a

The lambda function is obviously in the brackets. Where does foldl get its initial value from? And what is [b] in this case?

Answer 1

We can step through the evaluation of, say, myReverse [1,2,3]. We need the definition of foldl

foldl f z []     = z
foldl f z (x:xs) = foldl f (f z x) xs

So we have

myReverse [1,2,3,4]
-- definition of myReverse
= foldl (\a x -> x:a) [] [1,2,3]
-- definition of foldl (x:xs case)
= foldl (\a x -> x:a) ((\a x -> x:a) [] 1) [2,3]
-- beta reduction [1]
= foldl (\a x -> x:a) [1] [2,3]
-- definition of foldl
= foldl (\a x -> x:a) ((\a x -> x:a) [1] 2) [3]
-- beta reduction
= foldl (\a x -> x:a) [2,1] [3]
-- definition of foldl
= foldl (\a x -> x:a) ((\a x -> x:a) [2,1] 3) []
-- beta reduction
= foldl (\a x -> x:a) [3,2,1] []
-- definition of foldl ([] case)
= [3,2,1]

with the important caveat at [1] and for each beta reduction step that this beta reduction actually only happens when something scrutinizes the result. As foldl is progressing, the repeated applications of f build up as thunks, so what we really get (if f = \a x -> x:a) is:

foldl f [] [1,2,3]
foldl f (f [] 1) [2,3]
foldl f ((f 2 (f [] 1))) [3]
foldl f (((f 3 ((f 2 (f [] 1)))))) []
(((f 3 ((f 2 (f [] 1))))))

This is why we have foldl', which is strict in its accumulator and prevents this thunk build-up.

The initial value is []. The [b] in this case is the same as the a in foldl, which is the [a] in myReverse.