[Agda] Performance issues with --sharing
Peter Selinger
selinger at mathstat.dal.ca
Fri Sep 25 15:47:32 CEST 2015
Sergei Meshveliani wrote:
>
> On Thu, 2015-09-24 at 13:57 -0300, Peter Selinger wrote:
> > Dear all,
> >
> > last month, in the thread "type check performance", Wolfram Kahl
> > suggested that I try the experimental --sharing feature in the
> > development branch.
> >
> > The issue at hand was Agda's extremely inefficient evaluation
> > strategy, which is normal order and not lazy: it recomputes the same
> > value a potentially unlimited number of times.
> >
> > [..]
> >
> > I've created a self-contained example below. In order to compare
> > different Agda versions without depending on different versions of the
> > standard library, I have made the example to be completely independent
> > of the library.
> >
> > Here are the results:
> > [..]
> >
> > ----------------------------------------------------------------------
> > -- Begin Agda Code
> > ----------------------------------------------------------------------
> >
> > -- Natural numbers
> > data Nat : Set where
> > zero : Nat
> > succ : Nat -> Nat
> >
> > _+_ : Nat -> Nat -> Nat
> > zero + m = m
> > succ n + m = succ (n + m)
> >
> > _-_ : Nat -> Nat -> Nat
> > zero - m = zero
> > n - zero = n
> > succ n - succ m = n - m
> >
> > {-# BUILTIN NATURAL Nat #-}
> > {-# BUILTIN NATPLUS _+_ #-}
> > {-# BUILTIN NATMINUS _-_ #-}
> >
> > -- Lists
> > data List (X : Set) : Set where
> > nil : List X
> > _::_ : X -> List X -> List X
> >
> > replicate : ∀ {X} -> Nat -> X -> List X
> > replicate zero x = nil
> > replicate (succ n) x = x :: replicate n x
> >
> > foldl : ∀ {A B} -> (A -> B -> A) -> A -> List B -> A
> > foldl f a nil = a
> > foldl f a (x :: xs) = foldl f (f a x) xs
> >
> > -- Test
> > test : Nat -> Nat
> > test n = foldl (\a x -> succ ((a + x) - a)) 0 (replicate n 1)
>
>
> But how precisely the test is run?
>
> For n : Nat
> n = 12345678,
>
> how much (show n) will take?
> Will the test convert n into the unary system and back?
>
> (I do not know what is the effect of the above BUILTIN).
>
> Instead of measuring the true foldl, could happen so that it measures
> the conversion costs of Decimal <--> Unary for n ?
>
> In the performance tests, I do not use BUILTIN, and use the binary
> arithmetic of Bin for the counter like n above.
> And I do not know, may be BUILTIN is simpler.
You will notice that the function that is being folded here,
(\a x -> succ ((a + x) - a))
is the second projection, i.e., a+x-a = x. So no large numbers ever
appear in this example; in fact, test n always returns 2.
To eliminate any doubt, just fold a boolean function:
data Bool : Set where
true : Bool
false : Bool
and : Bool -> Bool -> Bool
and true true = true
and _ _ = false
test2 : Nat -> Bool
test2 n = foldl (\a x -> and a (and a x)) true (replicate n true)
You will get exactly the same timing behavior (up to a constant
factor). I used BUILTIN primarily so I could write "test 18" instead
of "test (succ (succ (succ ...)))".
-- Peter
More information about the Agda
mailing list