[Agda] Evaluation question

[mechvel at scico.botik.ru]

The last exponential adventure I had with Agda 2.6.1 was with the 
function like

   f x =  let y = g x in h y y

The Glasgow Haskell compiler supports sharing of  y,  and Agda evaluates 
y twice
(the needed sharing can be reached by introducing a certain additional 
function, as Ulf advised).
I expect the same will be with `where' and `case'.
This gives a cost explosion when mixed with recursion.

I do not know of whether this thing is somehow hidden in your example,
I just write for any occasion.

--
SM



On 2021-05-30 14:41, Martin Escardo 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