8
$\begingroup$

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

$\endgroup$
2
  • 1
    $\begingroup$ Note that Agda's guardedness checker will refuse guard-check: ``` map : ∀ {A B} -> (A -> B) -> Stream A -> Stream B ; map f a .head = f (a .head) ; map f a .tail = map f (a .tail) ; repeat' : ∀ {A} -> (a : A) -> Stream A ; repeat' a .head = a ; repeat' a .tail = map (λ x -> x) (repeat' a) ; ``` So it seems that Agda's guard checker is very, very limited. $\endgroup$ Feb 13, 2022 at 4:44
  • 1
    $\begingroup$ Is there a language whose guard condition is not that limited? Coq will also reject this example, so I'm curious what standard "very, very limited" is relative to. $\endgroup$
    – Li-yao Xia
    Feb 13, 2022 at 16:43

1 Answer 1

8
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.