[Agda] evaluation in compilation

[Andreas Abel]

I added this to the bug tracker...

   http://code.google.com/p/agda/issues/detail?id=704

On 03.10.12 1:47 AM, Andreas Abel wrote:
> When I try to load your example, I get a "stack overflow".  So it is not
> a problem of the compiler, but already type checking fails.
>
> I found the problem:
>
>  > zs = merge xs ys
>  >
>  > hl : List Nat
>  > hl   with zs
>
> If you "with" an expression, like "zs" here, it is normalized.  This
> means that Agda has to compute the list of length 16000, with (in this
> case possibly inefficient) call-by-name evaluation strategy.
>
> That can well blow the Agda type checker.
>
> It is advisable to avoid "with" in this case.
>
> -- this works
> bla : List ℕ → List ℕ
> bla [] = []
> bla (z ∷ zs') =  z ∷ (last $ fromL z zs') ∷ []
>
> hl = bla zs
>
> main : IO Unit
> main = putStrLn (toCostring $ showNatList hl)
>
> Or use "case" from the std-lib.
>
> Cheers,
> Andreas
>
>
>   Skipping Prelude
> (/Users/abel/public_html/repos/AgdaPrelude/src/Prelude.agdai).
> Stack space overflow: current size 8388608 bytes.
> Use `+RTS -Ksize -RTS' to increase it.
>     7,195,923,960 bytes allocated in the heap
>     1,737,295,060 bytes copied during GC
>       285,621,572 bytes maximum residency (14 sample(s))
>        21,748,488 bytes maximum slop
>               707 MB total memory in use (0 MB lost due to fragmentation)
>
>    Generation 0: 13317 collections,     0 parallel, 48.47s, 49.44s elapsed
>    Generation 1:    14 collections,     0 parallel,  3.11s,  5.09s elapsed
>
>    INIT  time    0.00s  (  0.08s elapsed)
>    MUT   time   22.88s  ( 25.11s elapsed)
>    GC    time   51.58s  ( 54.54s elapsed)
>    EXIT  time    0.00s  (  0.00s elapsed)
>    Total time   74.46s  ( 79.72s elapsed)
>
>    %GC time      69.3%  (68.4% elapsed)
>
>    Alloc rate    314,514,602 bytes per MUT second
>
>    Productivity  30.7% of total user, 28.7% of total elapsed
>
>
>
> On 01.10.12 6:51 PM, Serge D. Mechveliani wrote:
>> module Main where
>> open import Foreign.Haskell
>> open import IO.Primitive
>> open import Relation.Nullary
>> open import Function using ( _$_ )
>> open import Data.Nat as Nat
>> open import Data.Nat.Show
>> open import Data.List as List
>> open import Data.List.NonEmpty renaming ( fromList to fromL )
>> open import Data.String renaming ( _++_ to _Str++_ )
>> open import Prelude using ( toCostring )             -- by F. Kettelhoit
>>
>> showNatList : List Nat -> String
>> showNatList xs = "[" Str++ (showL xs) Str++ "]"
>>    where
>>    showL : List Nat -> String
>>    showL []        = ""
>>    showL (x :: []) = show x
>>    showL (x :: xs) = (show x) Str++ "," Str++ showL xs
>>
>> merge : List Nat -> List Nat -> List Nat
>> merge []        ys        =  ys
>> merge xs        []        =  xs
>> merge (x :: xs) (y :: ys)  with
>>                         x <=? y | merge xs (y :: ys) | merge (x :: xs) ys
>> ...                  | yes _ | zs | _  =  x :: zs
>> ...                  | _     | _  | zs =  y :: zs
>>
>> concatCopies : {A : Set} -> Nat -> List A -> List A
>> concatCopies 0       xs =  []
>> concatCopies (suc n) xs =  xs ++ (concatCopies n xs)
>>
>> xs0 : List Nat
>> xs0 = 1 :: 3 :: 4 :: 6 :: []
>>
>> n : Nat
>> n = 16000  -- 32000
>>
>> xs = concatCopies n xs0
>> ys = concatCopies n $ List.reverse xs0
>> zs : List Nat
>> zs = merge xs ys
>>
>> hl : List Nat
>> hl   with zs
>> ... | z :: zs' =  z :: (last $ fromL z zs') :: []
>> ... | _       =  []
>>
>> main : IO Unit
>> main = putStrLn (toCostring $ showNatList hl)
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/