<div dir="ltr">Expanding a little on what Neel said, and assuming that the papers I've read in the past are still relevant:<div><br></div><div>A key part of why first-order approximation can lead to faster unification/judgmental equality checking</div><div>is the following. In Coq, great care is taken to not expand definitions (deltas in the delta-equality sense).</div><div>This is because Coq will allow unification problems to be solved with applications of definitions resembling</div><div>constructor applications when finding first-order approximate solutions. This is why Coq</div><div>does not generate most general unifiers, whereas Agda does.</div><div><br></div><div>In contrast, when unifying/checking judgmental equality for the problem x = y, Agda will first</div><div>convert x and y to weak-head normal form. This constant conversion to whnf (in every recursive call of equality</div><div>checking that fails alpha-conversion) can of course be expensive, as the reduction process can be computationally</div><div>intensive and result in large weak-head normal terms. </div><div>Again, Coq will do the same thing if first-order approximation fails, but many times Coq unification can find solutions</div><div>before getting to that point.</div><div><br></div><div>So I would say a caveat to comparing Coq and Agda is that they are not solving the same problem. Agda cares</div><div>about most-general unifiers whereas Coq does not.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Jan 9, 2017 at 9:28 AM, Neel Krishnaswami <span dir="ltr"><<a href="mailto:nk480@cl.cam.ac.uk" target="_blank">nk480@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
In terms of design, Coq's type inference algorithm in roughly the same<br>
ballpark as Agda's. Namely, they are both built on a foundation of<br>
pattern unification, with some extensions.<br>
<br>
Eg, on the one hand my understanding is that Agda is a bit smarter<br>
about resolving  patterns outside of the pattern fragment lazily, but<br>
that Coq uses the "first-order approximation" to solve some problems<br>
outside the pattern fragment. So it shouldn't be the case that type<br>
*inference* is hugely more expensive for either system. (Though<br>
typeclass resolution in Coq can be slow, since it is willing to<br>
backtrack in that case.)<br>
<br>
However, my understanding is that Agda still has a fairly simple<br>
implementation of judgmental equality, whereas Coq has optimized it<br>
very heavily. So reflective decision procedures are more likely to<br>
be efficient in Coq than in Agda.<br>
<br>
(I haven't dug deeply into the implementations of either system, so<br>
take all this with a grain of salt, though.)<br>
<br>
Best,<br>
Neel<div class="HOEnZb"><div class="h5"><br>
<br>
On 09/01/17 11:51, Thorsten Altenkirch wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Just a general remark: when we talk about type checking we really mean<br>
type inference, which involves solving equations due to implicit syntax.<br>
My impression is that some of the stuff done in Coq tactics is done as<br>
type inference in the case of Agda. Another issue is that a lot of Coq<br>
practice doesn¹t use dependent types but uses simply typed programs and<br>
then uses predicate logic to reason about completely bypassing some of the<br>
issues Agda has.<br>
<br>
Thorsten<br>
<br>
On 08/01/2017, 19:20, "Agda on behalf of Sergei Meshveliani"<br>
<<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.s<wbr>e</a> on behalf of <a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>> wrote:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Dear Agda developers,<br>
I have the following question about the type check performance.<br>
<br>
Last summer I talked to a person who is experienced in programming<br>
proofs in Coq. I asked him about the type check performance.<br>
He said that the only source of an unnatural type check cost with Coq<br>
can be not of the language/compiler/interpreter itself, but due to<br>
unlucky usage of proof _tactics_ in the user program.<br>
Of course, one can apply a proof tactic in a terrible way.<br>
<br>
With Agda, I currently use (sometimes) only one tactic, it is of the<br>
Standard library: bringing to normal form by SemiringSolver.<br>
And this cannot involve any inefficiency.<br>
So, the question is:<br>
what is this that makes Agda type check performance cost much more than<br>
Coq's ?<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</blockquote>
<br>
<br>
<br>
<br>
<br>
This message and any attachment are intended solely for the addressee<br>
and may contain confidential information. If you have received this<br>
message in error, please send it back to me, and immediately delete it.<br>
<br>
Please do not use, copy or disclose the information contained in this<br>
message or in any attachment.  Any views or opinions expressed by the<br>
author of this email do not necessarily reflect the views of the<br>
University of Nottingham.<br>
<br>
This message has been checked for viruses but the contents of an<br>
attachment may still contain software viruses which could damage your<br>
computer system, you are advised to perform your own checks. Email<br>
communications with the University of Nottingham may be monitored as<br>
permitted by UK legislation.<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br>
</blockquote>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature">Respectfully,<br>Larry Diehl<br></div>
</div>