[Agda] type check with large constant

[Ulf Norell]

I did mean `n`, which is a free variable of the term `(a + n) ∸ a`.
Built-in arithmetic
can only do its thing if all arguments to the built-in function are
constants, but in this
case `n` is an argument to the function and its value is not fixed at type
checking time.

/ Ulf

On Mon, Feb 12, 2018 at 4:57 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> 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
> >
> >
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180212/6de89062/attachment.html>