<div dir="ltr"><div>Just letting you know, that xekoukou/agda-ocaml is 3 times faster than haskell (and on ocassions much faster)</div><div>It simply requires some love from the community. ( I have no time to work on it, for the moment.)</div><div><br></div><div>It is also strict, so you could check if the problem is strict evaluation or not.<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Mar 28, 2019 at 3:22 PM Guillaume Brunerie <<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi Sergei,<br>
<br>
With foldl, you make Agda compute (…(1 + 1/2) + …) + 1/29) + 1/30)<br>
(associated to the left), whereas with foldr you make Agda compute (1<br>
+ (1/2 + … + (1/29 + 1/30)…) (associated to the right).<br>
I think it makes sense that the second one is slower because the<br>
denominators of the intermediate results grow much faster since the<br>
beginning, compared to the first one : 1/28 + (1/29 + 1/30) has a<br>
bigger denominator than ((1 + 1/2) + 1/3).<br>
Even though in the end you get the same result, the intermediate<br>
calculations are more complicated in the case of foldr than in the<br>
case of foldl.<br>
<br>
Best,<br>
Guillaume<br>
<br>
Den tors 28 mars 2019 kl 14:14 skrev Sergei Meshveliani <<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>>:<br>
><br>
> People,<br>
><br>
> I run<br>
>   sum : List Fraction → Fraction<br>
>   sum = foldl _+fr_ 0fr<br>
><br>
> to sum a list  [1/m | (m : Integer) <- [1 .. 30]]<br>
><br>
> of fractions, where _+fr_ is my home-made generic fraction addition.<br>
> This example is expensive to run because the intermediate denominators<br>
> grow somewhat like m!.<br>
><br>
> But what is remarkable: changing foldl to foldr makes it slower 15<br>
> times.<br>
> What is the source of this slowing down?<br>
><br>
> I expect that only about 30 calls of _+fr_ or foldr(l) are put to stack<br>
> in the worst case, and the stack occurs large because some of these<br>
> calls contain large data inside.<br>
> Then, it remains to find out how laziness relates to foldl and foldr in<br>
> Agda, what MAlonzo makes of it, and how it is treated in GHC.<br>
> (GHC has a certain strictness analysis ...<br>
> and I recall that in GHC foldr was more lucky on average than foldl).<br>
><br>
> What people would tell about this?<br>
><br>
> Thanks,<br>
><br>
> ------<br>
> Sergei<br>
><br>
><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>