<div dir="ltr">Absolutely it will help. Using a strict foldl your example runs without performance problems:<div><br></div><div><div>open import Relation.Binary.PropositionalEquality as PE using (_≡_)</div><div>open import Data.List</div><div>open import Data.Nat  using (ℕ; suc; _+_; _∸_; _*_)</div><div><br></div><div>open import Agda.Builtin.Strict</div><div><br></div><div>comb : ℕ → ℕ → ℕ</div><div>comb a x =  suc ((a + x) ∸ a)</div><div><br></div><div>foldl&#39; : ∀ {a b} {A : Set a} {B : Set b} → (A → B → A) → A → List B → A</div><div>foldl&#39; c n []       = n</div><div>foldl&#39; c n (x ∷ xs) = primForce (c n x) λ n₁ → foldl&#39; c n₁ xs</div><div><br></div><div>test&#39; : ℕ → ℕ</div><div>test&#39; n = foldl&#39; comb 0 (replicate n 1)</div><div><br></div><div>{-      n  time</div><div>     1000   16ms</div><div>    10000  140ms</div><div>   100000   1.4s</div><div>-}</div></div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Sep 6, 2016 at 11:22 AM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Sun, 2016-09-04 at 07:59 +0200, Ulf Norell wrote:<br>
&gt; The key thing to remember is that _$!_ only evaluates the argument<br>
&gt; to weak head normal form (just like in Haskell). You can step through<br>
&gt; this by hand to see where the space leak is:<br>
&gt;<br>
&gt;<br>
&gt; fooBy 1000 (suc zero) -&gt;<br>
&gt; fooBy 999 $! foo (suc zero) -&gt;<br>
&gt; fooBy 999 (suc (id zero)) -&gt;<br>
&gt; fooBy 998 $! foo (suc (id zero)) -&gt;<br>
&gt; fooBy 998 (suc (id (id zero))) -&gt;<br>
&gt; ...<br>
</span>&gt; []<br>
<br>
<br>
By the way, has it sense to use this  primForce  for increasing<br>
performance of type checking in some examples?<br>
For example, consider the following known example which yields an<br>
exponential cost growth of type checking:<br>
<br>
------------------------------<wbr>------------------------------<wbr>------------<br>
open import Relation.Binary.<wbr>PropositionalEquality as PE using (_≡_)<br>
open import Data.List using (replicate; foldl)<br>
open import Data.Nat  using (ℕ; suc; _+_; _∸_; _*_)<br>
<br>
comb : ℕ → ℕ → ℕ<br>
comb a x =  suc ((a + x) ∸ a)<br>
<br>
test : ℕ → ℕ<br>
test n = foldl comb 0 (replicate n 1)<br>
<br>
lemma : test 3 ≡ 2<br>
lemma = PE.refl<br>
<br>
-- lemma2 : 12 * 20 ≡ 240<br>
-- lemma2 = PE.refl<br>
{- n    time [sec]<br>
   18    4<br>
   19    6<br>
   20   12<br>
   21   22<br>
-}<br>
------------------------------<wbr>------------------------------<wbr>------------<br>
<br>
<br>
Will the strictness annotation help?<br>
<br>
My current DoCon-A library for algebra needs 12 Gb memory to type-check<br>
in 1 hour. May setting  primForce  help this?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
&gt;<br>
&gt; / Ulf<br>
&gt;<br>
&gt; On Sat, Sep 3, 2016 at 1:33 AM, Martin Stone Davis<br>
&gt; &lt;<a href="mailto:martin.stone.davis@gmail.com">martin.stone.davis@gmail.com</a>&gt; wrote:<br>
&gt;         I&#39;m trying to use strict evaluation to avoid getting a space<br>
&gt;         leak but my attempt fails: the below code blows-up the memory.<br>
&gt;         (This question is a follow-up to a discussion in agda issue<br>
&gt;         #2161).<br>
&gt;<br>
&gt;         --<br>
&gt;<br>
&gt;<br>
&gt;         open import Agda.Builtin.Strict<br>
&gt;<br>
&gt;         infixr 0 _$!_<br>
&gt;         _$!_ : ∀ {a b} {A : Set a} {B : A → Set b} → (∀ x → B x) → ∀ x<br>
&gt;         → B x<br>
&gt;         f $! x = primForce x f<br>
&gt;<br>
&gt;         open import Agda.Builtin.Nat<br>
&gt;              using (zero; suc; Nat)<br>
&gt;         open import Agda.Builtin.Equality<br>
&gt;              using (_≡_; refl)<br>
&gt;<br>
&gt;         id : {A : Set} → A → A<br>
&gt;         id x = x<br>
&gt;<br>
&gt;         data Nat&#39; : Set where<br>
&gt;           zero : Nat&#39;<br>
&gt;           suc : Nat&#39; → Nat&#39;<br>
&gt;<br>
&gt;         foo : Nat&#39; → Nat&#39;<br>
&gt;         foo zero = zero<br>
&gt;         foo (suc b) = suc (id b)<br>
&gt;<br>
&gt;         fooBy : Nat → Nat&#39; → Nat&#39;<br>
&gt;         fooBy zero x = x<br>
&gt;         fooBy (suc n) x = fooBy n $! foo x<br>
&gt;<br>
&gt;         test : fooBy 10000000 (suc zero) ≡ suc zero<br>
&gt;         test = refl<br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt;         ______________________________<wbr>_________________<br>
&gt;         Agda mailing list<br>
&gt;         <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt;         <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt; ______________________________<wbr>_________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br>
<br>
</div></div></blockquote></div><br></div>