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

[Conor McBride]

On 3 Jun 2010, at 11:07, Ulf Norell wrote:

>
> On Wed, Jun 2, 2010 at 10:01 PM, Thorsten Altenkirch <txa at cs.nott.ac.uk 
> > wrote:
> It seems that it is a feature of Agda that it will run out of memory  
> if you try to formalize category theory :-)
>
> It's for your own protection!
>
> Seriously though, my suspicion is that the terms you get when  
> formalizing category theory get extremely
> large with all the implicit stuff filled in. Being careful to  
> maintain sharing might help with that, but that
> requires some reworking of the internals.

What astonishes me is how much further people seem to get when
they're formalizing type theory. It's a fix!

Or is it that treatments of type theory tend to live in the
inductively defined fragment, which is less eta-expandable?

Cheers

Conor