[Agda] MAlonzo performance

[Alan Jeffrey]

My experience with MAlonzo is that it gives decent performance as long 
as you tune your code to MAlonzo's strengths. In particular, not linking 
against the standard library, and structuring code so that the 
executable fragment doesn't carry proofs around. Of course, this is 
easier said than done, some code is naturally proof-carrying.

You can see a (rather old, and probably now non-compiling) example of 
this over at https://github.com/agda/agda-system-io which does a lot of 
low-level hackery to get decent space/time performance out of MAlonzo.

A.

On 03/27/2014 01:07 PM, Mateusz Kowalczyk wrote:
> 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
>