[Agda] type check performance

[Neel Krishnaswami]

Hi,

In terms of design, Coq's type inference algorithm in roughly the same
ballpark as Agda's. Namely, they are both built on a foundation of
pattern unification, with some extensions.

Eg, on the one hand my understanding is that Agda is a bit smarter
about resolving  patterns outside of the pattern fragment lazily, but
that Coq uses the "first-order approximation" to solve some problems
outside the pattern fragment. So it shouldn't be the case that type
*inference* is hugely more expensive for either system. (Though
typeclass resolution in Coq can be slow, since it is willing to
backtrack in that case.)

However, my understanding is that Agda still has a fairly simple
implementation of judgmental equality, whereas Coq has optimized it
very heavily. So reflective decision procedures are more likely to
be efficient in Coq than in Agda.

(I haven't dug deeply into the implementations of either system, so
take all this with a grain of salt, though.)

Best,
Neel

On 09/01/17 11:51, Thorsten Altenkirch wrote:
> 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.
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>