<div dir="ltr">There&#39;s nothing you can do at the moment for the polymorphic diagonal function,<div>but pattern matching makes things strict, so you could do something like</div><div><br></div><div><div>strictNat : {A : Set} → ℕ → (ℕ → A) → A</div><div>strictNat zero    f = f zero</div><div>strictNat (suc n) f = f (suc n)</div><div><br></div><div>notslower : strictNat (2 ^ 13 * 0) Δ ≡ Δ 0</div><div>notslower = refl</div></div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Aug 11, 2015 at 5:30 PM, Peter Selinger <span dir="ltr">&lt;<a href="mailto:selinger@mathstat.dal.ca" target="_blank">selinger@mathstat.dal.ca</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">This may be a newbie question. I have a program whose type-checking<br>
requires the evaluation of some moderately large terms. The fact that<br>
Agda uses normal order (or call-by-name) evaluation makes the<br>
evaluations very slow. Is there a way to force certain terms to be<br>
evaluated to normal form?<br>
<br>
Here&#39;s a toy example (adapted from<br>
<a href="http://stackoverflow.com/questions/21210569/is-the-evaluation-strategy-of-agda-specified-anywhere" rel="noreferrer" target="_blank">http://stackoverflow.com/questions/21210569/is-the-evaluation-strategy-of-agda-specified-anywhere</a>):<br>
<br>
  open import Data.Product<br>
  open import Relation.Binary.PropositionalEquality<br>
<br>
  -- using a unary implementation of ℕ for illustration purposes.<br>
  data ℕ : Set where<br>
    zero : ℕ<br>
    suc  : ℕ → ℕ<br>
<br>
  {-# BUILTIN NATURAL ℕ #-}<br>
<br>
  infixl 4 _+_<br>
  infixl 5 _*_<br>
  infixr 6 _^_<br>
<br>
  _+_ : (m n : ℕ) → ℕ<br>
  zero  + n = n<br>
  suc m + n = suc (m + n)<br>
<br>
  _*_ : (m n : ℕ) → ℕ<br>
  zero  * n = zero<br>
  suc m * n = n + m * n<br>
<br>
  _^_ : (m n : ℕ) → ℕ<br>
  m ^ zero = suc zero<br>
  m ^ suc n = m * m ^ n<br>
<br>
  -- naive diagonal function<br>
  Δ : {A : Set} -&gt; A -&gt; A × A<br>
  Δ x = (x , x)<br>
<br>
  -- checking takes about 11 seconds<br>
  slow : 2 ^ 13 * 0 ≡ 0<br>
  slow = refl<br>
<br>
  -- takes about 22 seconds<br>
  slower : Δ (2 ^ 13 * 0) ≡ Δ 0<br>
  slower = refl<br>
<br>
Naturally, &quot;slower&quot; takes about twice as long to type-check than<br>
&quot;slow&quot;.<br>
<br>
It is stated here that using &quot;with&quot; on an expression causes the<br>
expression to be evaluated to normal form:<br>
<a href="https://lists.chalmers.se/pipermail/agda/2012/004443.html" rel="noreferrer" target="_blank">https://lists.chalmers.se/pipermail/agda/2012/004443.html</a><br>
<br>
Therefore, I figured the following could be a way to speed up the<br>
diagonal function:<br>
<br>
  -- better diagonal function?<br>
  Δ&#39; : {A : Set} -&gt; A -&gt; A × A<br>
  Δ&#39; x with x<br>
  Δ&#39; x | y = (y , y)<br>
<br>
However, this doesn&#39;t work at all, as the result still takes 22<br>
seconds to evaluate:<br>
<br>
  -- takes about 22 seconds<br>
  slower&#39; : Δ&#39; (2 ^ 13 * 0) ≡ Δ&#39; 0<br>
  slower&#39; = refl<br>
<br>
Is there a way to force some term to be evaluated strictly?<br>
<br>
Thanks, -- Peter<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>