[Agda] Performance issues with --sharing

[Sergei Meshveliani]

On Thu, 2015-09-24 at 13:57 -0300, Peter Selinger wrote:
> Dear all,
> 
> last month, in the thread "type check performance", Wolfram Kahl
> suggested that I try the experimental --sharing feature in the
> development branch.
> 
> The issue at hand was Agda's extremely inefficient evaluation
> strategy, which is normal order and not lazy: it recomputes the same
> value a potentially unlimited number of times.
> 
> [..]
>
> I think a proper lazy evaluation strategy will eventually be a
> must-have feature, and unfortunately, --sharing does not seem to be
> it. Right now I am rewriting many of my programs using forced
> strictness and CPS translations, and this makes them efficient, but
> unreadable (and non-trivial to prove theorems about).
> 
> As mentioned in a previous thread: I am aware that the code becomes
> more efficient when I compile it to Haskell. But since all of my code
> is used inside proofs, it is really the type checking cost that is
> affected. 


I join this wish.

I have not looked into Peter's example, but my experience with DoConA
shows that the type check expense remains unnaturally great.
Currently I am happy with that it type-checks within 9 Gb and 10
minutes. But the project is small, it needs to grow.

I did an experiment: replaced most of proofs (95 %) with `postulate',
so that it contained almost exclusively (nested) type declarations,
parametric modules, and several trivial algorithms.
And this reduced thing still needs  3 Gb  to type-check.
 
I am not sure, but suspect that call by need, and such things, will
reduce the type check expense in my current project somewhat 20 times
(and remove an exponent cost summand that, I suspect, the type checker
has). 

Regards,

------
Sergei