Am I using sound equational reasoning about a definition of filter in terms of foldr?

Question

well, this is the definition of the filter function using foldr:

myFilter p xs = foldr step [] xs
    where step x ys | p x       = x : ys
                    | otherwise = ys

so for example let's say i have this function:

myFilter odd [1,2,3,4]

so it will be:

foldr step [] [1,2,3,4]

and this will be

step 1 (foldr step [] [2,3,4])

and this will be

step 1 (step 2 (foldr step [] [3,4]))

and this will be

step 1 (step 2 (step 3 (foldr step [] [4])))

and this will be

step 1 (step 2 (step 3 (step 4 (foldr step [] []))))

and foldr step [] [] is [] so:

step 1 (step 2 (step 3 (step 4 [])))

now we will actually get into the step function.
here is the definition of step inside the myFilter function, from above:

step x ys | p x       = x : ys
          | otherwise = ys

also, i remind you that p is actually the odd function in our example.

well, again, we are here:

step 1 (step 2 (step 3 (step 4 [])))

and

x = 4 in the most inner step, and 4 isn't odd, so we returning ys, which is []

so now we get this:

step 1 (step 2 (step 3 []))

now, in the most inner step, x = 3, and 3 is odd, so we return x:ys, which is 3 : [], which is [3], and now we get:

step 1 (step 2 [3])

and now, in the inner step, x = 2, and 2 isn't odd, so we return ys, which is [3], so now we will get:

step 1 [3]

and now, x = 1, and 1 is odd, so we return x : ys, which is 1 : [3], which is [1,3].

The End :-).

am i right in all my moves?
thanks a lot :-).

p.s. the definition of myFilter is from the book Real World Haskell, in chapter 4.

Answer 1

This looks right to me on first read.

The important thing to remember though is that in order to achieve lazy evaluation, Haskell will actually look at things the other way. In other words, the real sequence is more like

step 1 (step 2 (step 3 (step 4 [])))

becomes

step 1 <block1>

which becomes

[1, <block1>]

then if you try to pull the next element from that list, it will evaluate

[1, step 2 <block2>]

which becomes

[1, <block2>]

and then trying to evaluate

[1, step 3 (step 4 [])]

turns into

[1, step 3 <block3>]

which becomes

[1, 3, <block3>]

etc. This took me a while to understand. It was counterintuitive to me that since foldr seems to be evaluated from the "inside out" but foldl is evaluated from the "outside in" that foldr would be lazy (which it is), whereas foldl is strict. But if you think of it the way I outlined above, it makes sense (to me, anyway).