[Agda] Evaluation question

[Ulf Norell]

Actually, after fixing the duplication of b the lambdas are no longer an
issue, so

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

has the same performance.

/ Ulf

On Mon, May 31, 2021 at 9:18 AM Ulf Norell <ulf.norell at gmail.com> wrote:

> If we also fix the lambda-lifting issue, using case_of_, we can get it
> down to 2^n:
>
> epsilon : Nat → (Cantor → Bool) → Cantor
> epsilon zero    p = λ i → false
> epsilon (suc n) p =
>   case p (cons false (epsilon n (p ∘ cons false))) of λ
>     b → cons b (epsilon n (p ∘ cons b))
>
> This version runs about 6 times slower than ghci, which I think isn't too
> bad.
>
> / Ulf
>
> On Mon, May 31, 2021 at 9:07 AM Ulf Norell <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>
>> 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/9b465804/attachment.html>