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

[Thorsten Altenkirch]

It seems that it is a feature of Agda that it will run out of memory  
if you try to formalize category theory :-)

See James Chapman's recent attempts.

Cheers,
Thorsten

On 2 Jun 2010, at 20:50, Dan Licata wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda