[Agda] help avoiding space leak using strict evaluation

[Ulf Norell]

The key thing to remember is that _$!_ only evaluates the argument
to weak head normal form (just like in Haskell). You can step through
this by hand to see where the space leak is:

fooBy 1000 (suc zero) ->
fooBy 999 $! foo (suc zero) ->
fooBy 999 (suc (id zero)) ->
fooBy 998 $! foo (suc (id zero)) ->
fooBy 998 (suc (id (id zero))) ->
...

/ Ulf

On Sat, Sep 3, 2016 at 1:33 AM, Martin Stone Davis <
martin.stone.davis at gmail.com> wrote:

> 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 agda issue #2161
> <https://github.com/agda/agda/issues/2161>).
>
> --
>
> open import Agda.Builtin.Strict
>
> infixr 0 _$!_
> _$!_ : ∀ {a b} {A : Set a} {B : A → Set b} → (∀ x → B x) → ∀ x → B x
> f $! x = primForce x f
>
> open import Agda.Builtin.Nat
>      using (zero; suc; Nat)
> open import Agda.Builtin.Equality
>      using (_≡_; refl)
>
> id : {A : Set} → A → A
> id x = x
>
> data Nat' : Set where
>   zero : Nat'
>   suc : Nat' → Nat'
>
> foo : Nat' → Nat'
> foo zero = zero
> foo (suc b) = suc (id b)
>
> fooBy : Nat → Nat' → Nat'
> fooBy zero x = x
> fooBy (suc n) x = fooBy n $! foo x
>
> test : fooBy 10000000 (suc zero) ≡ suc zero
> test = refl
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160904/eb6d8ee6/attachment.html