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

[Daniel Peebles]

No, I don't even mean dealing with generated code (as I almost never
compile my Agda). This is about optimizing the typechecker so that our
compile-time normalization runs in reasonable time.

Take Fin, indexed by naturals. Now say you take the bitvector library that
Eric Mertens and I wrote, that represents machine words of arbitrary bit
lengths. Clearly these should be isomorphic to Fin (2 ^ n). Attempting to
even begin to typecheck a proof of that is completely intractable in
current Agda, though. Apparently there are quadratic numbers of conversions
(quadratic in the *value* of the number) to and from unary naturals and GMP
integers during the typechecking and that's what makes this so unpleasant.

So when I say I welcome optimizations to Agda's special treatment of
naturals, I mean during normalization, not compilation. Large naturals can
be represented intelligently, and even open terms (suc (suc (suc (suc (suc
(suc (blah blah blah))))))) could be represented internally as an addition
to avoid exponential blowup of terms in memory. I think there's a lot of
potentially very useful work to be done here, completely independently of
compiler backends. I do think that your bindings work is also important for
real backends, but I don't think it makes any of James's work any less
necessary or important.

Dan

On Thu, Apr 19, 2012 at 12:09 PM, Alan Jeffrey <ajeffrey at bell-labs.com>wrote:

> 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>
>>
>>    <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>
>>
>>    <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/>
>>
>>        <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>
>>    <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/fe229938/attachment-0001.html