[Agda] evaluation in compilation

[Serge D. Mechveliani]

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.

Yesterday I had a false impression about the list sorting performance 
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