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

[Daniel Peebles]

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.


On Thu, Apr 19, 2012 at 10:36 AM, Alan Jeffrey <ajeffrey at bell-labs.com>wrote:

> You might want to have a look at the agda-data-bindings project up on
> Github...
>
>  https://github.com/agda/agda-**data-bindings<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<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/<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.
>>
> ______________________________**_________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120419/b698efc1/attachment.html