[Agda] defining coinductive types

[Aaron Stump]

On Tue, Dec 17, 2013 at 9:59 AM, Nils Anders Danielsson <nad at cse.gu.se>wrote:

> 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.
>

I see.  Certainly some of those definitions are remarkably compact.


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

This is very helpful to me.  Since I'm not the biggest Haskeller in the
world, would you mind making the complete source file you used for testing
(I assume you compiled this with ghc, and have a 'main' entrypoint)
available to me?  I'd appreciate it.  It would help me experiment with
these encodings.

Thanks,
Aaron


>
>   {-# 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131217/e56bfd69/attachment.html