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