[Agda] type check with large constant

[Sergei Meshveliani]

On Mon, 2018-02-12 at 08:18 +0100, Ulf Norell wrote:
> 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 `_∸_`.


Did you mean `a' being free there rather than `n' ?

As to `a', it is a constant, it is substituted with 12345, at some
stage. I do not know of whether this occurrence is qualified as free.
 
> I would advise abstracting over `a` whenever you can.

Thank you for your note. I shall think about this.

------
Sergei



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