[Agda] Evaluation question

[Ulf Norell]

That's interesting. I don't know what changed, but it's very recent. I was
using a build from a couple
of weeks ago and got the doubly exponential behaviour.

My guess would be https://github.com/agda/agda/issues/5379 which changed
the strictness behaviour
of the reduce monad.

/ Ulf

On Mon, May 31, 2021 at 9:42 AM Martin Escardo <m.escardo at cs.bham.ac.uk>
wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210531/a27d957c/attachment.html>