[Agda] Evaluation question

[Martin Escardo]

Thanks, Ulf, for the three messages. I will try all that.

At the same time, just before your message, I tried the release
candidate of Agda 2.6.2, without any change to my code, and I can run
example2 11 in about the same time as you.

What has changed in 2.6.2 regarding evaluation?

Best,
Martin

On 31/05/2021 08:07, ulf.norell at gmail.com wrote:
> 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
> <mailto: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 <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe