I would welcome patches to the compiler, though. It&#39;s doing some fairly strange inefficient stuff with Nats (converting to and from GMP integers way too often) right now, and it&#39;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">&lt;<a href="mailto:ajeffrey@bell-labs.com">ajeffrey@bell-labs.com</a>&gt;</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&#39;s mappings ! and % back and forth from Agda&#39;s naturals to Haskell naturals.<br>
<br>
There is also a datatype:<br>
<br>
  data Strict (A : Set) : Set where<br>
    ! : A -&gt; 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&#39;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&#39;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&#39;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} -&gt;  x ≡ y -&gt;  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 &quot;The<br>
Genuine Sieve of Eratosthenes&quot; by M.E. O&#39;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>