<div dir="ltr">The one in the standard library is very slow, but if you're willing to use 'erase' [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"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></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>
> Another reason for necessity of n-ary provable arithmetic:<br>
><br>
> _≤?_ of Data.Nat.decTotalOrder is slow.<br>
><br>
> Probably this is because it is not built-in<br>
> (and how can it? assuming that the result may contain a proof made of<br>
> many certain constructors).<br>
><br>
> This leads, for example, to that sorting of the list [10000 ... 1] is<br>
> done many times faster when the numbers are binary-coded<br>
> (and it is applied _≤?_ of DecTotalOrder for Bin).<br>
><br>
> ------<br>
> Sergei<br>
><br>
><br>
><br>
> On Thu, 2016-09-22 at 22:30 +0400, Sergei Meshveliani wrote:<br>
> > On Thu, 2016-09-22 at 12:38 -0400, Wolfram Kahl wrote:<br>
> > > Sergei,<br>
> > ><br>
> > > On Wed, Sep 21, 2016 at 02:34:28PM +0200, Ulf Norell wrote:<br>
> > > > How is this better than what we do at the moment? It seems to me that<br>
> > > > your postulated properties of the macro digit operations are going to be<br>
> > > > more<br>
> > > > complicated than what we postulate right now (namely that Haskell Integer<br>
> > > > arithmetic implement the expected functions on natural numbers).<br>
> > ><br>
> > > Indeed.<br>
> > ><br>
> > > One possibly interesting avenue to expore in this direction,<br>
> > > and requiring no modification of Agda, would be starting from the fact<br>
> > > that GHC supports two implementations of Haskell Integer:<br>
> > ><br>
> > > * The default implementation calls the GPL-licenced GMP library via the FFI<br>
> > ><br>
> > > * An alternative implementation (called SimpleInteger?)<br>
> > > for GPL-averse contexts is, if I remember correctly, implemented in Haskell.<br>
> > > (So that would be some kind of lists of Macrodigits already.)<br>
> > ><br>
> > > You could go and implement your lists of Macrodigits in Agda, and<br>
> > > use Agda's reverse FFI to export this to Haskell to replace SimpleInteger.<br>
> > ><br>
> > > And try to be faster! ;-)<br>
> ><br>
> ><br>
> > 1) In principle: Agda Standard library needs a proved arithmetic for<br>
> > Nat which is several times faster that the existing one of Data.Bin.<br>
> ><br>
> > 2) For example, Bin._+_ is 2^n times faster than Nat._+_ (unary),<br>
> > and can be supplied with all the necessary proofs<br>
> > (mainly: a proof for that the ring of Nat is isomorphic to the ring of<br>
> > Bin, this is enough).<br>
> ><br>
> > 3) Further, _+_ for the Hexa -coded naturals is can be programmed in<br>
> > Agda, so that it will be several times faster than Bin._+_, and will be<br>
> > supplied with the proof for that the ring of Nat is isomorphic to the<br>
> > ring of Hexa).<br>
> > And this does not need any built-ins (no postulates) for digits.<br>
> > But it will be about 8 times slower than Integer._+_ in GHC<br>
> > (because 4-Hexa-digit numbers are summed by one macrodigit operation in<br>
> > GHC, and because a digit operation in Hexa in Agda is not in one step).<br>
> ><br>
> > 4) As to doing the same for lists of large macrodigits (say 64 bit<br>
> > digit), there it will have sense to make the digit operations built-in<br>
> > (with several postulated properties) an all the rest written in Agda,<br>
> > with proofs.<br>
> ><br>
> ><br>
> > But I am not currently going to implement any of these things.<br>
> > These are only my notes, comments.<br>
> ><br>
> > []<br>
><br>
><br>
><br>
><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>