[Agda] laziness damaged

[Jeffrey, Alan S A (Alan)]

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).

The JS back end is strict, and will probably perform even more poorly than the MAlonzo back end.

A.
________________________________________
From: agda-bounces at lists.chalmers.se [agda-bounces at lists.chalmers.se] on behalf of Serge D. Mechveliani [mechvel at botik.ru]
Sent: Wednesday, October 17, 2012 6:50 AM
To: agda at lists.chalmers.se
Subject: [Agda] laziness damaged

People,

The issue 716 on the Bug Tracker includes an archive with an
implementation for sorting functions  orderList-easy  and  orderList
for the `merge' method (O(n*log(n))
(see the comments on the Tracker).
The result of  orderList  is a record including a proof for orderedness
of the result list.
The function `main' applies  orderList  to certain long list and prints
out  [head ys, last ys]  for the result  ys
-- without using the proof part.
Still the cost of this computation is 6 times more than in the case of
orderList-easy
(for  Agda-2.3.0.1 + MAlonzo + lib-0.6).

Nils Anders writes there in `comments'

> This can certainly take extra time (and space) if the compiler isn't
> smart enough to erase the proofs (and MAlonzo isn't).


Dear Agda developers,
please, pay attention to this point of laziness.

Agda is said _lazy_.
The developers even said "it is too lazy at the moment".
And now, it occurs  too strict at the moment.

For example, Haskell laziness would not allow this factor of 6 (in GHC)
-- in many cases (though, it depends on the code details).
Consider a function for division of naturals with remainder, returning
a pair  (quot , rem),  where both parts are recursively accumulated in
the program. And consider a client function
                            f n m = let (_, r) = quotRem n m in  r^2

For any reasonably programmed  quotRem,  f  will save the cost related
to accumulation of  quot.  This is by laziness.
One needs to use all the benefits of laziness.
This is very important for practice, mathematical methods are full with
such examples.

May be, Agda has some profound reason for being strict in this particular
case and point?  What about the example of quotRem ?
What is with other Agda compilers?

Thanks,
Sergei






_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda