<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Dec 17, 2013 at 9:59 AM, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On 2013-12-16 18:48, Aaron Stump wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Probably there is some good reason this approach is not followed.<br>
</blockquote>
<br></div>
I guess one important reason is that I and others are used to<br>
programming with lazy data types in Haskell, and want to be able to<br>
write similar programs in Agda. Consider parser combinators, for<br>
instance.<br></blockquote><div><br></div><div>I see. Certainly some of those definitions are remarkably compact.</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
One might also be interested in performance. Consider the following four<br>
Haskell definitions of the stream of Fibonacci numbers:<br></blockquote><div><br></div><div>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.</div>
<div><br></div><div>Thanks,</div><div>Aaron</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
{-# LANGUAGE RankNTypes #-}<br>
<br>
data StreamObserver a r<br>
= OHead (a -> r)<br>
| OTail (StreamObserver a r)<br>
<br>
type Stream a = forall r. StreamObserver a r -> r<br>
<br>
head' :: Stream a -> a<br>
head' xs = xs (OHead id)<br>
<br>
tail' :: Stream a -> Stream a<br>
tail' xs = xs . OTail<br>
<br>
cons :: a -> Stream a -> Stream a<br>
cons x xs (OHead f) = f x<br>
cons x xs (OTail o) = xs o<br>
<br>
zipWith1 :: (a -> b -> c) -> Stream a -> Stream b -> Stream c<br>
zipWith1 f xs ys (OHead g) = g (f (head' xs) (head' ys))<br>
zipWith1 f xs ys (OTail o) = zipWith1 f (tail' xs) (tail' ys) o<br>
<br>
zipWith2 :: (a -> b -> c) -> Stream a -> Stream b -> Stream c<br>
zipWith2 f xs ys =<br>
cons (f (head' xs) (head' ys)) (zipWith2 f (tail' xs) (tail' ys))<br>
<br>
fib1 :: Stream Integer<br>
fib1 (OHead f) = f 0<br>
fib1 (OTail (OHead f)) = f 1<br>
fib1 (OTail (OTail o)) = zipWith1 (+) fib1 (tail' fib1) o<br>
<br>
fib2 :: Stream Integer<br>
fib2 (OHead f) = f 0<br>
fib2 (OTail (OHead f)) = f 1<br>
fib2 (OTail (OTail o)) = zipWith2 (+) fib2 (tail' fib2) o<br>
<br>
fib3 :: Stream Integer<br>
fib3 = cons 0 (cons 1 (zipWith1 (+) fib3 (tail' fib3)))<br>
<br>
fib4 :: Stream Integer<br>
fib4 = cons 0 (cons 1 (zipWith2 (+) fib4 (tail' fib4)))<br>
<br>
If I use GHC 7.6.3, then fib2 and fib4 are reasonably fast, but fib1 and<br>
fib3 are horribly slow. If I turn off optimisations, then fib2 is also<br>
horribly slow.<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD<br>
</font></span></blockquote></div><br></div></div>