[Agda] MAlonzo performance

[Aaron Stump]

I will echo this concern about performance.  I am finding for my Agda 
parser generator called gratr -- see

https://svn.divms.uiowa.edu/repos/clc/projects/gratr2

with username guest, password guest -- that just getting Agda to 
type-check a file a couple thousand lines long takes more time and 
memory (10 minutes?  more than 4GB?) than is feasible for a development 
cycle where you are tweaking your grammar and then compiling so you can 
run sample input strings.

I am currently working on contortions so I can get realistic grammars, 
which generate Agda files tens of thousands of lines long, through 
(hint: type-checking very large strings is instantaneous). But this is 
ugly.

Cheers,
Aaron
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
>