[Agda] foldr _+_ vs foldl

[Apostolis Xekoukoulotakis]

I do not know why it is faster , only that it is. It is using optimizations
that others have done, the ocaml community, not me.

( I forgot to add the agda list to the email recepients, doing it now).

On Fri, Mar 29, 2019 at 5:37 PM Sergei Meshveliani <mechvel at botik.ru> wrote:

>
> Also as  agda-ocaml  is strict, it has sense to compare it to Idris and
> Coq.
>
>
>
> On Fri, 2019-03-29 at 15:54 +0200, Apostolis Xekoukoulotakis wrote:
> >
> >
> >
> > On Fri, Mar 29, 2019 at 1:35 PM Sergei Meshveliani <mechvel at botik.ru>
> > wrote:
> >
> >         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 ?
> >
> > Yes, agda-ocaml is a backend , like MAlonzo and the javascript ones.
> >
> >
> >         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.
> >
> >
> > The reason for the computational cost here is probably due to what the
> > others said.
> >
> > I compiled a program about foldr / foldl with naturals instead of
> > Rationals, and it is 3 times faster
> >
> > than the ghc backend.
> >
> >
> >
> > I use the zarith library to represent big integers, and naturals :
> >
> > https://github.com/ocaml/Zarith
> >
> >
> >
> >         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.
> >
> >
> >
> > Because , agda is a total language, you can use either strict
> > evaluation or lazy evaluation on the same agda code.
> >
> >
> > With strict evaluation and with agda-ocaml, one needs to simply
> > increase the limits of the stack to a big number so
> > that it does not stack overflow.
> >
> >
> >         Regards,
> >
> >         ------
> >         Sergei
> >
> >
> >
> >
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190329/79a316b2/attachment.html>