[Agda] result code explosion
Serge D. Mechveliani
mechvel at botik.ru
Tue Apr 2 14:45:23 CEST 2013
Dear Agda developers,
there is a certain problem with the memory expenses, intermediate and
final code explosion.
Do you consider the ways to reduce the produced code size?
I do understand that
* Agda is not Haskell; checking dependent types looks like an heavy
problem, there may be even a fundamental reason of why it may take a
lot of memory/time,
* it may occur that my application code can be optimized many times
with respect to memory (this is my first experience with dependent
But let me describe the situation, just to inform you of what is
happining, for any occasion.
When type-checking my module AlgClasses2.agda,
Agda-2.3.2 MAlonzo (lib-0.7, ghc-7.6.2)
takes about 800 Mb memory.
On 1 Gb machine, the system starts swapping at this and slows down
All right, we have extended RAM, and this example is passed.
Now consider the type checker memory eagerness.
The module has about 400 lines of Agda source
-- counting without comments and empty lines.
This is quite large. So, one who got used to Haskell, would expect that
its processing would take the miminum of, say, 40 Mb.
My impression is that the type checker spends somewhat 20 times more
of memory than the GHC compiler spends for the Haskell code of the same
Concerning the code size:
1.034.755 b AlgClasses2.agdai
2.862.400 b AlgClasses2.hi
1.073.333 b AlgClasses2.hs -- 23413 lines
2.927.256 b AlgClasses2.o
400 lines of Agda have converted to 23413 lines of the Haskell code.
The executable has about 14 M byte.
My DoCon has about 100 times larger Haskell code for the demo program,
and GHC produces the executable of about 13 M byte.
So far, I never tried to run this AlgClasses2 executable, I expect
adventures at run time
(it has many nested `classes', but for really running it, I need to add
implementation for various instances).
All right, Agda is not Haskell, and I expected the effect of this kind.
But: may be something can be done?
About this particular application
It describes the algebraic `classes' from DSet to Ring, GCDRing,
FactorizationRing, EuclidanRing, Field.
Also it describes
Subset, Subsemigroup, ..., Subring, Ideal, ReductionIdeal.
This makes it many records, some of which are nested to the depth of
about 15 -- 20 levels. Typically such a record has 2 fields and also
exports about 8 items which are implemented via these fields. Such a
record looks almost like an usual program module, but has a couple of
I do not know, may be there is a particular reason of why this all
causes a certain Haskell code explosion.
But at least it is compiled (!), and I hope to reach running examples,
and to see further.
More information about the Agda