<div dir="ltr">The one in the standard library is very slow, but if you&#39;re willing to use &#39;erase&#39; [1] you<div>can implement a fast one that just needs a call to the builtin boolean equality on nats.</div><div>See the agda-prelude library for an implementation [2].</div><div><div><br></div><div>/ Ulf</div><div><br></div><div>[1] <a href="https://github.com/agda/agda-stdlib/blob/e3893da/src/Relation/Binary/PropositionalEquality/TrustMe.agda#L25-L26">https://github.com/agda/agda-stdlib/blob/e3893da/src/Relation/Binary/PropositionalEquality/TrustMe.agda#L25-L26</a></div></div><div>[2] <a href="https://github.com/UlfNorell/agda-prelude/blob/48d1b8e8/src/Prelude/Nat.agda#L67-L70">https://github.com/UlfNorell/agda-prelude/blob/48d1b8e8/src/Prelude/Nat.agda#L67-L70</a></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Sep 22, 2016 at 10:16 PM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">And how much does it cost  m ≟ n<br>
for Nat ?<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
On Fri, 2016-09-23 at 00:08 +0400, Sergei Meshveliani wrote:<br>
&gt; Another reason for necessity of n-ary provable arithmetic:<br>
&gt;<br>
&gt;   _≤?_  of Data.Nat.decTotalOrder  is slow.<br>
&gt;<br>
&gt; Probably this is because it is not built-in<br>
&gt; (and how can it? assuming that the result may contain a proof made of<br>
&gt; many certain constructors).<br>
&gt;<br>
&gt; This leads, for example, to that sorting of the list  [10000 ... 1]  is<br>
&gt; done many times faster when the numbers are binary-coded<br>
&gt; (and it is applied _≤?_ of DecTotalOrder for Bin).<br>
&gt;<br>
&gt; ------<br>
&gt; Sergei<br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt; On Thu, 2016-09-22 at 22:30 +0400, Sergei Meshveliani wrote:<br>
&gt; &gt; On Thu, 2016-09-22 at 12:38 -0400, Wolfram Kahl wrote:<br>
&gt; &gt; &gt; Sergei,<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; On Wed, Sep 21, 2016 at 02:34:28PM +0200, Ulf Norell wrote:<br>
&gt; &gt; &gt; &gt; How is this better than what we do at the moment? It seems to me that<br>
&gt; &gt; &gt; &gt; your postulated properties of the macro digit operations are going to be<br>
&gt; &gt; &gt; &gt; more<br>
&gt; &gt; &gt; &gt; complicated than what we postulate right now (namely that Haskell Integer<br>
&gt; &gt; &gt; &gt; arithmetic implement the expected functions on natural numbers).<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; Indeed.<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; One possibly interesting avenue to expore in this direction,<br>
&gt; &gt; &gt; and requiring no modification of Agda, would be starting from the fact<br>
&gt; &gt; &gt; that GHC supports two implementations of Haskell Integer:<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt;  * The default implementation calls the GPL-licenced GMP library via the FFI<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt;  * An alternative implementation (called SimpleInteger?)<br>
&gt; &gt; &gt;    for GPL-averse contexts is, if I remember correctly, implemented in Haskell.<br>
&gt; &gt; &gt;    (So that would be some kind of lists of Macrodigits already.)<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; You could go and implement your lists of Macrodigits in Agda, and<br>
&gt; &gt; &gt; use Agda&#39;s reverse FFI to export this to Haskell to replace SimpleInteger.<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; And try to be faster! ;-)<br>
&gt; &gt;<br>
&gt; &gt;<br>
&gt; &gt; 1) In principle:  Agda Standard library needs a proved arithmetic for<br>
&gt; &gt; Nat which is several times faster that the existing one of Data.Bin.<br>
&gt; &gt;<br>
&gt; &gt; 2) For example, Bin._+_ is  2^n times  faster than Nat._+_ (unary),<br>
&gt; &gt; and can be supplied with all the necessary proofs<br>
&gt; &gt; (mainly: a proof for that the ring of Nat is isomorphic to the ring of<br>
&gt; &gt; Bin, this is enough).<br>
&gt; &gt;<br>
&gt; &gt; 3) Further, _+_ for the  Hexa -coded naturals is can be programmed in<br>
&gt; &gt; Agda, so that it will be several times faster than Bin._+_, and will be<br>
&gt; &gt; supplied with the proof for that the ring of Nat is isomorphic to the<br>
&gt; &gt; ring of Hexa).<br>
&gt; &gt; And this does not need any built-ins (no postulates) for digits.<br>
&gt; &gt; But it will be about 8 times slower than Integer._+_ in GHC<br>
&gt; &gt; (because 4-Hexa-digit numbers are summed by one macrodigit operation in<br>
&gt; &gt; GHC, and because a digit operation in Hexa in Agda is not in one step).<br>
&gt; &gt;<br>
&gt; &gt; 4) As to doing the same for lists of large macrodigits (say 64 bit<br>
&gt; &gt; digit), there it will have sense to make the digit operations built-in<br>
&gt; &gt; (with several postulated properties) an all the rest written in Agda,<br>
&gt; &gt; with proofs.<br>
&gt; &gt;<br>
&gt; &gt;<br>
&gt; &gt; But  I am not currently going to implement any of these things.<br>
&gt; &gt; These are only my notes, comments.<br>
&gt; &gt;<br>
&gt; &gt; []<br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt;<br>
<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>