[Agda] Efficient numeric computations in Agda

[Nils Anders Danielsson]

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?

-- 
/NAD