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).

Answer 2

At first glance, the steps you've taken in your specific example look correct individually. However, I'd like to point out that both filter and foldr can be usefully applied to infinite lists--which should indicate that the order of your steps is incorrect as far as Haskell is concerned.

Answer 3

Just to expand on the lazy evaluation order: Basically Haskell always evaluates the function first, not looking at the arguments until it has to.

If the result of the call to myFilter is used (for example printed), the function will be evaluated in the following order:

myFilter odd [1,2,3,4]

First the myFilter function is evaluated:

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

Now foldr is the outermost function and gets evaluated:

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

Now step gets evaluated producing a 1, since 1 is odd:

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

Now the first element of the result list is available and can be used by the calling function. If the calling function also uses the following elements evaluation continues with the foldr:

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

The evaluation of step now doesn't produce any new elements, since 2 is even:

1 : foldr [] [3,4]

So foldr again:

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

Now evaluating step produces 3:

1 : 3 : foldr [] [4]

Evaluating foldr;

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

And step once more:

1 : 3 : foldr [] []

Finally foldr evaluates to an empty list:

1 : 3 : []