[Agda] evaluation in compilation

[Serge D. Mechveliani]

On Mon, Oct 01, 2012 at 02:34:00PM +0400, Serge D. Mechveliani wrote:
> Please, how to prevent a compilation time evaluation?
> [..]


Nils  advises: 
> One option is to avoid hard-coded constants, and read data from a file.

Indeed, I tried in my example to input the counter value (bit list) from 
a file. It helps.
I expect this is because the compiler does not see a concrete value of 
the counter  n,  hence the whole concatenation expression is already 
normal at the compilation time.
And at the running time,  n  is read from a file, is converted to a 
concrete  n : Bin,  and the further normalization is performed.

Also I think that by "normalization" the agda people mean the 
normalization similar to the one of Term Rewriting, and here it is, 
probably, by applying the the program clauses.
But this makes it just evaluation by a program.
Does it?

Now, is reading from a file a regular way out?
Probably, not.
For example, in DoCon in  Haskell,  I use various tables, like
(a contrived example)
  primesUpToBound :: List Integer
  primesUpToBound =  <forming the list of first 10^5 primes>

Many functions use such a constant list as a global value. Hence it is 
computed not more than once, and its value is transmitted by the 
identifier (primesUpToBound).

In the current Agda, each such table will need to be accompanied with
the corresponding file containing some small parameter from which the 
table is built (to avoid compilation time evaluation).
This looks awkward. 

On the other hand, I start to think now that probably

  the problem of unneeded compilation time normalization is not as 
  urgently important as others (the developers could save effort).  

I have an impression that the  performance order  is more urgent.
I do not mean 10-20 times acceleration or such, no native code 
generators, no technical things, no huckery.
I mean preserving the cost order. 
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).
With Glasgow Haskell, I rely on this feature, and hope that Agda will
acquire such. 

Thanks,

------
Sergei