[Agda] foldr _+_ vs foldl

[Ulf Norell]

I wouldn't be so quick to blame laziness and strictness analysis in this
case. Folding from the left or from the right creates very different
intermediate terms. In ghci:

λ scanl (+) 0 [ 1 / fromIntegral n | n <- [1..30] ] :: [Rational]
[0 % 1,1 % 1,3 % 2,11 % 6,25 % 12,137 % 60,49 % 20,363 % 140,761 % 280,7129
% 2520,7381 % 2520,83711 % 27720,86021 % 27720,1145993 % 360360,1171733 %
360360,1195757 % 360360,2436559 % 720720,42142223 % 12252240,14274301 %
4084080,275295799 % 77597520,55835135 % 15519504,18858053 %
5173168,19093197 % 5173168,444316699 % 118982864,1347822955 %
356948592,34052522467 % 8923714800,34395742267 % 8923714800,312536252003 %
80313433200,315404588903 % 80313433200,9227046511387 %
2329089562800,9304682830147 % 2329089562800]
λ scanr (+) 0 [ 1 / fromIntegral n | n <- [1..30] ] :: [Rational]
[9304682830147 % 2329089562800,6975593267347 % 2329089562800,5811048485947
% 2329089562800,5034685298347 % 2329089562800,4452412907647 %
2329089562800,3986594995087 % 2329089562800,3598413401287 %
2329089562800,3265686320887 % 2329089562800,2974550125537 %
2329089562800,2715762396337 % 2329089562800,2482853440057 %
2329089562800,2271118025257 % 2329089562800,2077027228357 %
2329089562800,1897866492757 % 2329089562800,247357564651 %
332727080400,225175759291 % 332727080400,102190158383 %
166363540200,5435533399 % 9786090600,4891861699 % 9786090600,230358121 %
515057400,204605251 % 515057400,1260550957 % 3605401800,99697187 %
327763800,3715069 % 14250600,1560647 % 7125300,255127 % 1425060,15409 %
109620,1261 % 12180,59 % 870,1 % 30,0 % 1]

/ Ulf


On Thu, Mar 28, 2019 at 2:14 PM Sergei Meshveliani <mechvel at botik.ru> wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190328/e882e7f1/attachment.html>