[Agda] MAlonzo performance

[Sergei Meshveliani]

Dear Agda developers,

this is about the performance of the checker and also of MAlonzo.

1) I have the  DoCon  library for computer algebra written in Haskell.

2) I have a certain small initial  DoCon-A  library   written in Agda, 
   with proofs provided. 

The Agda source is somewhat 50 times smaller than the Haskell source of 
DoCon, about 2 units lower in the used domain constructor level,
may be, 300 times smaller in functionality 
(if not to count proofs!).


GHC `makes' DoCon in about 10 minutes, taking about 200 Mb  of space.

As to  DoCon-A, 
it  type-checks  within a  9 Gb  in 15 min.

(this is on the Development Agda of February 16, 2014).

Then, there proceeds  MAlonzo + GHC,  which takes  58 minutes 
to produce  .hs  and  .o
(I put  -M9G  for space into the  $MAlonzo-opt option).

There are many modules, and
the average                 .agda  size  is  20 Kb. 
the average produced        .hs    size  is  15 Mb. 

I compile DoCon-A by 

  agda -c $libOpt +RTS ..-M9G ..-RTS  $MAlonzo-opt  AlgTest.agda


To really develop a project, there will be needed to increase the domain
level in the .agda code somewhat on 2 units, to increase the module
import level on 3-4 units, to add many times more of functionality.

And looking forward, I 

(1) wonder about how could this fit into 12 Gb and, say, 20 hours,

(2) recall that  fast Integer with proofs  is desirable in the Library
(represented by macro-digits in  N-ary system).

About (2):
Many things in algorithmic algebra can be computed over  
(Integer modulo m)  rather than Integer,  with  1 < m < 20.
For example, computing in  FiniteField(prime-m)  and in constructions
over it.

Still large Integer cannot be avoided in practice for a long time.
It is evident that it can be programmed in Agda with proofs.
Probably, it is very difficult to provide proofs for _advanced_
algorithms for an arbitrary large integer arithmetic. 
Therefore, I think, simplest algorithms need to be applied -- for the
first release.
If it is, say, 10 - 20  times slower on average than in GHC, this will
be all right.

Regards,

------
Sergei