[Agda] type check with large constant

[Sergei Meshveliani]

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

[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

Post by Sergei Meshveliani
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
https://lists.chalmers.se/mailman/listinfo/agda

[Sergei Meshveliani]

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

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.

Post by Ulf Norell
I would advise abstracting over `a` whenever you can.

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

------
Sergei

Post by Ulf Norell
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
https://lists.chalmers.se/mailman/listinfo/agda

[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

Post by Sergei Meshveliani

Post by 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 `_∞_`.

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.

Post by Ulf Norell
I would advise abstracting over `a` whenever you can.

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

Post by Ulf Norell
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
https://lists.chalmers.se/mailman/listinfo/agda