[Agda] interactive Bin arith performance

[Sergei Meshveliani]

On Thu, 2019-01-31 at 07:03 +0100, Ulf Norell wrote:
> On Wed, Jan 30, 2019 at 10:58 PM Sergei Meshveliani <mechvel at botik.ru>
> wrote:
> 
>         
>         Does it make difference for performance whether the module
>         M1.agda is previously compiled or not?  
>         (I have an impression that it is equally slow).
> 
> 
> It makes no difference.


I see. 
The remaining question is: why 10.000 slow down?
A particular method applied to division of 520 by 10 in binary system
with a particular representation shows this ratio.
Other examples, like 10^4 - 10^3,  show a small ratio, I do not recall,
somewhat from 10 to 50, this latter ratio looks natural.


If Agda developers ask, I can provide the code of this  binary-4.2-pre: 
аbout 10 .agda files, the size of zip file about 40 Кb.
(divMod uses all these modules).


My hope was as follows. An equational prover in the project is going to
be based on functions of computer algebra, like, say, divMod for binary
numbers, a bit more complex.
Their evaluation takes most of the cost in the proof search.

Approach (I):
if the type checker interprets these functions about 100 times slower
than the compiled functions run, then this can be tolerable.
But 10.000 slow down will make the approach practically useless.

Approach (II): 
a certain basic function in the prover is compiled, and the interpreter
in the type checker needs to be able to run fast a compiled function
(for example, this is possible in Glasgow Haskell).

Approach (III):
a basic function  f  is in Haskell, and it is a fixed function that
makes almost all the prover. It is compiled once by GHC, and is ready to
run fast. It takes and returns the data like, say List (List Bin),
and this needs to be by the interface between Agda data and Haskell
data. The prover takes the returned  result :  List (List Bin),  
and the rest proof search is not expensive, it is interpreted by the
type checker. 

The best one is (II). But I do not know what problems the Agda project
will have to solve for (II).

If (I) and (II) fail, then consider (III).
I have a large library being run under GHC. And it only remains to
arrange an interface like  List (List Bin) -- [[Bin]]
-- something of this kind.
I wonder of whether such an interface can be set.
And (III) still does not look nice, it can be considered as a temporary
solution.

Regards,

------
Sergei