<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">&lt;<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>&gt;</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&#39;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 &#39;main&#39; entrypoint) available to me?  I&#39;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 -&gt; r)<br>
    | OTail (StreamObserver a r)<br>
<br>
  type Stream a = forall r. StreamObserver a r -&gt; r<br>
<br>
  head&#39; :: Stream a -&gt; a<br>
  head&#39; xs = xs (OHead id)<br>
<br>
  tail&#39; :: Stream a -&gt; Stream a<br>
  tail&#39; xs = xs . OTail<br>
<br>
  cons :: a -&gt; Stream a -&gt; Stream a<br>
  cons x xs (OHead f) = f x<br>
  cons x xs (OTail o) = xs o<br>
<br>
  zipWith1 :: (a -&gt; b -&gt; c) -&gt; Stream a -&gt; Stream b -&gt; Stream c<br>
  zipWith1 f xs ys (OHead g) = g (f (head&#39; xs) (head&#39; ys))<br>
  zipWith1 f xs ys (OTail o) = zipWith1 f (tail&#39; xs) (tail&#39; ys) o<br>
<br>
  zipWith2 :: (a -&gt; b -&gt; c) -&gt; Stream a -&gt; Stream b -&gt; Stream c<br>
  zipWith2 f xs ys =<br>
    cons (f (head&#39; xs) (head&#39; ys)) (zipWith2 f (tail&#39; xs) (tail&#39; 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&#39; 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&#39; fib2) o<br>
<br>
  fib3 :: Stream Integer<br>
  fib3 = cons 0 (cons 1 (zipWith1 (+) fib3 (tail&#39; fib3)))<br>
<br>
  fib4 :: Stream Integer<br>
  fib4 = cons 0 (cons 1 (zipWith2 (+) fib4 (tail&#39; 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>