[Agda] laziness damaged

[Serge D. Mechveliani]

On Wed, Oct 17, 2012 at 01:40:31PM +0000, Jeffrey, Alan S A (Alan) wrote:
> My suspicion is that Agda is being lazy on the proof objects, but 
> unevaluated lazy objects still come with a cost. The run-time still 
> has to build thunks for each of the unevaluated proof objects, and 
> those thunks may end up being quite large (and also keeping other 
> pointers live, so the garbage collector can't do as good a job).
> 

May be.
But generally: is the laziness in this my example of the  orderList 
record usage  a matter of MAlonzo itself, or may be these laziness 
decisions are relayed onto Glasgow Haskell ?

Does the proof part break laziness in  list (orderList ...) ?
If the code contains some non-trivial dependence beween accumulating the 
list part and the proof part, then this will almost surely break 
laziness in using the result record fields, and this will be natural.

The code is not so simple (the internal part is `merge1'). I doubt. 
6 times expense factor looks great, but I am not sure that Glasgow 
Haskell will do it smaller for a similar example.
At least the code can be observed.

On the other hand, I provide now a very simple test for laziness.
And  Agda-2.3.0.1 + MAlonzo + lib-0.6  
shows on it as lazy as  Glasgow Haskell.

This example adds  (step : Bin)  to each component of a pair
(counter : Bin) times,  and prints the result  pair : Bin \times Bin.

The  counter  constant is imported from  Laziness-constants  in order
to prevent a run time normalization.

There are the three variants for `main'
  "pair"    -- print the full result `pair',
  "proj_1"  -- print (proj_1 pair),
  "accum1"  -- print the result of accum1 -- which accumulates in a 
               separate loop only the first component.

n             min M     time [sec] for large Memory
2^18           
  "pair"      13m       10.2
  "proj_1"    13m        6.2
  "accum1"     0.6m      4.7

It is visible that "proj_1" has about 2 times smaller time than "pair",
almost the same time as "accum1", but much greater in memory than
"accum1".
This latter memory expense is due to "unneeded" laziness in the part of 
(sucBin cnt) argument in  accumPair.
A completely similar result is in Glasgow Haskell.

Some math sybols are replaced in the below code:

---------------------------------------------------------------
{-# OPTIONS --no-termination-check #-} 
...
open import Laziness-constants using ( counter )

concatStr : List String -> String 
concatStr = foldr _Str++_ ""

showBit : Bit -> String
showBit zero = "0"
showBit _    = "1"
showBin : Bin -> String 
showBin = concatStr o map showBit o toBits

accumPair : Bin -> Bin \times Bin  
accumPair step =  acc 0# 0# 0#             -- add `step' `counter' times
     where
     acc : Bin -> Bin -> Bin -> Bin \times Bin  
     acc cnt m n   with  cnt Bin=?  counter
     ...         | yes _ = (m , n)
     ...         | no _  = acc (sucBin cnt) (step Bin+ m) (step Bin+ n) 
  
accum1 : Bin -> Bin 
accum1 step = acc 0# 0#  
              where
              acc : Bin -> Bin -> Bin
              acc cnt m   with  cnt Bin=? counter
              ...       | yes _ = m 
              ...       | no _  = acc (sucBin cnt) (step Bin+ m)

step = fromBits (1b :: 0b :: 1b :: [])   -- 5

resStr = (showBin $ proj_1 pair) Str++ ", " Str++ (showBin $ proj_2 pair)
         -- (showBin $ proj_1 pair)
         -- showBin $ accum1 step
         where
         pair = accumPair step

main : IO Unit
main = putStrLn $ toCostring resStr
---------------------------------------------------------------


Regards,
Sergei