<div dir="ltr"><div>I haven't looked at what the type checker is doing in detail that makes test2 so extremely slow, but note that built-in arithmetic does not kick in for open terms. In your example `(a + n) ∸ a` contains a free variable `n`, if the type checker has to evaluate it (which I suspect it does for test2, but not test1) it will use the non-built-in recursive definitions for `_+_` and `_∸_`.<br><br></div><div>I would advise abstracting over `a` whenever you can.<br></div><div><br></div>/ Ulf<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Feb 10, 2018 at 2:45 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear all,<br>
<br>
I need to type-check a program that uses a certain large global constant<br>
a.<br>
And the function  test2  below is type-checked much longer than  test1,<br>
It takes too long.<br>
This is  Agda 2.5.3.<br>
<br>
Can people, please, explain the effect?<br>
<br>
------------------------------<wbr>------------------------------<wbr>--<br>
open import Function using (_∘_; _$_)<br>
open import Relation.Binary.<wbr>PropositionalEquality using (_≡_; cong)<br>
open import Data.Nat            using (ℕ; suc; _+_; _∸_)<br>
open import Data.Nat.Properties using (+-comm)<br>
<br>
a : ℕ<br>
a = 12345<br>
<br>
test1 :  ∀ n → (a + n) ∸ a ≡ (n + a) ∸ a<br>
test1 n =  cong (_∸ a) (+-comm a n)<br>
<br>
test2 :  ∀ n → suc ((a + n) ∸ a) ≡ suc ((n + a) ∸ a)<br>
test2 n =  cong (suc ∘ (_∸ a)) (+-comm a n)<br>
<br>
           -- cong suc (test1 n)<br>
------------------------------<wbr>------------------------------<wbr>---<br>
<br>
The interactive type-checker highlights the expression<br>
                     cong (suc ∘ (_∸ a)) (+-comm a n)<br>
<br>
and hangs for a long time.<br>
<br>
Also  test2  type-checks fast if it is implemented as<br>
cong suc (test1 n).<br>
<br>
I can type-check the whole program with, say,  a = 7.<br>
But for a good run-time performance `a' needs to be large<br>
(and it relies on that the run-time arithmetic is built-in).<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>