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.

Distillate

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

Stavros

thanks for that. well, i'm very newbie in haskell, so i don't know all the "backstage" of haskell. i just needed to know if it's simply like this. maybe in later chapters of the book, they will discuss about what you tried to teach me here (which i need to read more, to understand it) thanks a lot :-). – Distillate

I think you're on the right track. I wouldn't call this the "back end" so much as understanding how lazy evaluation works. For a simple case like this it doesn't matter, but when you come to see that foldr works on infinite lists and foldl doesn't, this will help you understand why. – Stavros

Answer 2

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 step [] [2,3,4])

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

1 : foldr step [] [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 step [] [3,4])

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

1 : foldr step [] [3,4]

So foldr again:

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

Now evaluating step produces 3:

1 : 3 : foldr step [] [4]

Evaluating foldr;

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

And step once more:

1 : 3 : foldr step [] []

Finally foldr evaluates to an empty list:

1 : 3 : []

Bastien

so what you say is that the recursion is realy not a recursion? in your evaluation, everything is computed from the beginning to the end, and in the end, it's just give me the list. what i understand, is that there is realy a recursion that at first go from start to the end of the input list, and after that, everything is computed from the inner step to the outer one. i hope that it also will be explained in the book, in future reading :). thank you :-) – Distillate

Answer 3

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.

Exuviae

thanks for that. i think that my comment to Dan, is also (sort of) for you. :-). – Distillate