[Agda] Performance issues with --sharing
Sergei Meshveliani
mechvel at botik.ru
Fri Sep 25 16:58:09 CEST 2015
On Fri, 2015-09-25 at 10:47 -0300, Peter Selinger wrote:
> 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.
>
> [..]
I knew of this property of the given combining function.
I meant another point:
the value origin for the counter n, which is used to obtain some
long list (replicate n 1).
Regards,
------
Sergei
More information about the Agda
mailing list