[Agda] foldr _+_ vs foldl

Sergei Meshveliani mechvel at botik.ru
Thu Mar 28 13:36:15 CET 2019


People,

I run 
  sum : List Fraction → Fraction
  sum = foldl _+fr_ 0fr  

to sum a list  [1/m | (m : Integer) <- [1 .. 30]]  

of fractions, where _+fr_ is my home-made generic fraction addition.
This example is expensive to run because the intermediate denominators
grow somewhat like m!.

But what is remarkable: changing foldl to foldr makes it slower 15
times.
What is the source of this slowing down?

I expect that only about 30 calls of _+fr_ or foldr(l) are put to stack
in the worst case, and the stack occurs large because some of these
calls contain large data inside.
Then, it remains to find out how laziness relates to foldl and foldr in 
Agda, what MAlonzo makes of it, and how it is treated in GHC.
(GHC has a certain strictness analysis ...
and I recall that in GHC foldr was more lucky on average than foldl).

What people would tell about this?

Thanks,

------
Sergei 
 



More information about the Agda mailing list