<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' : ∀ {a b} {A : Set a} {B : Set b} → (A → B → A) → A → List B → A</div><div>foldl' c n [] = n</div><div>foldl' c n (x ∷ xs) = primForce (c n x) λ n₁ → foldl' c n₁ xs</div><div><br></div><div>test' : ℕ → ℕ</div><div>test' n = foldl' 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"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></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>
> The key thing to remember is that _$!_ only evaluates the argument<br>
> to weak head normal form (just like in Haskell). You can step through<br>
> this by hand to see where the space leak is:<br>
><br>
><br>
> fooBy 1000 (suc zero) -><br>
> fooBy 999 $! foo (suc zero) -><br>
> fooBy 999 (suc (id zero)) -><br>
> fooBy 998 $! foo (suc (id zero)) -><br>
> fooBy 998 (suc (id (id zero))) -><br>
> ...<br>
</span>> []<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>
><br>
> / Ulf<br>
><br>
> On Sat, Sep 3, 2016 at 1:33 AM, Martin Stone Davis<br>
> <<a href="mailto:martin.stone.davis@gmail.com">martin.stone.davis@gmail.com</a>> wrote:<br>
> I'm trying to use strict evaluation to avoid getting a space<br>
> leak but my attempt fails: the below code blows-up the memory.<br>
> (This question is a follow-up to a discussion in agda issue<br>
> #2161).<br>
><br>
> --<br>
><br>
><br>
> open import Agda.Builtin.Strict<br>
><br>
> infixr 0 _$!_<br>
> _$!_ : ∀ {a b} {A : Set a} {B : A → Set b} → (∀ x → B x) → ∀ x<br>
> → B x<br>
> f $! x = primForce x f<br>
><br>
> open import Agda.Builtin.Nat<br>
> using (zero; suc; Nat)<br>
> open import Agda.Builtin.Equality<br>
> using (_≡_; refl)<br>
><br>
> id : {A : Set} → A → A<br>
> id x = x<br>
><br>
> data Nat' : Set where<br>
> zero : Nat'<br>
> suc : Nat' → Nat'<br>
><br>
> foo : Nat' → Nat'<br>
> foo zero = zero<br>
> foo (suc b) = suc (id b)<br>
><br>
> fooBy : Nat → Nat' → Nat'<br>
> fooBy zero x = x<br>
> fooBy (suc n) x = fooBy n $! foo x<br>
><br>
> test : fooBy 10000000 (suc zero) ≡ suc zero<br>
> test = refl<br>
><br>
><br>
><br>
><br>
><br>
> ______________________________<wbr>_________________<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/<wbr>mailman/listinfo/agda</a><br>
><br>
><br>
><br>
> ______________________________<wbr>_________________<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/<wbr>mailman/listinfo/agda</a><br>
<br>
<br>
</div></div></blockquote></div><br></div>