[Agda] Efficient numeric computations in Agda

[Alan Jeffrey]

There's also bindings to the native Haskell Integer type in 
Data.Natural, available from:

   https://github.com/agda/agda-data-bindings/

The only operations are zero, suc, _+_ and fold, though that is just 
because those were the only ones I happened to need.

A.


On 08/14/2011 05:44 PM, Nils Anders Danielsson wrote:
> On 2011-08-14 23:45, Arseniy Alekseyev wrote:
>> I am starting to learn Agda and trying to solve some Project Euler
>> problems with it.
>> To solve some of them one needs efficient number representation
>> (binary rather than unary).
>>
>> The agda standard library seems not to provide such data types.
>
> Data.Bin provides a binary representation of natural numbers along with
> a small set of operations. Performance is likely to be terrible in
> comparison with something like GMP.
>
> The Epic backend automatically turns unary natural numbers into binary
> ones.
>
>> Another problem I had is the performance of Data.Nat.DivMod.divMod.
>> The source code says that its run time should be linear in the size of
>> dividend, but for me it's definitely quadratic.
>
> The source code states the following:
>
>     The run-time complexity of this implementation of integer division
>     should be linear in the size of the dividend, assuming that
>     well-founded recursion and the equality type are optimised properly
>     (see "Inductive Families Need Not Store Their Indices" (Brady,
>     McBride, McKinna, TYPES 2003)).
>
>> I'm running the code from emacs' "Evaluate term to normal form"
>> command.
>
> This evaluator does not perform this kind of optimisation. Neither does
> the Haskell backend. I'm not sure how well the Epic backend handles this
> code. Daniel and Olle, have you tested this?
>