<div dir="ltr"><div dir="ltr"><div dir="ltr"><br></div><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Feb 1, 2019 at 10:50 AM 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">Can anybody, please, explain what is happening in the below simple and<br>
self-contained example? <br>
<br>
-----------------------------------------------------------------<br>
f : (m : ℕ) → ∃ (\n → n ≤ m)<br>
<br>
f 0       =  (0 , ≤-refl)<br>
f (suc m) =  let (n , n≤m) = f m<br>
             in<br>
             case suc n ≤? m of \<br>
                             { (yes _) → (n , ≤-step n≤m)<br>
                             ; (no _ ) → (suc n , s≤s n≤m) }<br>
<br>
g = proj₁ ∘ f<br>
-----------------------------------------------------------------<br>
<br>
emacs,   C-c C-l <br>
             g 22<br>
<br>
is evaluated in  25 sec.<br></blockquote><div><br></div><div>In this case the problem isn't proof evaluation, but the 'let' which doesn't share</div><div>evaluation of the right-hand side. This means that every occurrence of `n`</div><div>corresponds to a new call to `f`, making it exponential. If you change `f` to</div><div><br></div><div><div>f 0       =  (0 , ≤-refl)</div><div>f (suc m) =</div><div>  case f m of λ where</div><div>    (n , n≤m) →</div><div>             case suc n ≤? m of \</div><div>                             { (yes _) → (n , ≤-step n≤m)</div><div>                             ; (no _ ) → (suc n , s≤s n≤m) }</div></div><div><br></div><div>it runs fast (or as fast as the unary implementation of ≤? allows).</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">Still the evaluation cost of the compiled code looks as quadratic.<br>
I think, this is because  k ≤? l  is solved  m  times for  k  having  k<br>
`suc' constructors for  k = 0, ..., m. <br></blockquote><div><br></div><div>Indeed. _≤?_ is linear in the value of the first argument.</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">Does the compiled  g  evaluate proofs?<br>
If not, then who has removed the  proof evaluation part (PEP)<br>
from the code?<br>
<br>
Type checking produces  Foo.agdai  which has PEP,<br>
MAlonzo takes Foo.agdai, compiles to Haskell with removing the PEP, <br>
and  Foo.hs  does not have PEP<br>
-- is this so?</blockquote><div><br></div><div>Essentially yes, but the erasure actually happens when compiling the type</div><div>checked code to an intermediate language (called treeless), which the GHC</div><div>backend then turns into Haskell code.</div><div><br></div><div>Also it's a bit misleading to talk about proof evaluation, since there is no</div><div>clear distinction between proofs and terms in Agda.</div><div><br></div><div>/ Ulf</div></div></div></div>