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

[Nicolas Pouillard]

On Sun, 06 Jun 2010 14:05:15 +0100, Nils Anders Danielsson <nad at Cs.Nott.AC.UK> wrote:
> On 2010-06-05 19:45, Nicolas Pouillard wrote:
> > Throwing away these terms using an option may allow to significantly reduce
> > the memory needed to type-check big developments.
> 
> Perhaps. However, the compiler does generate code for abstract blocks,
> so it would not (in general) be correct to do so.

I agree, that's why I suggested an option, mainly to speed up development
time.

> > This seems counter intuitive. I makes more sense and would fit nicely
> > with submodules to have each abstract block independent.
> 
> Sometimes later abstract definitions depend on the actual definitions of
> earlier abstract definitions. In that case it can be quite convenient
> not to have to write all abstract definitions in a single block.

One can make the same argument in the opposite direction. Suppose I want
write a definition without relying on previous definitions and make it
abstract as well.

To workaround any of the two situations one can keep both the concrete
version and the abstract one.

< concrete-foo : Bar
< concrete-foo = ...
<
< abstract
<   foo : Bar
<   foo = concrete-foo

This may suggest a finer-grained support at the term level, where we could
make abstract a name in a term.

< term ::= ... | abstract name

Using this, `abstract foo' is almost like `foo' (same type and definition)
but can only be compared by its name and so will only be equal to itself.

What do you think?

Best regards,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr