[Agda] type check performance

Sergei Meshveliani mechvel at botik.ru
Wed Jan 11 14:01:15 CET 2017


Can anybody, please, explain in short, what is happening with type
inference in the example of

 slow :  {A : Set} → A → A
 slow =  id id id id  id id id id  id id id id  id id id id
         id id id id  id id id id
?
Why is it so expensive in Agda and in Coq ?

What terms are being unified, normalized (by which rules?) ?
(I expect that these terms internally represent type expressions).
Is this pattern matching of a term against a ground term, or it is
finding a most general unifier for two terms having variables? 

As I recall, a naive unification method costs exponentially for the
worst case, and there is known the method by Martelli & Montanari,
which improves this ...

Thanks,

------
Sergei



On Tue, 2017-01-10 at 16:15 -0800, Larrytheliquid wrote:
> 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
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda




More information about the Agda mailing list