[Agda] Evaluation question

[Martin Escardo]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: CantorSearch.hs
Type: text/x-haskell
Size: 858 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210530/6ef6b070/attachment.bin>