<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) -&gt;</div><div>fooBy 999 $! foo (suc zero) -&gt;</div><div>fooBy 999 (suc (id zero)) -&gt;</div><div>fooBy 998 $! foo (suc (id zero)) -&gt;</div><div>fooBy 998 (suc (id (id zero))) -&gt;</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">&lt;<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a>&gt;</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&#39;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&#39; : Set where<br>
        zero : Nat&#39;<br>
        suc : Nat&#39; → Nat&#39;<br>
      <br>
      foo : Nat&#39; → Nat&#39;<br>
      foo zero = zero<br>
      foo (suc b) = suc (id b)<br>
      <br>
      fooBy : Nat → Nat&#39; → Nat&#39;<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>