[Agda] FYI: Rationals in Idris

[Bas Spitters]

In our paper with Robbert Krebbers
Type classes for efficient exact real arithmetic in Coq
http://www.lmcs-online.org/ojs/viewarticle.php?id=987&layout=abstract

We emphasise the use of approximate rationals (e.g. dyadic rationals)
for efficient computation. The efficiency gain is quite striking.


Of course, we also provide a library for rational numbers in corn.
IIRC this was the basis for the current implementation of rationals in
the coq std lib by Pierre Letouzey.

Bas

On Fri, Dec 11, 2015 at 2:15 PM, Ulf Norell <ulf.norell at gmail.com> wrote:
> Also:
> https://github.com/UlfNorell/agda-prelude/blob/master/src/Data/Rational.agda
>
> I maintain (statically) the invariant that numerator and denominator are
> coprime by doing a gcd for every operation, which of course affects
> performance. Everything is using primitive integer operations though so it's
> fast enough for practical applications, if not for high-performance
> situations.
>
> / Ulf
>
> On Fri, Dec 11, 2015 at 1:55 PM, Dr. ÉRDI Gergő <gergo at erdi.hu> wrote:
>>
>> I hope this might be useful to someone as well:
>> http://stackoverflow.com/questions/31212459/how-to-add-two-rational-in-agda/31265445#31265445
>>
>> On 11 Dec 2015 20:46, "Andreas Abel" <abela at chalmers.se> wrote:
>>>
>>> Nicola Botta told me that he and Tim Richter both implemented rationals
>>> in Idris.  See:
>>>
>>>
>>>
>>> https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/NonNegRationalProperties.lidr
>>>
>>>
>>>
>>> https://github.com/nicolabotta/SeqDecProbs/blob/master/frameworks/14-/NonNegRational2.lidr
>>>
>>> It is not clear yet whether these implementations are efficient enough.
>>> I just post them as a reference in case someone makes a library for
>>> rationals in Agda.
>>>
>>> Cheers,
>>> Andreas
>>>
>>> --
>>> Andreas Abel  <><      Du bist der geliebte Mensch.
>>>
>>> Department of Computer Science and Engineering
>>> Chalmers and Gothenburg University, Sweden
>>>
>>> andreas.abel at gu.se
>>> http://www2.tcs.ifi.lmu.de/~abel/
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>