[Agda] running out of memory in formalization of category theory

[Dan Licata]

Hi everyone,

I need to formalize a little category theory, in particular the
Grothendieck construction and the various type constructors in Cat.  I
know others have run into trouble with Agda being slow / running out of
memory when formalizing category theory, and I'm running into similar
issues.

For example, the three files defining the Grothendieck construction take
1-2 minutes to check each, which makes it very hard to use the
interactive editor.  Other parts of the development just run out of heap
(using +RTS -M2G on a 2.26GHz Macbook pro with 4GB RAM, which is all I
can do before it goes into page swap hell).

If it's helpful, there are +RTS -s reports in the following files:
homotopy.coercions.cat.dat.Groth
homotopy.coercions.cat.dat.GrothTermA
homotopy.coercions.cat.dat.GrothTermB
homotopy.coercions.cat.dat.GrothTermC
homotopy.coercions.ProdB [runs out of memory]

The allocation rate seems quite high (300-500MB / second).  


I've come up with a few strategies that have gotten me this far:

(1) Defining "raw" categories (just the sets of objects and arrows) and
functors (just the actions) and raw versions of each construction,
and then proving that the raw versions are in fact categories (identity
and composition, etc.) and functors (preserve identities and
compositions).  This worked in some spots where trying to define the
whole category/functor all at once did not.

(2) Using datatypes instead of records, and sometimes pattern-matching
earlier than I'd like.  For example, homotopy/coercions/Groth.lagda and
homotopy/coercions/Groth-RunsOutOfMemory.lagda differ only by currying:
the version that takes a (dependent) pair of arguments and projects out
the componenets runs out of memory, whereas the version that takes two
separate arguments works.


If anyone has any advice about

(a) what is causing Agda to be slow here?
(b) any workarounds?

I'd greatly appreciate it.

The code is here:
http://www.cs.cmu.edu/~drl/tmp/groth.tgz


Thanks!
-Dan