[Agda] type check with large constant

[Ulf Norell]

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 `_∸_`.

I would advise abstracting over `a` whenever you can.

/ Ulf

On Sat, Feb 10, 2018 at 2:45 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> Dear all,
>
> I need to type-check a program that uses a certain large global constant
> a.
> And the function  test2  below is type-checked much longer than  test1,
> It takes too long.
> This is  Agda 2.5.3.
>
> Can people, please, explain the effect?
>
> --------------------------------------------------------------
> open import Function using (_∘_; _$_)
> open import Relation.Binary.PropositionalEquality using (_≡_; cong)
> open import Data.Nat            using (ℕ; suc; _+_; _∸_)
> open import Data.Nat.Properties using (+-comm)
>
> a : ℕ
> a = 12345
>
> test1 :  ∀ n → (a + n) ∸ a ≡ (n + a) ∸ a
> test1 n =  cong (_∸ a) (+-comm a n)
>
> test2 :  ∀ n → suc ((a + n) ∸ a) ≡ suc ((n + a) ∸ a)
> test2 n =  cong (suc ∘ (_∸ a)) (+-comm a n)
>
>            -- cong suc (test1 n)
> ---------------------------------------------------------------
>
> The interactive type-checker highlights the expression
>                      cong (suc ∘ (_∸ a)) (+-comm a n)
>
> and hangs for a long time.
>
> Also  test2  type-checks fast if it is implemented as
> cong suc (test1 n).
>
> I can type-check the whole program with, say,  a = 7.
> But for a good run-time performance `a' needs to be large
> (and it relies on that the run-time arithmetic is built-in).
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180212/cb050aad/attachment.html>