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