[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.
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
More information about the Agda
mailing list