[Agda] type check performance

[Thorsten Altenkirch]

Just a general remark: when we talk about type checking we really mean
type inference, which involves solving equations due to implicit syntax.
My impression is that some of the stuff done in Coq tactics is done as
type inference in the case of Agda. Another issue is that a lot of Coq
practice doesn¹t use dependent types but uses simply typed programs and
then uses predicate logic to reason about completely bypassing some of the
issues Agda has.

Thorsten

On 08/01/2017, 19:20, "Agda on behalf of Sergei Meshveliani"
<agda-bounces at lists.chalmers.se on behalf of mechvel at botik.ru> 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





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.