<div dir="ltr"><div>If we also fix the lambda-lifting issue, using case_of_, we can get it down to 2^n:</div><div><br></div><div style="margin-left:40px"><span style="font-family:monospace">epsilon : Nat → (Cantor → Bool) → Cantor<br>epsilon zero    p = λ i → false<br>epsilon (suc n) p =<br>  case p (cons false (epsilon n (p ∘ cons false))) of λ<br>    b → cons b (epsilon n (p ∘ cons b))</span></div><div><br></div><div>This version runs about 6 times slower than ghci, which I think isn't too bad.<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:07 AM Ulf Norell <<a href="mailto:ulf.norell@gmail.com">ulf.norell@gmail.com</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"><div dir="ltr"><div>I assume we are talking type-checking time evaluation and not compiling to Haskell.</div><div><br></div><div>In this case, surprisingly, I don't think the lambda lifting of b is the problem. Rather I think</div><div>the double exponential is because the Agda abstract machine is bad at evaluating lambdas.</div><div>If you get rid of the lambda in the local α:<br></div><div style="margin-left:40px"><span style="font-family:monospace"><br></span></div><div style="margin-left:40px"><span style="font-family:monospace">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></span></div><div><br></div><div>it runs in what looks like 3^n to me. With this version I can C-c C-n example2 11 in 10s. Still far</div><div>from the Haskell performance, but at least it's no longer a double exponential.<br></div><div><br></div><div>/ Ulf<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">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>> 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">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><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>
</blockquote></div>