[Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes

[Alan Jeffrey]

You might want to have a look at the agda-data-bindings project up on 
Github...

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

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.

There is also a datatype:

   data Strict (A : Set) : Set where
     ! : A -> Strict A

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.

   https://github.com/agda/agda-system-io

It might be that these libraries (or something like them) could be used 
in your case without patching the compiler.

A.

On 04/18/2012 03:48 PM, James Deikun wrote:
> I've been playing around with an (unproven; even un-termination-checked
> in places) implementation of the Sieve of Eratosthenes to see how well
> Agda's compile-time evaluator can stack up in the best cases.  The
> call-by-name evaluation model and the fundamentally unary nature of
> builtin Naturals present substantial difficulties, but it seems
> eminently practical to determine primes as high as the 400th (2741) if
> not higher.  The code is located at http://github.com/xplat/potpourri/
> under the Primes directory.
>
> In order to achieve reasonable performance for operations on Nats I
> created a small library, FastNat.agda, which binds a couple of unbound
> builtins and redefines basic auxiliary datatypes, like _≤_, as well as
> many of the functions and proofs.  It aims at allowing small, fast
> representations by using naturals and their equalities to represent all
> induction and indexing in the datatypes (since naturals can be
> represented as literals and equalities are constant size; see also
> below).  _≤_ is represented as follows:
>
>> record _≤_ (m n : Nat) : Set where
>>    constructor le
>>    field
>>      k : Nat
>>      m+k≡n : m + k ≡ n
>
> Needless recursion when building or verifying equalities is prevented
> using the following function, which throws away its argument while
> requiring a suitable proof of said argument's existence:
>
>> hideProof : {a : Level} {A : Set a} {x y : A} ->  x ≡ y ->  x ≡ y
>> hideProof eq = trustMe
>
> By careful use of this primitive and builtins such as NATEQUALS and
> NATLESS it should be possible to build, say, a DecTotalOrder with all
> operations executing on literals in time logarithmic in the magnitude of
> the numbers; this has been verified for all operations but total (which
> still uses a raw trustMe) and no serious difficulties are anticipated.
>
> FastNat does, however, require a small patch (attached) to Agda to
> achieve its advertised speed.
>
> The pairing heap (Heap.agda) and sieve (Sieve.agda) implementations use
> pattern-matching as a sequentialization measure to control duplication
> of unevaluated thunks, which can cause an exponential slowdown.  Aside
> from that they are largely straightforward implementations of the
> respective data structure and algorithm, the latter following "The
> Genuine Sieve of Eratosthenes" by M.E. O'Neill.
>
> Comments and improvements gratefully accepted.