[Agda] foldr _+_ vs foldl

[Guillaume Brunerie]

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