[Agda] foldr _+_ vs foldl

[Sergei Meshveliani]

I thank people for their comments.


On Thu, 2019-03-28 at 14:22 +0100, Guillaume Brunerie wrote:
> Hi Sergei,
> 
> With foldl, you make Agda compute (…(1 + 1/2) + …) + 1/29) + 1/30)
> (associated to the left), whereas with foldr you make Agda compute (1
> + (1/2 + … + (1/29 + 1/30)…) (associated to the right).
> I think it makes sense that the second one is slower because the
> denominators of the intermediate results grow much faster since the
> beginning, compared to the first one : 1/28 + (1/29 + 1/30) has a
> bigger denominator than ((1 + 1/2) + 1/3).
> [..]


I agree. 
foldl op b (reverse xs)  may have a greatly different cost than 
foldl op b xs.

In the example considered, it is cheaper to start with additions that
produce a smaller denominator. Because the size of the currently
obtained denominator effects the cost of all the further additions. 

This consideration does not depend on the choice of programming system.
Then, we need to think of how to make a particular compiler to arrange
addition in the needed order.    
 
Thanks,

-----
Segei



> Even though in the end you get the same result, the intermediate
> calculations are more complicated in the case of foldr than in the
> case of foldl.
> 
> Best,
> Guillaume
> 
> Den tors 28 mars 2019 kl 14:14 skrev Sergei Meshveliani <mechvel at botik.ru>:
> >
> > 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
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
>