Understanding direct self-reference in Haskell

Question

I just started learning Haskell a few hours a go, trying to comprehend what this The Fibonacci sequence does:

fibs = 0 : 1 : next fibs
  where
    next (a : t@(b:_)) = (a+b) : next t

next function is strange to me, it will eventually get some "invalid" input, like at first it goes like this:

next (0:1) = (0+1) : next [1]

but then next ([1]) is not operable, since t@(b:_) has no input in it. So how does next work?

And my next confusion is fib itself, since it's suppose to be a Fibonacci sequence, I assume it will get fibs = 0 : 1 : 1 : next fibs after the first step, but then we will need to compute next([0, 1, 1]) witch gives (0+1): next([1, 1]) == 1 : next([1, 1]), we get the initial element 1, so in next([0, 1, 1]), the first value of the list (in next fibs) will be 1, but attached this 1 to the original fib, we get 0 : 1 : 1 : 1 which is not Fibonacci sequence.

I think I misunderstood something, so how it actually works?

Answer 1

The standard way to define the result of a recursive definition is to approximate such value starting from undefined and unfolding the recursion from there as follows:

-- A function describing the recursion
f x = 0 : 1 : next x

fibs0 = undefined
fibs1 = f fibs0 = 0 : 1 : next undefined 
      -- next requires at least 2 elements
      = 0 : 1 : undefined
fibs2 = f fibs1 = 0 : 1 : next fibs1
      = 0 : 1 : next (0 : 1 : undefined)
      = 0 : 1 : 1 : next (1 : undefined)
      -- next requires at least 2 elements
      = 0 : 1 : 1 : undefined
fibs3 = f fibs2 = 0 : 1 : next fibs2
      = 0 : 1 : next (0 : 1 : 1 : undefined)
      = 0 : 1 : 1 : next (1 : 1 : undefined)
      = 0 : 1 : 1 : 2 : next (1 : undefined)
      -- next requires at least 2 elements
      = 0 : 1 : 1 : 2 : undefined
fibs4 = f fibs3 = 0 : 1 : next fibs3
      = 0 : 1 : next (0 : 1 : 1 : 2 : undefined)
      ...

If we keep going on we will approach the full sequence "at the limit", approximating it step by step. This informal argument can be formally justified through the Kleene's fixed point theorem.