[Agda] help avoiding space leak using strict evaluation

[Sergei Meshveliani]

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