[Agda] tweaking evaluation

[Ulf Norell]

There's nothing you can do at the moment for the polymorphic diagonal
function,
but pattern matching makes things strict, so you could do something like

strictNat : {A : Set} → ℕ → (ℕ → A) → A
strictNat zero    f = f zero
strictNat (suc n) f = f (suc n)

notslower : strictNat (2 ^ 13 * 0) Δ ≡ Δ 0
notslower = refl

/ Ulf

On Tue, Aug 11, 2015 at 5:30 PM, Peter Selinger <selinger at mathstat.dal.ca>
wrote:

> This may be a newbie question. I have a program whose type-checking
> requires the evaluation of some moderately large terms. The fact that
> Agda uses normal order (or call-by-name) evaluation makes the
> evaluations very slow. Is there a way to force certain terms to be
> evaluated to normal form?
>
> Here's a toy example (adapted from
>
> http://stackoverflow.com/questions/21210569/is-the-evaluation-strategy-of-agda-specified-anywhere
> ):
>
>   open import Data.Product
>   open import Relation.Binary.PropositionalEquality
>
>   -- using a unary implementation of ℕ for illustration purposes.
>   data ℕ : Set where
>     zero : ℕ
>     suc  : ℕ → ℕ
>
>   {-# BUILTIN NATURAL ℕ #-}
>
>   infixl 4 _+_
>   infixl 5 _*_
>   infixr 6 _^_
>
>   _+_ : (m n : ℕ) → ℕ
>   zero  + n = n
>   suc m + n = suc (m + n)
>
>   _*_ : (m n : ℕ) → ℕ
>   zero  * n = zero
>   suc m * n = n + m * n
>
>   _^_ : (m n : ℕ) → ℕ
>   m ^ zero = suc zero
>   m ^ suc n = m * m ^ n
>
>   -- naive diagonal function
>   Δ : {A : Set} -> A -> A × A
>   Δ x = (x , x)
>
>   -- checking takes about 11 seconds
>   slow : 2 ^ 13 * 0 ≡ 0
>   slow = refl
>
>   -- takes about 22 seconds
>   slower : Δ (2 ^ 13 * 0) ≡ Δ 0
>   slower = refl
>
> Naturally, "slower" takes about twice as long to type-check than
> "slow".
>
> It is stated here that using "with" on an expression causes the
> expression to be evaluated to normal form:
> https://lists.chalmers.se/pipermail/agda/2012/004443.html
>
> Therefore, I figured the following could be a way to speed up the
> diagonal function:
>
>   -- better diagonal function?
>   Δ' : {A : Set} -> A -> A × A
>   Δ' x with x
>   Δ' x | y = (y , y)
>
> However, this doesn't work at all, as the result still takes 22
> seconds to evaluate:
>
>   -- takes about 22 seconds
>   slower' : Δ' (2 ^ 13 * 0) ≡ Δ' 0
>   slower' = refl
>
> Is there a way to force some term to be evaluated strictly?
>
> Thanks, -- Peter
>
> _______________________________________________
> 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/20150812/b0ab331c/attachment.html