<div dir="ltr"><div>The key thing to remember is that _$!_ only evaluates the argument</div><div>to weak head normal form (just like in Haskell). You can step through</div><div>this by hand to see where the space leak is:</div><div><br></div><div>fooBy 1000 (suc zero) -></div><div>fooBy 999 $! foo (suc zero) -></div><div>fooBy 999 (suc (id zero)) -></div><div>fooBy 998 $! foo (suc (id zero)) -></div><div>fooBy 998 (suc (id (id zero))) -></div><div>...</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Sep 3, 2016 at 1:33 AM, Martin Stone Davis <span dir="ltr"><<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div text="#000000" bgcolor="#FFFFFF">
<p>I'm trying to use strict evaluation to avoid getting a space leak
but my attempt fails: the below code blows-up the memory. (This
question is a follow-up to a discussion in <a href="https://github.com/agda/agda/issues/2161" target="_blank">agda issue #2161</a>).</p>
<p>--<br>
</p>
<p>open import Agda.Builtin.Strict<br>
<br>
infixr 0 _$!_<br>
_$!_ : ∀ {a b} {A : Set a} {B : A → Set b} → (∀ x → B x) → ∀ x → 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>
</p>
</div>
<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></blockquote></div><br></div>