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

Accepted Answer

Execution isn't going to be, as you put it, "awful". :) Lazy evaluation is your best friend here. What does laziness mean? - Things are not evaluated before their results are really needed; - 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 = ``` 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 : ``` 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 ` : `, 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 : ` 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 : ``` with `` containing the yet-unevaluated expression `map (+1) (1 : )`. At yet a later point in your program, pattern matching may force ``, so that we get ``` naturals = 0 : 1 : 2 : ``` with `` containing the yet-unevaluated expression `map (+1) (2 : )`. And so forth.

How is co-recursion handled?

Solution

Problem