[Agda] Evaluation question
Martin Escardo
m.escardo at cs.bham.ac.uk
Mon May 31 22:28:13 CEST 2021
On 31/05/2021 10:15, ulf.norell at gmail.com wrote:
> 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.
I think I know why: In Agda 2.6.1 the default is --auto-inline, as
opposed to Agda 2.6.2.
But case_of_ is useless efficiency-wise with inlining.
In fact, your proposed solution with case_of_ doesn't make any
difference in Agda 2.6.1, unless you declare
{-# NOINLINE case_of_ #-}
With this, I can get up to n=17 with 2.6.1 in example2, in 37sec in a
core-i7 machine. And the time is 2^n quite precisely experimentally.
For Agda 2.6.2 release candidate, I can do n=17 for example2 in 25sec
provided:
* I compile Agda with -foptimise-heavily
* I run Agda with --auto-inline
* But keep case_of_ as NOINLINE
Because optimise-heavily and --auto-inline were default in 2.6.1,
something seems to have got better in Agda 2.6.2. But for examples like
this only. My repository TypeTopology types checks in 4min in both 2.6.1
and 2.6.2 with the above options.
Also, as discussed, the original version without case_of_ is already
fast enough in Agda 2.6.2.
Martin
>
> My guess would be https://github.com/agda/agda/issues/5379
> <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
> <mailto: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
> <mailto: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>
> > <mailto: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>
> <mailto: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>
> > <https://lists.chalmers.se/mailman/listinfo/agda
> <https://lists.chalmers.se/mailman/listinfo/agda>>
> >
>
> --
> Martin Escardo
> http://www.cs.bham.ac.uk/~mhe <http://www.cs.bham.ac.uk/~mhe>
>
--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
More information about the Agda
mailing list