[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