[Agda] interactive Bin arith performance

[Ulf Norell]

On Thu, Jan 31, 2019 at 4:40 PM Sergei Meshveliani <mechvel at botik.ru> wrote:

> 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.
>

The cost of running an algorithm is not related to the size of the output,
or
the whole P vs NP thing would be kind of silly.


> Also why strict? Is not Agda lazy?
>

A function can still be strict in some arguments even with lazy evaluation.


> 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'' ?
>

Yes.


> > 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?
>

Indeed. But equality proofs are erased. The _<_ proof may or may not be
erased depending on how you defined it.


> 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?
>

No. Type checking doesn't do any analysis of this sort.


>
> 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?
>

How is it known that no proofs need to be evaluated for test0? C-c C-n runs
the
compile-time evaluator, which is what the type checker uses when evaluating
terms
for type checking. This evaluator does not have the same freedoms when it
comes
to erasing proof objects as the run-time code generator. In particular it
needs to
evaluate equality proofs if they are matched on, to avoid looping on
inconsistent
assumptions.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190131/c770ab4c/attachment.html>