[Agda] foldr _+_ vs foldl

[Apostolis Xekoukoulotakis]

Just letting you know, that xekoukou/agda-ocaml is 3 times faster than
haskell (and on ocassions much faster)
It simply requires some love from the community. ( I have no time to work
on it, for the moment.)

It is also strict, so you could check if the problem is strict evaluation
or not.

On Thu, Mar 28, 2019 at 3:22 PM Guillaume Brunerie <
guillaume.brunerie at gmail.com> 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).
> 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
> _______________________________________________
> 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/af6c13be/attachment.html>