<div dir="ltr"><div>That's interesting. I don't know what changed, but it's very recent. I was using a build from a couple</div><div>of weeks ago and got the doubly exponential behaviour.</div><div><br></div><div>My guess would be <a href="https://github.com/agda/agda/issues/5379">https://github.com/agda/agda/issues/5379</a> which changed the strictness behaviour</div><div>of the reduce monad.<br></div><div><br></div><div>/ Ulf<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, May 31, 2021 at 9:42 AM Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk">m.escardo@cs.bham.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Thanks, Ulf, for the three messages. I will try all that.<br>
<br>
At the same time, just before your message, I tried the release<br>
candidate of Agda 2.6.2, without any change to my code, and I can run<br>
example2 11 in about the same time as you.<br>
<br>
What has changed in 2.6.2 regarding evaluation?<br>
<br>
Best,<br>
Martin<br>
<br>
On 31/05/2021 08:07, <a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a> wrote:<br>
> I assume we are talking type-checking time evaluation and not compiling<br>
> to Haskell.<br>
> <br>
> In this case, surprisingly, I don't think the lambda lifting of b is the<br>
> problem. Rather I think<br>
> the double exponential is because the Agda abstract machine is bad at<br>
> evaluating lambdas.<br>
> If you get rid of the lambda in the local α:<br>
> <br>
> epsilon : Nat → (Cantor → Bool) → Cantor<br>
> epsilon zero    p = λ i → false<br>
> epsilon (suc n) p = cons b α<br>
>   where<br>
>     b : Bool<br>
>     b = p (cons false (epsilon n λ α → p (cons false α)))<br>
> <br>
>     α : Cantor<br>
>     α = epsilon n (p ∘ cons b)<br>
> <br>
> it runs in what looks like 3^n to me. With this version I can C-c C-n<br>
> example2 11 in 10s. Still far<br>
> from the Haskell performance, but at least it's no longer a double<br>
> exponential.<br>
> <br>
> / Ulf<br>
> <br>
> On Sun, May 30, 2021 at 1:41 PM Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a><br>
> <mailto:<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>>> wrote:<br>
> <br>
>     Consider the following Haskell code (also attached) and its translation<br>
>     to Agda (not included).<br>
> <br>
>     * In Agda the (good) runtime behaviour of example1 is replicated - it is<br>
>     linear.<br>
> <br>
>     * However, example2 in Haskell runs in roughly O(2^n) whereas in Agda it<br>
>     seems to run in O(2^(2^n)). The largest I can run in Agda is n=4.<br>
> <br>
>     How do I rewrite the program in Agda to get the same times as in<br>
>     Haskell? The crucial function is "epsilon".<br>
> <br>
>     --<br>
>     *Main> example1 (nat (10^6))<br>
>     True<br>
>     (2.83 secs, 696,069,600 bytes)<br>
>     *Main> example2 (nat (15))<br>
>     False<br>
>     (1.09 secs, 504,960,752 bytes)<br>
>     *Main> example2 (nat 15)<br>
>     False<br>
>     (1.11 secs, 504,960,752 bytes)<br>
>     *Main> example2 (nat 16)<br>
>     False<br>
>     (2.44 secs, 1,130,698,664 bytes)<br>
>     *Main> example2 (nat 17)<br>
>     False<br>
>     (5.42 secs, 2,516,654,176 bytes)<br>
>     *Main> example2 (nat 18)<br>
>     False<br>
>     (12.03 secs, 5,571,156,248 bytes)<br>
>     --<br>
> <br>
>     data Nat = Zero | Succ Nat<br>
> <br>
>     type Cantor = Nat -> Bool<br>
> <br>
>     cons :: Bool -> Cantor -> Cantor<br>
>     cons b alpha Zero     = b<br>
>     cons b alpha (Succ n) = alpha n<br>
> <br>
>     epsilon :: Nat -> (Cantor -> Bool) -> Cantor<br>
>     epsilon Zero p     = \i -> False<br>
>     epsilon (Succ n) p = cons b alpha<br>
>      where<br>
>       b :: Bool<br>
>       b = p (cons False (epsilon n (\alpha -> p (cons False alpha))))<br>
> <br>
>       alpha :: Cantor<br>
>       alpha = epsilon n (\alpha -> p (cons b alpha))<br>
> <br>
>     forevery :: Nat -> (Cantor -> Bool) -> Bool<br>
>     forevery n p = p (epsilon n p)<br>
> <br>
>     -- Examples<br>
> <br>
>     nat :: Integer -> Nat<br>
>     nat 0 = Zero<br>
>     nat n = Succ (nat (n-1))<br>
> <br>
>     p1 :: Nat -> Cantor -> Bool<br>
>     p1 n alpha = alpha n == alpha n<br>
> <br>
>     example1 :: Nat -> Bool<br>
>     example1 n = forevery (Succ n) (p1 n)<br>
> <br>
>     p2 :: Nat -> Cantor -> Bool<br>
>     p2 Zero     alpha = True<br>
>     p2 (Succ n) alpha = alpha Zero /= p2 n (\i -> alpha (Succ i))<br>
> <br>
>     example2 :: Nat -> Bool<br>
>     example2 n = forevery n (p2 n)<br>
> <br>
>     I think that "b" in Haskell gets evaluated at most once, but in Agda it<br>
>     is evaluated zero times or else repeatedly. But I may be wrong. I tried<br>
>     primForce but it didn't seem to make any difference.<br>
> <br>
>     How do I make example2 as fast as in Haskell?<br>
> <br>
>     Martin<br>
> <br>
>     _______________________________________________<br>
>     Agda mailing list<br>
>     <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>><br>
>     <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
>     <<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a>><br>
> <br>
<br>
-- <br>
Martin Escardo<br>
<a href="http://www.cs.bham.ac.uk/~mhe" rel="noreferrer" target="_blank">http://www.cs.bham.ac.uk/~mhe</a><br>
</blockquote></div>