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

[James Deikun]

On Mon, 2012-04-23 at 16:14 +0200, Nils Anders Danielsson wrote:
> On 2012-04-18 22:48, James Deikun wrote:
> > 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
> 
> Nice trick. I wonder if it's sound. If it is sound, then we should
> perhaps try to find a less hacky way to do this.

Indeed.  I can't say for sure that it's sound, but at least the one
major issue I thought of (that termination checking might see that the
recursive calls are thrown away and admit proofs that wouldn't terminate
with 'hideProof = id') doesn't seem to be a problem from my testing.
(I'm not sure that it won't show up in sufficiently complex mutual
recursions, though.)

And this does seem to be more generally applicable than many of the
other speedup techniques.

> > 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.
> 
> We should really switch to a more efficient evaluation strategy.

I had heard that something like this might come out of the last AIM; is
there any work in progress?

It does seem like a tough nut to crack, with reduce and reduceB
currently in TCM; eliminating that effect to allow the reuse of
Haskell's lazy evaluation would be a serious bit of rearchitecture in
itself, and both graph- and let-based explicit call-by-need evaluators
would need a major reworking of the term representation ...