[Agda] type check performance
G. Allais
guillaume.allais at ens-lyon.org
Wed Jan 11 14:07:20 CET 2017
If you use an alternative definition of `id` that takes its type
argument explicitly, you can see where the problem comes from:
==============================================================
module Slow-id where
id : (A : Set) → A → A
id _ x = x
slow : (A : Set) → A → A
slow A =
(id {!!})
(id {!!})
(id {!!})
(id {!!})
(id {!!})
(id {!!})
(id {!!})
(id {!!})
{- `C-c C-s` solves the type holes to:
slow : (A : Set) → A → A
slow A =
(id (((((((A → A) → A → A) → (A → A) → A → A) →
((A → A) → A → A) → (A → A) → A → A) →
(((A → A) → A → A) → (A → A) → A → A) →
((A → A) → A → A) → (A → A) → A → A) →
((((A → A) → A → A) → (A → A) → A → A) →
((A → A) → A → A) → (A → A) → A → A) →
(((A → A) → A → A) → (A → A) → A → A) →
((A → A) → A → A) → (A → A) → A → A) →
(((((A → A) → A → A) → (A → A) → A → A) →
((A → A) → A → A) → (A → A) → A → A) →
(((A → A) → A → A) → (A → A) → A → A) →
((A → A) → A → A) → (A → A) → A → A) →
((((A → A) → A → A) → (A → A) → A → A) →
((A → A) → A → A) → (A → A) → A → A) →
(((A → A) → A → A) → (A → A) → A → A) →
((A → A) → A → A) → (A → A) → A → A))
(id ((((((A → A) → A → A) → (A → A) → A → A) →
((A → A) → A → A) → (A → A) → A → A) →
(((A → A) → A → A) → (A → A) → A → A) →
((A → A) → A → A) → (A → A) → A → A) →
((((A → A) → A → A) → (A → A) → A → A) →
((A → A) → A → A) → (A → A) → A → A) →
(((A → A) → A → A) → (A → A) → A → A) →
((A → A) → A → A) → (A → A) → A → A))
(id (((((A → A) → A → A) → (A → A) → A → A) →
((A → A) → A → A) → (A → A) → A → A) →
(((A → A) → A → A) → (A → A) → A → A) →
((A → A) → A → A) → (A → A) → A → A))
(id ((((A → A) → A → A) → (A → A) → A → A) →
((A → A) → A → A) → (A → A) → A → A))
(id (((A → A) → A → A) → (A → A) → A → A))
(id ((A → A) → A → A))
(id (A → A))
(id A)
-}
==============================================================
On 11/01/17 14:01, Sergei Meshveliani wrote:
> 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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170111/e1a83884/attachment.sig>
More information about the Agda
mailing list