[Agda] interactive Bin arith performance

[Ulf Norell]

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.

/ Ulf

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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190131/65611c59/attachment.html>