I would welcome patches to the compiler, though. It's doing some fairly strange inefficient stuff with Nats (converting to and from GMP integers way too often) right now, and it'd be nice to speed up everything that used them.<div>
<br><br><div class="gmail_quote">On Thu, Apr 19, 2012 at 10:36 AM, Alan Jeffrey <span dir="ltr"><<a href="mailto:ajeffrey@bell-labs.com">ajeffrey@bell-labs.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
You might want to have a look at the agda-data-bindings project up on Github...<br>
<br>
<a href="https://github.com/agda/agda-data-bindings" target="_blank">https://github.com/agda/agda-<u></u>data-bindings</a><br>
<br>
It has bindings for a bunch of low-level Haskell types, including Naturals. There's mappings ! and % back and forth from Agda's naturals to Haskell naturals.<br>
<br>
There is also a datatype:<br>
<br>
data Strict (A : Set) : Set where<br>
! : A -> Strict A<br>
<br>
whose constructor is strict in Haskell, so evaluates its argument to whnf. This was enough for me to get efficient naturals in the streaming I/O library, for example a word-count transducer that runs in constant space.<br>
<br>
<a href="https://github.com/agda/agda-system-io" target="_blank">https://github.com/agda/agda-<u></u>system-io</a><br>
<br>
It might be that these libraries (or something like them) could be used in your case without patching the compiler.<br>
<br>
A.<div><div class="h5"><br>
<br>
On 04/18/2012 03:48 PM, James Deikun wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
I've been playing around with an (unproven; even un-termination-checked<br>
in places) implementation of the Sieve of Eratosthenes to see how well<br>
Agda's compile-time evaluator can stack up in the best cases. The<br>
call-by-name evaluation model and the fundamentally unary nature of<br>
builtin Naturals present substantial difficulties, but it seems<br>
eminently practical to determine primes as high as the 400th (2741) if<br>
not higher. The code is located at <a href="http://github.com/xplat/potpourri/" target="_blank">http://github.com/xplat/<u></u>potpourri/</a><br>
under the Primes directory.<br>
<br>
In order to achieve reasonable performance for operations on Nats I<br>
created a small library, FastNat.agda, which binds a couple of unbound<br>
builtins and redefines basic auxiliary datatypes, like _≤_, as well as<br>
many of the functions and proofs. It aims at allowing small, fast<br>
representations by using naturals and their equalities to represent all<br>
induction and indexing in the datatypes (since naturals can be<br>
represented as literals and equalities are constant size; see also<br>
below). _≤_ is represented as follows:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
record _≤_ (m n : Nat) : Set where<br>
constructor le<br>
field<br>
k : Nat<br>
m+k≡n : m + k ≡ n<br>
</blockquote>
<br>
Needless recursion when building or verifying equalities is prevented<br>
using the following function, which throws away its argument while<br>
requiring a suitable proof of said argument's existence:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
hideProof : {a : Level} {A : Set a} {x y : A} -> x ≡ y -> x ≡ y<br>
hideProof eq = trustMe<br>
</blockquote>
<br>
By careful use of this primitive and builtins such as NATEQUALS and<br>
NATLESS it should be possible to build, say, a DecTotalOrder with all<br>
operations executing on literals in time logarithmic in the magnitude of<br>
the numbers; this has been verified for all operations but total (which<br>
still uses a raw trustMe) and no serious difficulties are anticipated.<br>
<br>
FastNat does, however, require a small patch (attached) to Agda to<br>
achieve its advertised speed.<br>
<br>
The pairing heap (Heap.agda) and sieve (Sieve.agda) implementations use<br>
pattern-matching as a sequentialization measure to control duplication<br>
of unevaluated thunks, which can cause an exponential slowdown. Aside<br>
from that they are largely straightforward implementations of the<br>
respective data structure and algorithm, the latter following "The<br>
Genuine Sieve of Eratosthenes" by M.E. O'Neill.<br>
<br>
Comments and improvements gratefully accepted.<br>
</blockquote></div></div>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>