Is it possible to define `fib` coinductive stream w/o sized types?

Question

In Agda with --guardedness, we can define productive definitions using copatterns like the following

repeat : ∀ {A} -> (a : A) -> Stream A
repeat a .head = a
repeat a .tail = repeat a

Given the coinductive definition of Stream. Similarly we can define zipWith:

zipWith : ∀ {A B C} -> (A -> B -> C) -> Stream A -> Stream B -> Stream C
zipWith f a b .head = f (a .head) (b .head)
zipWith f a b .tail = zipWith f (a .tail) (b .tail)

However, if we want to go further and define the Fibonacci stream:

fib : Stream Nat
fib .head = 0
fib .tail .head = 1
fib .tail .tail = zipWith _+_ fib (fib .tail)

Agda productivity checker will complain that the last clause is not (structurally) productive. In my impression, the recommended way to make fib work is to introduce a size parameter to the definition of Stream. However, since sized types are incompatible with guardedness, we have to completely get rid of guardedness if we want to use sized types (or give up --safe, which is undesirable). So, I wonder if there's a way to make fib work with guardedness (which means, no sized types)?

Answer 1

I recommend the state machine definition that we'd use for looping over Fibonacci numbers:

fib' : ℕ → ℕ → Stream ℕ
head (fib' x y) = x
tail (fib' x y) = fib' y (x + y)

fib : Stream ℕ
fib = fib' 0 1

The classic Haskell zipWith definition is more intended to show off several language features at once, and it's both less efficient and harder to reason about than the above version.

It's a good general approach to try to figure out the state that has to remembered and updated on each unfolding, when we try to convert complicated coinduction to versions that are more palatable to Agda.