# [Agda] evaluation in compilation

Serge D. Mechveliani mechvel at botik.ru
Wed Oct 3 16:35:44 CEST 2012

```On Wed, Oct 03, 2012 at 07:44:39AM +0200, Nils Anders Danielsson wrote:
> On 2012-10-02 22:22, Serge D. Mechveliani wrote:
>> For example, an algorithm of the cost  O(n^2)  needs to be programmed
>> in Agda also as taking  O(n^2),  not O(n^3).
>
> Are you saying that you're implementing a quadratic algorithm, but that
> Agda somehow makes it cubic? Can you give an example?

This was an error of mine.

in Agda.
It was due to a single conversion  Bin -> Nat  which has crept in the
test.
Now, I comment it out, and find that the `merge' method for sorting
(with no proof, so far, to compare to Glasgow Haskell)
costs  O(n*log(n))  in  Agda-MAlozo  -- similar as in Glasgow Haskell.

This was tested for a list  xs : List Nat  of small numbers, of length
12*(2^n),  n = 13, ..., 19.

The test prints only         hl = (head ys) :: (last ys) :: []
and a certain  alteredSum ys
for the ordered result  ys.
This is because the result printed out must be small.
On the other hand, this (I think) forces Agda to fully evaluate the
sorted list.

This test is also for  Bin.suc  and  concatenation with the same small
list xs0,  because these two operations repeat  2^19  times in the last
example. The whole test takes  29 sec,  while the part besides sorting
takes 3 sec. So everything looks good.

So far, I applied  --no-termination-check,
because it is difficult to prove termination for
concatCopies : {A : Set} -> Bin -> List A -> List A

I hope I could add a reasonable termination proof, but probably, the
performance test for merge sort does not depend on this.

Probably, I would add proofs to sorting and see the performance.
I am sure that this would not change the cost order, at least, the proof
for orderedness.

My current impresssion is:

so far I do not find any essential gap in Agda.

By an essential gap I mean an essential obstackle for designing a
computer algebra library for an efficient computation (and also for
proofs, for verified programming, for generic programming with something
like classes).

Why do the developers talk of slowness, of call by name?
Does this refer only to evaluation during compilation?

Concerning preventing of the compilation time
evaluation for a large constant
-------------------------------
I introduce the module  Constants.agda,  and put there, for example,

suchAndSuchCounter : Bin
suchAndSuchCounter = fromBits (0b :: 0b :: 0b :: 0b :: 0b ::
0b :: 0b :: 0b :: 0b :: 0b :: 1b :: [])
-- 2^10

And  Main.agda  imports from the module  Constants.
It looks better than  inputting from a file,  and this also prevents
unneeded normalization at the compilation time.
How reliable is this?

Probably, there are more urgent problems than this, of which I am not
so far aware.

Thanks,

------
Sergei

```