[Agda] [PATCH] Agda evaluation challenge -- Sieve of Eratosthenes
Alan Jeffrey
ajeffrey at bell-labs.com
Thu Apr 19 22:30:11 CEST 2012
Good point, this is compile-time rather than run-time. I guess my
grumble is with Agda's special treatment of naturals via BUILTINs rather
than this particular patch which looks like A Good Thing.
It would be nice if most of the BUILTINs could be moved out of the
compiler and into the standard library somehow, so that the optimized
representations used at run-time were accessible at compile-time too.
Even if this were doable, though, it still leaves the issue with
optimizing the representation of open terms. As you say, it would be
nice if an open term of type Nat could be represented normalized as
(k+M) for k an integer constant.
A.
On 04/19/2012 12:35 PM, Daniel Peebles wrote:
> 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
> <mailto: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>
> <mailto: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>
> <mailto: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>>
>
>
>
More information about the Agda
mailing list