[Agda] Evaluation question

[Ulf Norell]

I assume we are talking type-checking time evaluation and not compiling to
Haskell.

In this case, surprisingly, I don't think the lambda lifting of b is the
problem. Rather I think
the double exponential is because the Agda abstract machine is bad at
evaluating lambdas.
If you get rid of the lambda in the local α:

epsilon : Nat → (Cantor → Bool) → Cantor
epsilon zero    p = λ i → false
epsilon (suc n) p = cons b α
  where
    b : Bool
    b = p (cons false (epsilon n λ α → p (cons false α)))

    α : Cantor
    α = epsilon n (p ∘ cons b)

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
from the Haskell performance, but at least it's no longer a double
exponential.

/ Ulf

On Sun, May 30, 2021 at 1:41 PM Martin Escardo <m.escardo at cs.bham.ac.uk>
wrote:

> Consider the following Haskell code (also attached) and its translation
> to Agda (not included).
>
> * In Agda the (good) runtime behaviour of example1 is replicated - it is
> linear.
>
> * However, example2 in Haskell runs in roughly O(2^n) whereas in Agda it
> seems to run in O(2^(2^n)). The largest I can run in Agda is n=4.
>
> How do I rewrite the program in Agda to get the same times as in
> Haskell? The crucial function is "epsilon".
>
> --
> *Main> example1 (nat (10^6))
> True
> (2.83 secs, 696,069,600 bytes)
> *Main> example2 (nat (15))
> False
> (1.09 secs, 504,960,752 bytes)
> *Main> example2 (nat 15)
> False
> (1.11 secs, 504,960,752 bytes)
> *Main> example2 (nat 16)
> False
> (2.44 secs, 1,130,698,664 bytes)
> *Main> example2 (nat 17)
> False
> (5.42 secs, 2,516,654,176 bytes)
> *Main> example2 (nat 18)
> False
> (12.03 secs, 5,571,156,248 bytes)
> --
>
> data Nat = Zero | Succ Nat
>
> type Cantor = Nat -> Bool
>
> cons :: Bool -> Cantor -> Cantor
> cons b alpha Zero     = b
> cons b alpha (Succ n) = alpha n
>
> epsilon :: Nat -> (Cantor -> Bool) -> Cantor
> epsilon Zero p     = \i -> False
> epsilon (Succ n) p = cons b alpha
>  where
>   b :: Bool
>   b = p (cons False (epsilon n (\alpha -> p (cons False alpha))))
>
>   alpha :: Cantor
>   alpha = epsilon n (\alpha -> p (cons b alpha))
>
> forevery :: Nat -> (Cantor -> Bool) -> Bool
> forevery n p = p (epsilon n p)
>
> -- Examples
>
> nat :: Integer -> Nat
> nat 0 = Zero
> nat n = Succ (nat (n-1))
>
> p1 :: Nat -> Cantor -> Bool
> p1 n alpha = alpha n == alpha n
>
> example1 :: Nat -> Bool
> example1 n = forevery (Succ n) (p1 n)
>
> p2 :: Nat -> Cantor -> Bool
> p2 Zero     alpha = True
> p2 (Succ n) alpha = alpha Zero /= p2 n (\i -> alpha (Succ i))
>
> example2 :: Nat -> Bool
> example2 n = forevery n (p2 n)
>
> I think that "b" in Haskell gets evaluated at most once, but in Agda it
> is evaluated zero times or else repeatedly. But I may be wrong. I tried
> primForce but it didn't seem to make any difference.
>
> How do I make example2 as fast as in Haskell?
>
> Martin
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210531/b384be5a/attachment.html>