[Agda] interactive Bin arith performance

[Sergei Meshveliani]

On Thu, 2019-01-31 at 12:13 +0100, Ulf Norell wrote:
> Without looking at the code my guess would be that you are strict in
> the proof objects. At runtime (after compilation) the proof objects
> are erased and not evaluated, but at compile time you evaluate the
> generated proofs, causing the terrible performance.
> 

Well, DivRem data has two proofs in it, and divRem for Bin is defined 
recursively, similarly as by the construction of the bit list. 
How large can be a proof for that  520 == 52 * 10 + 0  in binary system?
I expect that in recursion there appear (log 520 =~ 9) of such proofs. 
There are also proofs for  r < 10  -- less than 5 steps for binary
system -- something like comparing bit lists lexicographically.

If all of them are computed strict, I still doubt about their great
cost. Because their data look small in size. 

Also why strict? Is not Agda lazy?

Well,  divRem 520 10  calls for something like  divRem 520/2 10.
Then,  q1, r1, and proofs for  
                          p11 : 520 = q1*10 + r1,   p12 : r1 < 10

for binary codes are being restored in a simple way from  q2, r2, and
the proofs for  
           p21 : 520/2 = q2*10 + r2,   p22 : r2 < 10.

p11 and p12 computed from p21, p22.
Do you mean that this forces unwinding all the structure of  pij,
and in these sense the method is ``strict in the proof objects'' ?


> At runtime (after compilation) the proof objects are erased and not 
> evaluated

Probably, this is not for the general case (?).
For example, for 
    p : 100 < (101 : Nat)
    p = s<=s (s<=s (s<=s (s<=s ... 

the proof  p  will be evaluated in a compiled program, if the main
function prints  p.
Do I understand correct?

And in my example of  test0 = remainder (divRem 520 10),  

proofs are not evaluated in the compiled program.

Now, return to Agda interpreter.
Before  
       C-c C-n test0,

there has been applied  C-c C-l.  And this type-checks everything in all
the related .agda modules. 
(Suppose for simplicity that we have all the library in a large single
module.) 
Hence it is already known, which proofs need to be evaluated in order to
print out  test0.  
Is it so?

And it is known that no proofs need to be evaluated for the main goal of
test0. Why 
           C-c C-n test0

evaluates some proofs here? 

Thanks,

------
Sergei



> 
> On Thu, Jan 31, 2019 at 12:11 PM Sergei Meshveliani <mechvel at botik.ru>
> wrote:
> 
>         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
>