Why right folding can process infinite list in Haskell?

Question

For an infinite list, there's no "last" element of it. So how could foldr work with it?

I've this code snippet from the Haskell book:

(&&)::Bool->Bool->Bool
True && x = x
False && _ = False

and' :: [Bool]->Bool
and' xs=foldr (Main.&&) True xs

Then in Prelude load this hs file and run:

*Main> and' (repeat False)
False

It works as expected, but I don't understand:

The definition of the (&&) receives boolean on the left of it, but we apply True && x = x while the variable x is in its right side. Isn't it strange?
Why foldr stops when (&&) returns False? In my understanding foldr will loop through the list from tail till head. Is there any internal "break" mechanism?
foldr starts from the last element of a list, but infinite list has no end. How does foldr begin to work?

Possible duplicate of [Left and Right Folding over an Infinite list](http://stackoverflow.com/questions/7396978/left-and-right-folding-over-an-infinite-list) — zakyggaps, Feb 19 '16 at 05:59
Or this one: https://stackoverflow.com/questions/833186/why-does-this-haskell-code-work-successfully-with-infinite-lists?rq=1. Either way, ___one question per post___. Your first one is different from your second and third. The second and third are duplicates of others. Also, `foldr` does not start from the right; it associates to the right: `f a (f b (f c( ... ))))`. Clean up your question. — Zeta, Feb 19 '16 at 06:01

score 2 · Answer 1 · answered Feb 19 '16 at 07:04

2

You need to familiarize with the syntax a bit. In Haskell, a function definition goes like this:

 this   =   that

and, basically, it means: When you see this it means that. In fact

True && x

is the same as x, and

False && x

is False, that is why we can write the definitions as in your example.

For your second question: it is not the case that foldr "stops". It is the && operator who does not evaluate its right operand, when the left one is False.

For your 3rd question: no, foldr does not start from the last element of a list. Please have a look at the definition of foldr:

foldr f z [] = z
foldr f z (x:xs) = x `f`  foldr f z xs

Now suppose

foldr (&&) True (False:xs)

it evaluates to

False && foldr (&&) True xs

And since

False && _

is False, the result is False

answered Feb 19 '16 at 07:04

Ingo

36,037
5
53
100

Shouldn't "foldr f z [] = z" be "foldr f z [] = f z"? I suppose f should be applied? – vik santata Feb 19 '16 at 08:15
And what does `f` mean? – vik santata Feb 19 '16 at 08:16
Infix application of **f** (you should really go at least through LYAH, as it is near impossible to discuss things when most basic syntax is not known). This also means that f is a function with two arguments, so no, it would not make sense to apply it to z in the first equation. – Ingo Feb 19 '16 at 09:46

Luis Casillas · Accepted Answer · 2016-02-20T00:29:15.803

Let's repeat your definitions and add a couple more:

(&&)::Bool->Bool->Bool
True && x = x
False && _ = False

and :: [Bool]->Bool
and xs = foldr (&&) True xs

repeat :: a -> [a]
repeat a = a : repeat a

foldr :: (a -> r -> r) -> r -> [a] -> r
foldr _ z [] = z
foldr f z (a:as) = f a (foldr f z as)

Now, we can prove this by evaluating it manually, taking care to do it "lazily" (outermost applications first, and evaluating only enough to resolve the outermost data constructors):

and (repeat False)
  = foldr (&&) True (repeat False)           -- definition of `and`
  = foldr (&&) True (False : repeat False)   -- definition of `repeat`
  = False && foldr (&&) True (repeat False)  -- `foldr`, second equation
  = False                                    -- `&&`, second equation

The key is that the second equation of the definition of && discards its second argument:

False && _ = False

This means, in runtime terms, that we never force foldr's recursive call at a step where we encounter False.

Another way to look at it is to contemplate foldr's second equation, and what it means when we have lazy evaluation:

foldr f z (a:as) = f a (foldr f z as)

Since the recursive call to foldr happens as an argument to f, this means that, at runtime, the function f decides whether the value of its second argument is necessary or not, and so chooses at each step of the fold whether to recurse down the list or not. And this "decision" process proceeds from left to right.

In my understanding foldr will loop through the list from tail till head. Is there any internal "break" mechanism?

Strictly speaking, in a pure functional language there is no intrinsic notion of evaluation order. Expressions may be evaluated in any order that's consistent with their data dependencies.

What you've said here is a common misunderstanding that people who've learned foldr from impure, eager languages carry over to Haskell. In an eager language that's a useful rule of thumb, but in Haskell, with purity lazy evaluation, that rule will only confuse you. Often the opposite rule of thumb is useful when programming Haskell: foldr will visit the list elements from left to right, and at each step its f argument function gets to decide whether the rest of the list is necessary.

The extreme example of this is to implement a function to get the head of a list using foldr:

-- | Return `Just` the first element of the list, or `Nothing` if the
-- list is empty.
safeHead :: [a] -> Maybe a
safeHead = foldr (\a _ -> Just a) Nothing

So for example:

safeHead [1..]
  = foldr (\a _ -> Just a) Nothing [1..]
  = foldr (\a _ -> Just a) Nothing (1:[2..])
  = (\a _ -> Just a) 1 (foldr (\a _ -> Just a) Nothing [2..])
  = Just 1

Why right folding can process infinite list in Haskell?

2 Answers2