[Agda] help avoiding space leak using strict evaluation

[Ulf Norell]

Absolutely it will help. Using a strict foldl your example runs without
performance problems:

open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Data.List
open import Data.Nat  using (ℕ; suc; _+_; _∸_; _*_)

open import Agda.Builtin.Strict

comb : ℕ → ℕ → ℕ
comb a x =  suc ((a + x) ∸ a)

foldl' : ∀ {a b} {A : Set a} {B : Set b} → (A → B → A) → A → List B → A
foldl' c n []       = n
foldl' c n (x ∷ xs) = primForce (c n x) λ n₁ → foldl' c n₁ xs

test' : ℕ → ℕ
test' n = foldl' comb 0 (replicate n 1)

{-      n  time
     1000   16ms
    10000  140ms
   100000   1.4s
-}

/ Ulf

On Tue, Sep 6, 2016 at 11:22 AM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> On Sun, 2016-09-04 at 07:59 +0200, Ulf Norell wrote:
> > 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))) ->
> > ...
> > []
>
>
> By the way, has it sense to use this  primForce  for increasing
> performance of type checking in some examples?
> For example, consider the following known example which yields an
> exponential cost growth of type checking:
>
> ------------------------------------------------------------------------
> open import Relation.Binary.PropositionalEquality as PE using (_≡_)
> open import Data.List using (replicate; foldl)
> open import Data.Nat  using (ℕ; suc; _+_; _∸_; _*_)
>
> comb : ℕ → ℕ → ℕ
> comb a x =  suc ((a + x) ∸ a)
>
> test : ℕ → ℕ
> test n = foldl comb 0 (replicate n 1)
>
> lemma : test 3 ≡ 2
> lemma = PE.refl
>
> -- lemma2 : 12 * 20 ≡ 240
> -- lemma2 = PE.refl
> {- n    time [sec]
>    18    4
>    19    6
>    20   12
>    21   22
> -}
> ------------------------------------------------------------------------
>
>
> Will the strictness annotation help?
>
> My current DoCon-A library for algebra needs 12 Gb memory to type-check
> in 1 hour. May setting  primForce  help this?
>
> Thanks,
>
> ------
> Sergei
>
>
> >
> > / 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).
> >
> >         --
> >
> >
> >         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
> >
> >
> >
> > _______________________________________________
> > 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/20160906/a8681972/attachment.html