[Agda] Performance issues and code structure.

[Dan Doel]

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