Why would using head/tail instead of pattern matching make evaluation terminate?

Question

As an exercise, I'm trying to define a ruler value

ruler :: (Num a, Enum a) => [a]

which corresponds to the ruler function

0,1,0,2,0,1,0,3,0,1,0,2,0,1,0,4,0,1,0,2...

where the n'th element of the list (assuming the first element corresponds to n=1) is the largest power of 2 which evenly divides n. To make it more interesting, I'm trying to implement ruler without having to do any divisibility testing.

Using a helper function

interleave :: [a] -> [a] -> [a]

which simply alternates the elements from the two given lists, I came up with this - but alas it doesn't work:

interleave :: [a] -> [a] -> [a]
interleave  (x:xs) (y:ys) = x : y : interleave xs ys
interleave  _      _      = []

ruler :: (Num a, Enum a) => [a]
ruler = foldr1 interleave . map repeat $ [0..]

main :: IO ()
main = print (take 20 ruler)

The program eventually uses up all stack space.

Now, what's strange is that the program works just fine if I adjust the definition of interleave so that it reads

interleave (x:xs) ys = x : head ys : interleave xs (tail ys)

I.e. I no longer use pattern matching on the second argument. Why does using head and tail here make ruler terminate - after all, the pattern matching is rather defensive (I only evaluate the first element of the list spine, no?).

Answer 1

The difference is that pattern matching forces the first item in the spine, head/tail do not.

You could use lazy patterns to achieve the same goal:

interleave  (x:xs) ~(y:ys) = x : y : interleave xs ys

Note the ~: this is equivalent to defining y and ys using head and tail.

For example: the list below is undefined.

fix (\ (x:xs) -> 1:x:xs)

where fix is the fixed point combinator (e.g. from Data.Function). By comparison, this other list repeats 1 forever:

fix (\ ~(x:xs) -> 1:x:xs)

This is because the 1 is produced before the list is split between x and xs.

---

Why forcing the first item in the spine triggers the problem?

When reasoning about a recursive equation such as

x = f x

it often helps to regard x as the value "approached" by the sequence of values

undefined
f undefined
f (f undefined)
f (f (f undefined))
...

(The above intuition can be made precise through a bit of denotational semantics and the Kleene's fixed point theorem.)

For instance, the equation

x = 1 : x

defines the "limit" of the sequence

undefined
1 : undefined
1 : 1 : undefined
...

which clearly converges to the repeated ones list.

When using pattern matching to define recursive values, the equation becomes, e.g.

(y:ys) = 1:y:ys

which, due to pattern matching, translates to

x = case x of (y:ys) -> 1:y:ys

Let us consider its approximating sequence

undefined
case undefined of (y:ys) -> ....   = undefined
case undefined of (y:ys) -> ....   = undefined
...

At the second step, the case diverges, making the result still undefined. The sequence does not approach the intended "repeated ones" list, but is constantly undefined.

Using lazy patterns, instead

x = case x of ~(y:ys) -> 1:y:ys

we obtain the sequence

undefined
case undefined of ~(y:ys) -> 1:y:ys 
    = 1 : (case undefined of (y:_) -> y) : (case undefined of (_:ys) -> ys)
    = 1 : undefined : undefined      -- name this L1
case L1 of ~(y:ys) -> 1:y:ys
    = 1 : (case L1 of (y:_) -> y) : (case L1 of (_:ys) -> ys)
    = 1 : 1 : undefined : undefined  -- name this L2
case L2 of ~(y:ys) -> 1:y:ys
    = 1 : (case L2 of (y:_) -> y) : (case L2 of (_:ys) -> ys)
    = 1 : 1 : 1 : undefined : undefined

which does converge to the intended list. Note how lazy patterns are "pushed forward" without evaluating the case argument early. This is what makes them lazy. In this way, the 1 is produced before the pattern matching is performed, making the result of the recursively defined entity non trivial.

Answer 2

The problem here is not so much about the pattern matching or using head and tail. The issue is how it's done, by defining your function as

interleave :: [a] -> [a] -> [a]
interleave  (x:xs) (y:ys) = x : y : interleave xs ys
interleave  _      _      = []

You're strictly pattern matching your arguments, that is, we need to know that they are lists of at least one element before we can choose the first branch. Since you're folding this function over an infinite list of lists, we can't really figure this out, and we run out of stack space.

To expand on this (to clarify things brought up in the comments), the first time we try to evaluate interleave (in ruler), we'd get something like

interleave (repeat 0) (foldr1 interleave (map repeat [1..]))

The first argument here of course matches the pattern, but to figure out if the second argument does, we have to try to evaluate it, so we get to

interleave (repeat 1) (foldr1 interleave (map repeat [2..]))

Now we can't evaluate this unless we know more about the second argument. Since the list [2..] never ends, this process can go on forever.

One solution to this is to do a lazy pattern binding on the second argument:

interleave  (x:xs) ~(y:ys) = x : y : interleave xs ys

This acts like a promise that the second argument does match the pattern, so don't worry about it (of course this will fail if that isn't true). This means that that first evaluation of interleave can go on without looking deeper into the repeated fold, which in a domino-like effect solves the issue.

A sidenote is that your this version of interleave (as well as your head/tail version) will only work on lists where the second list is as long as or longer than the first.

Answer 3

You are applying foldr with an strict combination function to an infinite list.

Boiled down to a minimal example, you can view this behaviour here:

*Main> :t const
const :: a -> b -> a
*Main> :t flip seq
flip seq :: c -> a -> c
*Main> foldr1 const [0..]
0
*Main> foldr1 (flip seq) [0..]
^CInterrupted.

The fix is, as explained in other answers, to make interleave lazy.

More concretely, here is what happens. First we resolve the foldr1, replacing every : of the outer list with interleave:

foldr1 interleave [[0..], [1...], ...]
= interleave [0...] (interleave [1...] (...))

In order to make progress, the first interleave wants to evaluate the second argument before producing the first value. But then the second wants to evaluate its second argument, and so on.

With the lazy definition of interleave, the first value is produced before evaluating the second argument. In particular, interleave [1...] (...) will evaluate to 1 : ... (which helps the first interleave to make progress) before evaluating stuff further down.