[Agda] Type-checker evaluator performance

[Ulf Norell]

On Wed, Feb 3, 2016 at 4:16 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:

>
> 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.
>
> I think that Agda is very good.
> And as it is really good, its type checker deserves to be optimized.
>

I'm absolutely not saying that Agda couldn't or shouldn't be optimised. I
also agree completely that performance debugging Agda programs is hard,
especially when it comes to type checking performance. What I'm trying to
say is that I sometimes get the feeling (perhaps unfairly?) that people
aren't even trying to optimise their programs because everybody knows that
Agda is slow.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160203/925cd9c4/attachment.html