[Agda] Type-checker evaluator performance

[Sergei Meshveliani]

On Wed, 2016-02-03 at 10:31 +0100, Ulf Norell wrote:
> I think it's unfortunate, if perhaps not completely undeserved, that
> Agda gets blamed every time a program is slow or uses a lot of memory.
> When people are writing slow Haskell programs their first thoughts are
> "maybe I should try to optimise my program", not "maybe someone should
> optimise GHC" and I wish we could have a little more of that for Agda
> programs. 
> [..]


I am using GHC for many years for programming symbolic computation in
algebra. Each time I was able to detect the source of inefficiency in
my program, and to obtain a naturally looking program which performance
is natural, is as expected.

With Agda, this is different.
I have a basic algebra library, with all the algorithms being simple.
Say, test primality of a natural by searching through, or may be, by
sieve. And the proofs are also simple, for example, 
"merging two ordered lists yields an ordered list",
"in a monoid an inverse to x is unique, if exists".

But it needs 17 Gb heap to type-check. And I do not see any way to
optimize my program any essentially.
With GHC, I always find: how to optimize my program in a natural way.
With Agda, I fail to find.

If I replace all functions and proofs with 'postulate', it will take
about 6 Gb  to type-check. Probably, it somehow unfolds the very _data
structures_ in a strange way (nested records, parametric module
hierarchy, importing each other).  I suspect that this is due to call by
name.

I think that Agda is very good. 
And as it is really good, its type checker deserves to be optimized.

Regards,

------
Sergei