How is co-recursion handled?

Question

Ok basically I have a problem knowing whether option 1 or 2 applies in the following case:

naturals = 0 : map (+ 1) naturals

Where options are:
1. The execution is awful, everything is recomputed at each step:

naturals     = [0]
naturals'    = 0:map (+ 1) [0]          // == [0, 1]
naturals''   = 0:map (+ 1) [0, 1]       // == [0, 1, 2]
naturals'''  = 0:map (+ 1) [0, 1, 2]    // == [0, 1, 2, 3]
naturals'''' = 0:map (+ 1) [0, 1, 2, 3] // == [0, 1, 2, 3, 4]

2. The execution is not awful, the list is always infinite and map is applied once only

naturals     = 0:something
                                  |
naturals'    = 0:      map (+ 1) (0:      something)
                                    |
naturals''   = 0:1:    map (+ 1) (0:1:    something')
                                      |
naturals'''  = 0:1:2:  map (+ 1) (0:1:2:  something'')
                                        |
naturals'''' = 0:1:2:3:map (+ 1) (0:1:2:3:something''')

with | indicating where map is at in its execution.

I do know that answers may be only 1 or 2 but I'd appreciate some pointers to good explanations on co-recursion too to clear the last doubts :)

Answer 1

Execution isn't going to be, as you put it, "awful". :) Lazy evaluation is your best friend here. What does laziness mean?

1. Things are not evaluated before their results are really needed;
2. Things are evaluated at most once.

"Things", here, are "not-yet-evaluated expressions", also known as "thunks".

Here is what happens:

You define

naturals = 0 : map (+1) naturals

Merely defining naturals doesn't introduce a need to evaluate it, so initially naturals will just point to a thunk for the unevaluated expression 0 : map (+1) naturals:

naturals = <thunk0>

At some point, your program may pattern match on naturals. (Pattern matching is essentially the only thing that forces evaluation in a Haskell program.) That is, your program needs to know whether naturals is the empty list or a head element followed by a tail list. This is where the right-hand side of your definition will be evaluated, but only as far as needed to find out whether naturals is constructed by [] or (:):

naturals = 0 : <thunk1>

That is naturals will now point to an application of the constructor (:) on the head element 0 and a thunk for the still-unevaluated tail. (Actually, the head element will also be still-unevaluated, so really naturals will point to something of the form <thunk> : <thunk>, but I will be leaving that detail out.)

It is not until some later point in your program where you may pattern match on the tail that the thunk for the tail gets "forced", i.e., evaluated. This means that the expression map (+1) naturals is to be evaluated. Evaluating this expression reduces to map pattern matching on naturals: it needs to know whether naturals is constructed by [] or (:). We saw that, at this point, rather than pointing to a thunk, naturals is already pointing to an application of (:), so this pattern match by map requires no further evaluation. The application of map does immediately see enough of naturals to figure out that it needs to produce an application of (:) itself and so it does: map produces 1 : <thunk2> where the thunk contains an unevaluated expression of the form map (+1) <?>. (Again, instead of 1, we actually have a thunk for 0 + 1.) What is <?> pointing to? Well, the tail of naturals, which happens to be what map was producing. Hence, we now have

naturals = 0 : 1 : <thunk2>

with <thunk2> containing the yet-unevaluated expression map (+1) (1 : <thunk2>).

At yet a later point in your program, pattern matching may force <thunk2>, so that we get

naturals = 0 : 1 : 2 : <thunk3>

with <thunk3> containing the yet-unevaluated expression map (+1) (2 : <thunk3>). And so forth.