[Agda] type check performance

[Larrytheliquid]

Expanding a little on what Neel said, and assuming that the papers I've
read in the past are still relevant:

A key part of why first-order approximation can lead to faster
unification/judgmental equality checking
is the following. In Coq, great care is taken to not expand definitions
(deltas in the delta-equality sense).
This is because Coq will allow unification problems to be solved with
applications of definitions resembling
constructor applications when finding first-order approximate solutions.
This is why Coq
does not generate most general unifiers, whereas Agda does.

In contrast, when unifying/checking judgmental equality for the problem x =
y, Agda will first
convert x and y to weak-head normal form. This constant conversion to whnf
(in every recursive call of equality
checking that fails alpha-conversion) can of course be expensive, as the
reduction process can be computationally
intensive and result in large weak-head normal terms.
Again, Coq will do the same thing if first-order approximation fails, but
many times Coq unification can find solutions
before getting to that point.

So I would say a caveat to comparing Coq and Agda is that they are not
solving the same problem. Agda cares
about most-general unifiers whereas Coq does not.

On Mon, Jan 9, 2017 at 9:28 AM, Neel Krishnaswami <nk480 at cl.cam.ac.uk>
wrote:

> 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
>>
>> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>



-- 
Respectfully,
Larry Diehl
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170110/1eb2d6df/attachment-0001.html>