[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