corecursion and codata

Question

Would like to get step-by-step explanation of the following function in Haskell

fibs = 0 : 1 : zipWith (+) fibs (tail fibs)

I understand that the "fibs" in general is "lazy", so next item would be calculated "on demand", however I'm not sure how the "tail" function would work on infinite list.

So the illustration of how it works with some intermediate data would help.

Answer 1

At the beginning, the evalution is like this:

fibs = 0 : 1 : zipWith (+) fibs (tail fibs)

If we replace fibs by its evaluation, it looks like this:

fibs = 0 : 1 : zipWith (+) (0 : 1 : ?) (1 : ?)

Where ? denotes the unevaluated thunk. Let's evaluate the next element of fibs:

fibs = 0 : 1 : zipWith (+) (0 : 1 : ?) (1 : ?) ==>
fibs = 0 : 1 : 1 : zipWith (+) (1 : ?) (?)

The first element of each of the argument lists of zipWith is consumed. Now, when we evaluated it, we also know, what the value of the next thunk is and we can fill it in. That allows us to evaluate the next cell, and so on:

fibs = 0 : 1 : 1 : zipWith (+) (1 : ?) (?) ==>
fibs = 0 : 1 : 1 : zipWith (+) (1 : 1 : ?) (1 : ?) ==>
fibs = 0 : 1 : 1 : 2 : zipWith (+) (1 : ?) (?) ==>
fibs = 0 : 1 : 1 : 2 : zipWith (+) (1 : 2 : ?) (2 : ?) ==>
fibs = 0 : 1 : 1 : 2 : 3 : zipWith (+) (2 : ?) (?) ==>
...

Answer 2

tail on an infinite list is very simple: generate the first argument if necessary, then throw it away.

So

fibs       =  0 : 1 : fibs'
tail fibs  =      1 : fibs'

and

tail fibs         =  1 : 1 : fibs''
tail (tail fibs)  =      1 : fibs''

and

tail (tail fibs)         =  1 : 2 : fibs'''
tail (tail (tail fibs))  =      2 : fibs'''

etc.