[Agda] defining coinductive types

[Nils Anders Danielsson]

On 2013-12-16 18:48, Aaron Stump wrote:
> Probably there is some good reason this approach is not followed.

I guess one important reason is that I and others are used to
programming with lazy data types in Haskell, and want to be able to
write similar programs in Agda. Consider parser combinators, for
instance.

One might also be interested in performance. Consider the following four
Haskell definitions of the stream of Fibonacci numbers:

   {-# LANGUAGE RankNTypes #-}

   data StreamObserver a r
     = OHead (a -> r)
     | OTail (StreamObserver a r)

   type Stream a = forall r. StreamObserver a r -> r

   head' :: Stream a -> a
   head' xs = xs (OHead id)

   tail' :: Stream a -> Stream a
   tail' xs = xs . OTail

   cons :: a -> Stream a -> Stream a
   cons x xs (OHead f) = f x
   cons x xs (OTail o) = xs o

   zipWith1 :: (a -> b -> c) -> Stream a -> Stream b -> Stream c
   zipWith1 f xs ys (OHead g) = g (f (head' xs) (head' ys))
   zipWith1 f xs ys (OTail o) = zipWith1 f (tail' xs) (tail' ys) o

   zipWith2 :: (a -> b -> c) -> Stream a -> Stream b -> Stream c
   zipWith2 f xs ys =
     cons (f (head' xs) (head' ys)) (zipWith2 f (tail' xs) (tail' ys))

   fib1 :: Stream Integer
   fib1 (OHead f)         = f 0
   fib1 (OTail (OHead f)) = f 1
   fib1 (OTail (OTail o)) = zipWith1 (+) fib1 (tail' fib1) o

   fib2 :: Stream Integer
   fib2 (OHead f)         = f 0
   fib2 (OTail (OHead f)) = f 1
   fib2 (OTail (OTail o)) = zipWith2 (+) fib2 (tail' fib2) o

   fib3 :: Stream Integer
   fib3 = cons 0 (cons 1 (zipWith1 (+) fib3 (tail' fib3)))

   fib4 :: Stream Integer
   fib4 = cons 0 (cons 1 (zipWith2 (+) fib4 (tail' fib4)))

If I use GHC 7.6.3, then fib2 and fib4 are reasonably fast, but fib1 and
fib3 are horribly slow. If I turn off optimisations, then fib2 is also
horribly slow.

-- 
/NAD