[Agda] type check performance

[Andreas Abel]

 > what is this that makes Agda type check performance cost much more
 > than Coq's ?

Sounds like a research question to me.
Maybe you can get some research funding to investigate this.

Best,
Andreas

On 08.01.2017 20:20, Sergei Meshveliani wrote:
> Dear Agda developers,
> I have the following question about the type check performance.
>
> Last summer I talked to a person who is experienced in programming
> proofs in Coq. I asked him about the type check performance.
> He said that the only source of an unnatural type check cost with Coq
> can be not of the language/compiler/interpreter itself, but due to
> unlucky usage of proof _tactics_ in the user program.
> Of course, one can apply a proof tactic in a terrible way.
>
> With Agda, I currently use (sometimes) only one tactic, it is of the
> Standard library: bringing to normal form by SemiringSolver.
> And this cannot involve any inefficiency.
> So, the question is:
> what is this that makes Agda type check performance cost much more than
> Coq's ?
>
> Regards,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/