<div dir="ltr"><div dir="ltr">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.<br></div><div dir="ltr"><br></div><div dir="ltr">( I forgot to add the agda list to the email recepients, doing it now).<br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Mar 29, 2019 at 5:37 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</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"><br>
Also as  agda-ocaml  is strict, it has sense to compare it to Idris and<br>
Coq.<br>
<br>
<br>
<br>
On Fri, 2019-03-29 at 15:54 +0200, Apostolis Xekoukoulotakis wrote:<br>
> <br>
> <br>
> <br>
> On Fri, Mar 29, 2019 at 1:35 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>><br>
> wrote:<br>
> <br>
>         Apostolis Xekoukoulotakis apostolis.xekoukoulotakis at<br>
>         <a href="http://gmail.com" rel="noreferrer" target="_blank">gmail.com</a> <br>
>         writes<br>
>         <br>
>         > Just letting you know, that xekoukou/agda-ocaml is 3 times<br>
>         faster than<br>
>         > haskell (and on ocassions much faster)<br>
>         > It simply requires some love from the community. ( I have no<br>
>         time to work<br>
>         > on it, for the moment.)<br>
>         ><br>
>         > It is also strict, so you could check if the problem is<br>
>         strict evaluation<br>
>         > or not.<br>
>         <br>
>         <br>
>         1. Haskell is a language. Do you mean the Glasgow Haskell<br>
>         tool? <br>
>         <br>
>         2. Do you mean 3 times faster than lazy Agda compiled to<br>
>         Haskell and run by ghc ? <br>
>         <br>
> Yes, agda-ocaml is a backend , like MAlonzo and the javascript ones.<br>
> <br>
>  <br>
>         3. Do you mean this concrete example of summing rationals?<br>
>            Its cost depends mainly on which _built-in_ thing is used<br>
>         for arithmetic of large integers,<br>
>            this has nothing to do with the choice of any high-level<br>
>         language.<br>
>         <br>
>  <br>
> The reason for the computational cost here is probably due to what the<br>
> others said.<br>
> <br>
> I compiled a program about foldr / foldl with naturals instead of<br>
> Rationals, and it is 3 times faster <br>
> <br>
> than the ghc backend. <br>
> <br>
> <br>
> <br>
> I use the zarith library to represent big integers, and naturals : <br>
> <br>
> <a href="https://github.com/ocaml/Zarith" rel="noreferrer" target="_blank">https://github.com/ocaml/Zarith</a><br>
> <br>
> <br>
> <br>
>         4. If you need to compare the GHC performance with your<br>
>         agda-ocaml, probably is more appropriate <br>
>            to compare them on implementing, say, a parser for the Agda<br>
>         syntax, or maybe,<br>
>            various parts of the type checker for Agda, to see how much<br>
>         the type check costs.<br>
>         <br>
>         5. Strict evaluation is a different world. Lazy computation<br>
>         allows us to write a simpler code.<br>
>            If you write all your applications in assembly, they will<br>
>         most probably be several times <br>
>            faster further.  <br>
>         <br>
> <br>
> <br>
> Because , agda is a total language, you can use either strict<br>
> evaluation or lazy evaluation on the same agda code.<br>
> <br>
> <br>
> With strict evaluation and with agda-ocaml, one needs to simply<br>
> increase the limits of the stack to a big number so<br>
> that it does not stack overflow.<br>
> <br>
>  <br>
>         Regards,<br>
>         <br>
>         ------<br>
>         Sergei<br>
>         <br>
>         <br>
>         <br>
>         <br>
<br>
<br>
</blockquote></div></div>