[Agda] type check performance
Sergei Meshveliani
mechvel at botik.ru
Wed Jan 11 19:46:00 CET 2017
I see, thank you.
Here the size of the type expression grows 2 times with each adding of
`id'.
Probably this expense in unavoidable. Because if we write a textbook and
need to explain what is the type of the leftmost `id' map there in
id id id id id id id id,
then we need to place to the text the below large expression.
And my case is different. I define standard classical algebraic
structures: Semigroup, Group, Ring, EuclideanRing, and such, and prove
in Agda certain well-known properties of their operations. There cannot
appear such type expressions like above for id id ... id.
And still its type check needs 7Gb RAM and 60 minutes of time (on a 3
GHz computer).
If we write all this as a textbook, together with rigorous constructive
proofs, this will probably make it a book of 500 pages. It will contain
many lemmata that refer to each other, and one structure definition
referring to another structure definition. 500 pages makes it about
500 * 5000 = 2500 K byte of volume -- this is very small.
GHC and Agda read and understand these proofs much faster than an human.
So Agda needs to type-check this book, probably, in 10 seconds.
There is something strange in these 60 minutes and 7 Gb minimum.
For example, EuclideanRing is far enough in the hierarchy.
And I ask to print the type (C-c C-d) of the function (lemma)
remByDivisor : (a b : C) → b ∣ a → eucRem a b ≈ 0#
in the module parameterized by an instance of EuclideanRing.
It shows
(a b : UpIntegralRing.Carrier upIR) →
(UpIntegralRing.*upMonoid upIR UpMonoid.∣ b) a →
(upIR UpIntegralRing.≈ EuclideanRing.eucRem upIR∣? E a b)
(UpIntegralRing.0# upIR)
This does not look like a large expression
(though it contains several parts that may need to be replaced with
their expanded definitions, depending on situation).
If a human can (?) check by hand in 10 days all the proofs in this 500
page book (this can be done by reading the source Agda program),
then why Agda cannot do the same in 10 seconds?
I do not know, may be a human avoids some unneeded expression expansion
when substituting things. The effect is not clear to me.
Regards,
------
Sergei
On Wed, 2017-01-11 at 14:07 +0100, G. Allais wrote:
> 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
> >
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
More information about the Agda
mailing list