<div dir="ltr"><div><div>On the matter of Agda vs human, there is also the question which one, when used as a proof checker, has more bugs impacting soundness. Probably the human brain includes lots of heuristics (similar to the first-order approximation used in Coq) that may or may not be sound in general. It may even skip some boring parts of a proof entirely. The simple fact that we understand Agda much better than the human brain (in a relative sense) is a huge plus for Agda in my eyes, and makes me much more likely to trust it. But the fact that it is simpler also means that it will be slower in certain cases (by which I do not mean that Agda couldn't work faster on your particular development).<br><br></div>Cheers,<br></div>Jesper<br><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Jan 11, 2017 at 7:46 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I see, thank you.<br>
Here the size of the type expression grows 2 times with each adding of<br>
`id'.<br>
<br>
Probably this expense in unavoidable. Because if we write a textbook and<br>
need to explain what is the type of the leftmost `id' map there in<br>
id id id id id id id id,<br>
then we need to place to the text the below large expression.<br>
<br>
And my case is different. I define standard classical algebraic<br>
structures: Semigroup, Group, Ring, EuclideanRing, and such, and prove<br>
in Agda certain well-known properties of their operations. There cannot<br>
appear such type expressions like above for id id ... id.<br>
<br>
And still its type check needs 7Gb RAM and 60 minutes of time (on a 3<br>
GHz computer).<br>
<br>
If we write all this as a textbook, together with rigorous constructive<br>
proofs, this will probably make it a book of 500 pages. It will contain<br>
many lemmata that refer to each other, and one structure definition<br>
referring to another structure definition. 500 pages makes it about<br>
500 * 5000 = 2500 K byte of volume -- this is very small.<br>
<br>
GHC and Agda read and understand these proofs much faster than an human.<br>
So Agda needs to type-check this book, probably, in 10 seconds.<br>
<br>
There is something strange in these 60 minutes and 7 Gb minimum.<br>
For example, EuclideanRing is far enough in the hierarchy.<br>
And I ask to print the type (C-c C-d) of the function (lemma)<br>
<br>
remByDivisor : (a b : C) → b ∣ a → eucRem a b ≈ 0#<br>
<br>
in the module parameterized by an instance of EuclideanRing.<br>
It shows<br>
<br>
(a b : UpIntegralRing.Carrier upIR) →<br>
(UpIntegralRing.*upMonoid upIR UpMonoid.∣ b) a →<br>
(upIR UpIntegralRing.≈ EuclideanRing.eucRem upIR∣? E a b)<br>
(UpIntegralRing.0# upIR)<br>
<br>
This does not look like a large expression<br>
(though it contains several parts that may need to be replaced with<br>
their expanded definitions, depending on situation).<br>
<br>
If a human can (?) check by hand in 10 days all the proofs in this 500<br>
page book (this can be done by reading the source Agda program),<br>
then why Agda cannot do the same in 10 seconds?<br>
<br>
I do not know, may be a human avoids some unneeded expression expansion<br>
when substituting things. The effect is not clear to me.<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<div class="m_3255012731417478609HOEnZb"><div class="m_3255012731417478609h5"><br>
<br>
<br>
On Wed, 2017-01-11 at 14:07 +0100, G. Allais wrote:<br>
> If you use an alternative definition of `id` that takes its type<br>
> argument explicitly, you can see where the problem comes from:<br>
><br>
> ==============================<wbr>==============================<wbr>==<br>
> module Slow-id where<br>
><br>
> id : (A : Set) → A → A<br>
> id _ x = x<br>
><br>
> slow : (A : Set) → A → A<br>
> slow A =<br>
> (id {!!})<br>
> (id {!!})<br>
> (id {!!})<br>
> (id {!!})<br>
> (id {!!})<br>
> (id {!!})<br>
> (id {!!})<br>
> (id {!!})<br>
><br>
> {- `C-c C-s` solves the type holes to:<br>
> slow : (A : Set) → A → A<br>
> slow A =<br>
> (id (((((((A → A) → A → A) → (A → A) → A → A) →<br>
> ((A → A) → A → A) → (A → A) → A → A) →<br>
> (((A → A) → A → A) → (A → A) → A → A) →<br>
> ((A → A) → A → A) → (A → A) → A → A) →<br>
> ((((A → A) → A → A) → (A → A) → A → A) →<br>
> ((A → A) → A → A) → (A → A) → A → A) →<br>
> (((A → A) → A → A) → (A → A) → A → A) →<br>
> ((A → A) → A → A) → (A → A) → A → A) →<br>
> (((((A → A) → A → A) → (A → A) → A → A) →<br>
> ((A → A) → A → A) → (A → A) → A → A) →<br>
> (((A → A) → A → A) → (A → A) → A → A) →<br>
> ((A → A) → A → A) → (A → A) → A → A) →<br>
> ((((A → A) → A → A) → (A → A) → A → A) →<br>
> ((A → A) → A → A) → (A → A) → A → A) →<br>
> (((A → A) → A → A) → (A → A) → A → A) →<br>
> ((A → A) → A → A) → (A → A) → A → A))<br>
> (id ((((((A → A) → A → A) → (A → A) → A → A) →<br>
> ((A → A) → A → A) → (A → A) → A → A) →<br>
> (((A → A) → A → A) → (A → A) → A → A) →<br>
> ((A → A) → A → A) → (A → A) → A → A) →<br>
> ((((A → A) → A → A) → (A → A) → A → A) →<br>
> ((A → A) → A → A) → (A → A) → A → A) →<br>
> (((A → A) → A → A) → (A → A) → A → A) →<br>
> ((A → A) → A → A) → (A → A) → A → A))<br>
> (id (((((A → A) → A → A) → (A → A) → A → A) →<br>
> ((A → A) → A → A) → (A → A) → A → A) →<br>
> (((A → A) → A → A) → (A → A) → A → A) →<br>
> ((A → A) → A → A) → (A → A) → A → A))<br>
> (id ((((A → A) → A → A) → (A → A) → A → A) →<br>
> ((A → A) → A → A) → (A → A) → A → A))<br>
> (id (((A → A) → A → A) → (A → A) → A → A))<br>
> (id ((A → A) → A → A))<br>
> (id (A → A))<br>
> (id A)<br>
> -}<br>
> ==============================<wbr>==============================<wbr>==<br>
><br>
> On 11/01/17 14:01, Sergei Meshveliani wrote:<br>
> > Can anybody, please, explain in short, what is happening with type<br>
> > inference in the example of<br>
> ><br>
> > slow : {A : Set} → A → A<br>
> > slow = id id id id id id id id id id id id id id id id<br>
> > id id id id id id id id<br>
> > ?<br>
> > Why is it so expensive in Agda and in Coq ?<br>
> ><br>
> > What terms are being unified, normalized (by which rules?) ?<br>
> > (I expect that these terms internally represent type expressions).<br>
> > Is this pattern matching of a term against a ground term, or it is<br>
> > finding a most general unifier for two terms having variables?<br>
> ><br>
> > As I recall, a naive unification method costs exponentially for the<br>
> > worst case, and there is known the method by Martelli & Montanari,<br>
> > which improves this ...<br>
> ><br>
> > Thanks,<br>
> ><br>
> > ------<br>
> > Sergei<br>
> ><br>
> ><br>
> ><br>
> > On Tue, 2017-01-10 at 16:15 -0800, Larrytheliquid wrote:<br>
> >> Expanding a little on what Neel said, and assuming that the papers<br>
> >> I've read in the past are still relevant:<br>
> >><br>
> >><br>
> >> A key part of why first-order approximation can lead to faster<br>
> >> unification/judgmental equality checking<br>
> >> is the following. In Coq, great care is taken to not expand<br>
> >> definitions (deltas in the delta-equality sense).<br>
> >> This is because Coq will allow unification problems to be solved with<br>
> >> applications of definitions resembling<br>
> >> constructor applications when finding first-order approximate<br>
> >> solutions. This is why Coq<br>
> >> does not generate most general unifiers, whereas Agda does.<br>
> >><br>
> >><br>
> >> In contrast, when unifying/checking judgmental equality for the<br>
> >> problem x = y, Agda will first<br>
> >> convert x and y to weak-head normal form. This constant conversion to<br>
> >> whnf (in every recursive call of equality<br>
> >> checking that fails alpha-conversion) can of course be expensive, as<br>
> >> the reduction process can be computationally<br>
> >> intensive and result in large weak-head normal terms.<br>
> >> Again, Coq will do the same thing if first-order approximation fails,<br>
> >> but many times Coq unification can find solutions<br>
> >> before getting to that point.<br>
> >><br>
> >><br>
> >> So I would say a caveat to comparing Coq and Agda is that they are not<br>
> >> solving the same problem. Agda cares<br>
> >> about most-general unifiers whereas Coq does not.<br>
> >><br>
> >> On Mon, Jan 9, 2017 at 9:28 AM, Neel Krishnaswami <<a href="mailto:nk480@cl.cam.ac.uk" target="_blank">nk480@cl.cam.ac.uk</a>><br>
> >> wrote:<br>
> >> Hi,<br>
> >><br>
> >> In terms of design, Coq's type inference algorithm in roughly<br>
> >> the same<br>
> >> ballpark as Agda's. Namely, they are both built on a<br>
> >> foundation of<br>
> >> pattern unification, with some extensions.<br>
> >><br>
> >> Eg, on the one hand my understanding is that Agda is a bit<br>
> >> smarter<br>
> >> about resolving patterns outside of the pattern fragment<br>
> >> lazily, but<br>
> >> that Coq uses the "first-order approximation" to solve some<br>
> >> problems<br>
> >> outside the pattern fragment. So it shouldn't be the case that<br>
> >> type<br>
> >> *inference* is hugely more expensive for either system.<br>
> >> (Though<br>
> >> typeclass resolution in Coq can be slow, since it is willing<br>
> >> to<br>
> >> backtrack in that case.)<br>
> >><br>
> >> However, my understanding is that Agda still has a fairly<br>
> >> simple<br>
> >> implementation of judgmental equality, whereas Coq has<br>
> >> optimized it<br>
> >> very heavily. So reflective decision procedures are more<br>
> >> likely to<br>
> >> be efficient in Coq than in Agda.<br>
> >><br>
> >> (I haven't dug deeply into the implementations of either<br>
> >> system, so<br>
> >> take all this with a grain of salt, though.)<br>
> >><br>
> >> Best,<br>
> >> Neel<br>
> >><br>
> >><br>
> >> On 09/01/17 11:51, Thorsten Altenkirch wrote:<br>
> >> Just a general remark: when we talk about type<br>
> >> checking we really mean<br>
> >> type inference, which involves solving equations due<br>
> >> to implicit syntax.<br>
> >> My impression is that some of the stuff done in Coq<br>
> >> tactics is done as<br>
> >> type inference in the case of Agda. Another issue is<br>
> >> that a lot of Coq<br>
> >> practice doesn¹t use dependent types but uses simply<br>
> >> typed programs and<br>
> >> then uses predicate logic to reason about completely<br>
> >> bypassing some of the<br>
> >> issues Agda has.<br>
> >><br>
> >> Thorsten<br>
> >><br>
> >> On 08/01/2017, 19:20, "Agda on behalf of Sergei<br>
> >> Meshveliani"<br>
> >> <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.<wbr>se</a> on behalf of<br>
> >> <a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>> wrote:<br>
> >><br>
> >> Dear Agda developers,<br>
> >> I have the following question about the type<br>
> >> check performance.<br>
> >><br>
> >> Last summer I talked to a person who is<br>
> >> experienced in programming<br>
> >> proofs in Coq. I asked him about the type<br>
> >> check performance.<br>
> >> He said that the only source of an unnatural<br>
> >> type check cost with Coq<br>
> >> can be not of the<br>
> >> language/compiler/interpreter itself, but due<br>
> >> to<br>
> >> unlucky usage of proof _tactics_ in the user<br>
> >> program.<br>
> >> Of course, one can apply a proof tactic in a<br>
> >> terrible way.<br>
> >><br>
> >> With Agda, I currently use (sometimes) only<br>
> >> one tactic, it is of the<br>
> >> Standard library: bringing to normal form by<br>
> >> SemiringSolver.<br>
> >> And this cannot involve any inefficiency.<br>
> >> So, the question is:<br>
> >> what is this that makes Agda type check<br>
> >> performance cost much more than<br>
> >> Coq's ?<br>
> >><br>
> >> Regards,<br>
> >><br>
> >> ------<br>
> >> Sergei<br>
> >><br>
> >> _____________________________<wbr>__________________<br>
> >> Agda mailing list<br>
> >> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> >> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mai<wbr>lman/listinfo/agda</a><br>
> >><br>
> >><br>
> >><br>
> >><br>
> >><br>
> >> This message and any attachment are intended solely<br>
> >> for the addressee<br>
> >> and may contain confidential information. If you have<br>
> >> received this<br>
> >> message in error, please send it back to me, and<br>
> >> immediately delete it.<br>
> >><br>
> >> Please do not use, copy or disclose the information<br>
> >> contained in this<br>
> >> message or in any attachment. Any views or opinions<br>
> >> expressed by the<br>
> >> author of this email do not necessarily reflect the<br>
> >> views of the<br>
> >> University of Nottingham.<br>
> >><br>
> >> This message has been checked for viruses but the<br>
> >> contents of an<br>
> >> attachment may still contain software viruses which<br>
> >> could damage your<br>
> >> computer system, you are advised to perform your own<br>
> >> checks. Email<br>
> >> communications with the University of Nottingham may<br>
> >> be monitored as<br>
> >> permitted by UK legislation.<br>
> >><br>
> >> _____________________________<wbr>__________________<br>
> >> Agda mailing list<br>
> >> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> >> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mai<wbr>lman/listinfo/agda</a><br>
> >><br>
> >> _____________________________<wbr>__________________<br>
> >> Agda mailing list<br>
> >> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> >> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mai<wbr>lman/listinfo/agda</a><br>
> >><br>
> >><br>
> >><br>
> >><br>
> >><br>
> >> --<br>
> >> Respectfully,<br>
> >> Larry Diehl<br>
> >><br>
> >> ______________________________<wbr>_________________<br>
> >> Agda mailing list<br>
> >> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> >> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
> ><br>
> ><br>
> > ______________________________<wbr>_________________<br>
> > Agda mailing list<br>
> > <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> > <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
> ><br>
><br>
> ______________________________<wbr>_________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</div></div></blockquote></div><br></div></div>