[Agda] MAlonzo performance

[Mateusz Kowalczyk]

On 27/03/14 17:50, Sergei Meshveliani wrote:
> 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
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

I'd like to latch onto this e-mail and ask whether anyone is working on
improving the size and performance of the generated Haskell code. Even
mere Hello World in Agda takes ~10 minutes to generate and compile and
the binary is tens of MBs big. I think this makes the code generation
very impractical (to not say useless) for toy examples, not to even
mention actual projects. I mean Sergei is worrying how to get his
project to take less than 20 hours to compile! Just the thought that 20
hours is a goal seems silly.

Is MAlonzo intended to ever be practical or is it just a project to show
that the generation is possible and we don't care for anything else?

Thanks

-- 
Mateusz K.