I've actually been working on rationals just recently, but the code is a bit of a mess. I take more or less the same approach as the std lib, though, but I use an irrelevant coprimality proof. I do prefer to keep the rationals in reduced form to be able to use propositional equality instead of a custom equivalence.<div>
<br></div><div>I haven't considered using the FFI, but using James Deikun's new Fast natural arithmetic (including a new fast GCD implementation) we can actually get reasonable performance out my code, even during compile-time normalization. James can probably give you more details on that.<br>
<br>I've mostly focussed on non-negative rationals so far, so most of the reasonable code is in <a href="https://github.com/copumpkin/rational/blob/master/Rational/Nonnegative.agda">https://github.com/copumpkin/rational/blob/master/Rational/Nonnegative.agda</a> . The Rational.agda module is somewhat bitrotted.<div>
<br></div><div>I apologize that the code is a mess, but I've been distracted by other things recently and haven't had a chance to continue it or tidy it up.</div><div><br></div><div>Dan<br><br><div class="gmail_quote">
On Wed, May 9, 2012 at 11:06 AM, Noam Zeilberger <span dir="ltr"><<a href="mailto:noam.zeilberger@gmail.com" target="_blank">noam.zeilberger@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Does anyone have experience writing Agda code involving some<br>
non-trivial computation on the integers/rationals? I'm writing some<br>
code where the goal is not formalization of arithmetic per se, but<br>
where I would like to be able to actually run some computations which<br>
might require, e.g., addition-multiplication-division of six-digit<br>
numbers. I think I would be happy if there were a way to defer all<br>
these calculations to Haskell's builtin exact rational arithmetic and<br>
then reason axiomatically...which seems to be what the foreign<br>
function interface would provide, except that if I understand<br>
correctly (<a href="http://wiki.portal.chalmers.se/agda/agda.php?n=Docs.FFI" target="_blank">http://wiki.portal.chalmers.se/agda/agda.php?n=Docs.FFI</a>) it<br>
only works with the Alonzo/MAlonzo backends, and not in interactive<br>
mode. Ideally, I would like to be able to run arithmetic computations<br>
interactively, see their results, *and* have Agda verify that the<br>
results have a particular normal form.<br>
<br>
For now I'm using the standard library implementations of Data.Nat and<br>
Data.Integer with a slightly modified Data.Rational (which does not<br>
keep rationals in reduced form, to make it easier to do computations),<br>
but this seems to be unworkably slow even on small examples. For<br>
example, computing the gcd (Data.Nat.Gcd) of 2012 and 1984 takes about<br>
three and a half minutes on my laptop.<br>
<br>
Noam<br>
_______________________________________________<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" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div></div>