[Agda] Performance issues and code structure.

[James Chapman]

Hi Dan,

This has also been one of my hobbies too for a while. It's quite fun  
to see how far you can get with these things before you run out of  
memory. :)

I can't offer any further insight into the inner workings of Agda but  
I do feel you pain! One simple thing I have found helpful is when you  
have a choice of categorical definition use the most concise/flatter  
one. E.g. Monads as Kleisli triples not as a functor with two natural  
transformations or adjunctions given with a bijection that is natural  
rather than with the unit and counit.

If you're interested you can find some of my previous experiments  
here. You're welcome to dig around.

http://sneezy.cs.nott.ac.uk/darcs/normal/Algebra/

Something more recent is this little workshop abstract:

http://www.cs.ioc.ee/~james/PUBLICATION_files/Assisted_Monads.pdf

Accompanying work in progress is here:

http://www.cs.ioc.ee/~james/repos/AssistedMonads/

Cheers,

James

On Sep 27, 2009, at 7:49 AM, Dan Doel wrote:

> Greetings,
>
> I've been starting up some formalism of category theory (with --type- 
> in-type
> for now, until universe polymorphism gets in swing), and seem to  
> have hit a
> wall in performance. The relevant module is available at:
>
>  http://code.haskell.org/~dolio/agda-share/categorica/Category/Product.agda
>
> There was nothing too bad about it until I added ×-swap, which  
> demonstrates
> that there's an isomorphism between the product of two objects and  
> the product
> of the objects in the opposite order. As you can see, there are  
> some, I think,
> fairly modest equational proofs, but with this in play, agda starts  
> taking
> quite a bit of time to check the module, and uses around 25% of my  
> memory in
> doing so (I have 2 gigabytes, for reference).
>
> As you can see, below that is half of a proof that product for three  
> objects
> is associative up to isomorphism. However, it's commented out,  
> because Agda is
> no longer capable of checking everything there at once. I think I've
> successfully had it check things when any one of the sub-proofs is  
> commented
> out, so I'm fairly confident that it should check. However, it ends  
> up taking
> about 75% of my memory, and eventually just quits. Loading it up  
> using the
> command line 'agda' command reveals that it's causing a (haskell)  
> stack
> overflow.
>
> Unless I've just glanced by it, I don't think the proof is circular,  
> and this
> seems to just be an exacerbated version of the swap proof. Is it the
> equational reasoning that's so expensive?
>
> Someone also suggest in #agda on freenode that bundling proof terms  
> into
> records representing structures caused performance problems, and  
> that's why
> the Algebra modules in the standard library are structured the way  
> they are.
> However, I tried breaking things up similarly in a brief experiment,  
> but
> didn't notice any improvements (I'm also not sure how to break up my
> _HasProducts record along those lines, as it doesn't exactly contain  
> ordinary
> terms and proof terms together itself, so much as it references a  
> bundling;
> moving the proofs to a separate module didn't help, either). Is that  
> one of
> the aims in the standard library, or no?
>
> It seems as though I've written proofs significantly larger than  
> these without
> completely exhausting my resources (or overflowing the stack),  
> although this
> is the first time I've made such extensive use of the equational  
> reasoning
> framework (which I copied into a module in the directory to prevent  
> agda --
> html from generating gobs of std-lib documents; apologies). Has  
> anyone else
> run into similar problems with this, and were you able to do  
> anything about
> it?
>
> I'd understand if Agda just needs some performance tweaking love.  
> But if I'm
> doing something wrong, or there's something I can do now to  
> alleviate the
> situation that isn't too invasive, it'd be nice to know.
>
> (On a side note, giant memory growth followed by stack overflow  
> sounds like a
> space leak due to lack of strictness, as far as Haskell goes. But, I  
> don't
> really know anything about what Agda does when it's checking/ 
> evaluating
> programs. It also seems to hang on to the memory after it completes,  
> so maybe
> the structures it's building are, in fact, that large.)
>
> Thanks.
>
> -- Dan
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda