[Agda] foldr _+_ vs foldl

[Sergei Meshveliani]

Apostolis Xekoukoulotakis apostolis.xekoukoulotakis at gmail.com 
writes

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


1. Haskell is a language. Do you mean the Glasgow Haskell tool? 

2. Do you mean 3 times faster than lazy Agda compiled to Haskell and run by ghc ? 

3. Do you mean this concrete example of summing rationals?
   Its cost depends mainly on which _built-in_ thing is used for arithmetic of large integers,
   this has nothing to do with the choice of any high-level language.
  
4. If you need to compare the GHC performance with your agda-ocaml, probably is more appropriate 
   to compare them on implementing, say, a parser for the Agda syntax, or maybe,
   various parts of the type checker for Agda, to see how much the type check costs.

5. Strict evaluation is a different world. Lazy computation allows us to write a simpler code.
   If you write all your applications in assembly, they will most probably be several times 
   faster further.  

Regards,

------
Sergei