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

[Alan Jeffrey]

I'm quite happy with optimizing the representation of Agda's primitives, 
but I'd rather do something that's not specific to naturals.

The approach I took with the JS back-end was to allow (essentially) view 
patterns in datatype bindings, which allow Agda datatypes to be bound to 
any native type.

Doing this for Haskell, we'd have something like:

   data Nat : Set where
     zero : Nat
     suc : Nat -> Nat

   {-# COMPILED_VIEW view inv Integer Zero Suc #-}

where Haskell defines:

   data View = Zero | Suc Integer

   view :: Integer -> View
   view 0 = Zero
   view n = Suc (n-1)

   inv :: View -> Integer
   inv Zero = 0
   inv (Suc n) = n+1

then the compiler just has to insert "view" and "inv" functions into the 
current translation, and hey presto Agda naturals are bound to Haskell 
integers.

Stick in some optimizations (view (inv x) == x) and (inv (view x) == x) 
and you should get a run-time that's as good as putting integer-specific 
trickery into the compiler.

A.


On 04/19/2012 10:46 AM, Daniel Peebles wrote:
> 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
> <mailto: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 <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/__mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
>
>