[Agda] test report

[mechvel at scico.botik.ru]

Dear all,

I report of a test for Agda-2.6.1 + MAlonzo for a certain real-world 
program for polynomials.

There is a simple method `simple' to find something and `efficient'.
All this is first programmed in Haskell (without proofs) and run under 
ghc-8.8.3.
* `efficient' must be supplied with the proof for its equivalence to 
`simple'.
* It needs to be almost as fast as the Haskell program, say, 3 times 
slower.

Concerning proof:
if it was possible to separate proof from `efficient', then its 
proof-free part would be
as simple and small as the Haskell's one.
The results are as follows.

* The source size is 5 times larger than Haskell's.
   It is all right, because there are many proofs, in particular, 
termination proved by proving
   various inequalities, and so on.

* The program is built in 5 minutes under +RTS -M8G -RTS.
   3 minutes of type checking, 2 minutes of complilation.
   In Haskell, it takes 3-4 seconds.
   It is all right, because there are many proofs.

* It has the same cost order in performance as Haskell's, and it is only 
2-3 times slower.
   Very good.

* I failed to separate the proof. Because it forced me to move things 
under 'let' and 'where'
   to the functions on the top level, giving them many "prefix" 
arguments.
   Also it has four functions mutually recursing each other. So that 
there was a great confusion
   when I started to add proofs as separate, the very evaluation function 
needs an awful refactoring
   and complication.
   So I gave up and incorporated the proof accumulation (very 
recursively) into the evaluation
   function. This proof is much-much simpler to form.
   I feared of the performance overhead caused by this.
   But as usual, there is not any essential overhead.
   I somehow keep in mind that there is a general reason for this.

* The Efficient.o file is  433 times larger than Efficient.o produced by 
GHC.
   I do not know, may be the MAlonzo part can be optimized.
   ?

Regards,

--
SM