[Agda] evaluation in compilation

[Andreas Abel]

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/