[Agda] test report

[Nils Anders Danielsson]

On 2021-03-30 01:04, mechvel at scico.botik.ru wrote:
> The run-time performance remains (it was satisfactory)
> - must it remain?

No, but if your program was fairly optimised I am not surprised that the
execution time did not change a lot. Even without the @0 annotation Agda
erases certain things, and due to lazy evaluation things that are not
erased might not be evaluated.

However, one can construct programs where the annotation makes a
difference. Try running the following program with and without the @0
annotations:

   open import Agda.Builtin.IO
   open import Agda.Builtin.Nat
   open import Agda.Builtin.Unit

   data Pair : Set where
     _,_ : Nat → @0 Nat → Pair

   f : Nat → @0 Nat → Pair
   f zero    n = zero , n
   f (suc m) n = f m (suc n)

   fst : Pair → Nat
   fst (m , _) = m

   postulate
     print : Nat → IO ⊤

   {-# COMPILE GHC print = print #-}

   main : IO ⊤
   main = print (fst (f 10000000 0))

Using "+RTS -s" I get reports like the following one with the
annotations:

       80,046,988 bytes allocated in the heap
            8,444 bytes copied during GC
           42,724 bytes maximum residency (2 sample(s))
           31,004 bytes maximum slop
                2 MiB total memory in use (0 MB lost due to fragmentation)

                                      Tot time (elapsed)  Avg pause  Max pause
   Gen  0        75 colls,     0 par    0.000s   0.000s     0.0000s    0.0000s
   Gen  1         2 colls,     0 par    0.000s   0.000s     0.0001s    0.0001s

   INIT    time    0.001s  (  0.000s elapsed)
   MUT     time    0.144s  (  0.144s elapsed)
   GC      time    0.001s  (  0.001s elapsed)
   EXIT    time    0.000s  (  0.000s elapsed)
   Total   time    0.145s  (  0.145s elapsed)

   %GC     time       0.0%  (0.0% elapsed)

   Alloc rate    557,463,190 bytes per MUT second

   Productivity  99.2% of total user, 99.2% of total elapsed

And reports like the following one without the annotations (presumably
because f's second argument becomes a larger and larger thunk as the
computation progresses):

      200,046,988 bytes allocated in the heap
      466,762,004 bytes copied during GC
      118,129,376 bytes maximum residency (8 sample(s))
        1,891,616 bytes maximum slop
              232 MiB total memory in use (0 MB lost due to fragmentation)

                                      Tot time (elapsed)  Avg pause  Max pause
   Gen  0       184 colls,     0 par    0.222s   0.222s     0.0012s    0.0030s
   Gen  1         8 colls,     0 par    0.506s   0.507s     0.0634s    0.2491s

   INIT    time    0.001s  (  0.001s elapsed)
   MUT     time    0.138s  (  0.138s elapsed)
   GC      time    0.728s  (  0.730s elapsed)
   EXIT    time    0.000s  (  0.000s elapsed)
   Total   time    0.866s  (  0.869s elapsed)

   %GC     time       0.0%  (0.0% elapsed)

   Alloc rate    1,447,119,322 bytes per MUT second

   Productivity  16.0% of total user, 15.9% of total elapsed

-- 
/NAD