<div dir="ltr"><div dir="ltr"><br></div><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Jan 31, 2019 at 4:40 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">On Thu, 2019-01-31 at 12:13 +0100, Ulf Norell wrote:<br>
> Without looking at the code my guess would be that you are strict in<br>
> the proof objects. At runtime (after compilation) the proof objects<br>
> are erased and not evaluated, but at compile time you evaluate the<br>
> generated proofs, causing the terrible performance.<br>
> <br>
<br>
Well, DivRem data has two proofs in it, and divRem for Bin is defined <br>
recursively, similarly as by the construction of the bit list. <br>
How large can be a proof for that  520 == 52 * 10 + 0  in binary system?<br>
I expect that in recursion there appear (log 520 =~ 9) of such proofs. <br>
There are also proofs for  r < 10  -- less than 5 steps for binary<br>
system -- something like comparing bit lists lexicographically.<br>
<br>
If all of them are computed strict, I still doubt about their great<br>
cost. Because their data look small in size. <br></blockquote><div><br></div><div>The cost of running an algorithm is not related to the size of the output, or</div><div>the whole P vs NP thing would be kind of silly.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">Also why strict? Is not Agda lazy?<br></blockquote><div><br></div><div>A function can still be strict in some arguments even with lazy evaluation.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">Well,  divRem 520 10  calls for something like  divRem 520/2 10.<br>
Then,  q1, r1, and proofs for  <br>
                          p11 : 520 = q1*10 + r1,   p12 : r1 < 10<br>
<br>
for binary codes are being restored in a simple way from  q2, r2, and<br>
the proofs for  <br>
           p21 : 520/2 = q2*10 + r2,   p22 : r2 < 10.<br>
<br>
p11 and p12 computed from p21, p22.<br>
Do you mean that this forces unwinding all the structure of  pij,<br>
and in these sense the method is ``strict in the proof objects'' ?<br></blockquote><div><br></div><div>Yes.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">> At runtime (after compilation) the proof objects are erased and not <br>
> evaluated<br>
<br>
Probably, this is not for the general case (?).<br>
For example, for <br>
    p : 100 < (101 : Nat)<br>
    p = s<=s (s<=s (s<=s (s<=s ... <br>
<br>
the proof  p  will be evaluated in a compiled program, if the main<br>
function prints  p.<br>
Do I understand correct?<br></blockquote><div><br></div><div>Indeed. But equality proofs are erased. The _<_ proof may or may not be</div><div>erased depending on how you defined it.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">And in my example of  test0 = remainder (divRem 520 10),  <br>
<br>
proofs are not evaluated in the compiled program.<br>
<br>
Now, return to Agda interpreter.<br>
Before  <br>
       C-c C-n test0,<br>
<br>
there has been applied  C-c C-l.  And this type-checks everything in all<br>
the related .agda modules. <br>
(Suppose for simplicity that we have all the library in a large single<br>
module.) <br>
Hence it is already known, which proofs need to be evaluated in order to<br>
print out  test0.  <br>
Is it so?<br></blockquote><div><br></div><div>No. Type checking doesn't do any analysis of this sort.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex">
<br>
And it is known that no proofs need to be evaluated for the main goal of<br>
test0. Why <br>
           C-c C-n test0<br>
<br>
evaluates some proofs here? <br></blockquote><div><br></div><div>How is it known that no proofs need to be evaluated for test0? C-c C-n runs the</div><div>compile-time evaluator, which is what the type checker uses when evaluating terms</div><div>for type checking. This evaluator does not have the same freedoms when it comes</div><div>to erasing proof objects as the run-time code generator. In particular it needs to</div><div>evaluate equality proofs if they are matched on, to avoid looping on inconsistent</div><div>assumptions.</div><div><br></div><div>/ Ulf</div><div> </div></div></div>