<div dir="ltr"><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Mar 4, 2020 at 5:33 PM <<a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><br>
It looks like this.<br>
Following this paper, we can define a direct product of rings, denote it <br>
_*_,<br>
and put<br>
     G = Z * Z * Z * Z * Z * Z * Z * Z             (I)<br>
<br>
for the ring Z for Integer.<br>
And it may occur that this will be a hard type checking example for <br>
Agda.<br></blockquote></div><div class="gmail_quote"><br></div><div class="gmail_quote">This will certainly not be a hard type checking problem for Agda. Depending on how</div><div class="gmail_quote">you define _*_ and Z computing with G can of course blow up.<br></div><div class="gmail_quote"><br></div><div class="gmail_quote">/ Ulf<br></div><div class="gmail_quote"><br></div><div class="gmail_quote">> On 04.03.20 00:04, Jason Gross wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
>> I'm confused by this.  Are you saying that in Agda typechecking is <br>
>> exponential<br>
>> in the number of files?  Or exponential in the number of nested <br>
>> abstractions? <br>
>> Or something else?  Do you have a toy example demonstrating this <br>
>> behavior?<br>
>> <br>
>> On Tue, Mar 3, 2020, 17:42 <<a href="mailto:mechvel@scico.botik.ru" target="_blank">mechvel@scico.botik.ru</a><br>
>> <mailto:<a href="mailto:mechvel@scico.botik.ru" target="_blank">mechvel@scico.botik.ru</a>>> wrote:<br>
>> <br>
>>     On 2020-03-04 00:31, Jason Gross wrote:<br>
>>     >> Which bottlenecks are you referring to? Are they intrinsically <br>
>> tied<br>
>>     > to dependent types, or they are related to the treatment of<br>
>>     > propositions and equality in systems such as Coq?<br>
>>     ><br>
>>     > The main bottleneck that I'm referring to here (though not the <br>
>> only<br>
>>     > one of my thesis) is the one that is due to the fact that <br>
>> arbitrary<br>
>>     > conversion problems can happen during typechecking.  This is <br>
>> used to<br>
>>     > great advantage in proof by reflection (where all of the work is <br>
>> done<br>
>>     > in checking that a proof of "true = true" has the type <br>
>> "some-check =<br>
>>     > true").  But it also causes performance issues if you're not <br>
>> careful.<br>
>>     > To take a toy example, consider two different definitions of<br>
>>     > factorial: n! = n * (n - 1)!, and n! = (n - 1)! * n.  Suppose <br>
>> you have<br>
>>     > two different ways of computing a vector (length-indexed list) <br>
>> of<br>
>>     > permutations, one which defines the length in terms of the first<br>
>>     > factorial, and the other one which defines the length in terms <br>
>> of the<br>
>>     > second factorial.  Suppose you now try to prove that the two <br>
>> methods<br>
>>     > give the same result on any concrete list of length of length <br>
>> 10.<br>
>>     > Just to check that this goal is valid, Coq is now trying to <br>
>> compute<br>
>>     > 10! as a natural number.  This example is a bit contrived, but <br>
>> less<br>
>>     > egregious versions of this issue abound, and when doing verified<br>
>>     > engineering at scale, these issues can add up in hard-to-predict <br>
>> ways.<br>
>>     >  I have a real-world example where changing the input size just <br>
>> a<br>
>>     > little bit caused `reflexivity` to take over 400 hours, rather <br>
>> than<br>
>>     > just a couple of minutes.<br>
>>     ><br>
>>     > On Tue, Mar 3, 2020, 16:00 Viktor Kunčak <<a href="mailto:vkuncak@gmail.com" target="_blank">vkuncak@gmail.com</a><br>
>>     <mailto:<a href="mailto:vkuncak@gmail.com" target="_blank">vkuncak@gmail.com</a>>> wrote:<br>
>>     ><br>
>>     >> I would be also curious to hear answers to this questions!<br>
>>     >> ("Lots of people do it" seems like a very compelling answer.)<br>
>>     >><br>
>>     >> Which bottlenecks are you referring to? Are they intrinsically <br>
>> tied<br>
>>     >> to dependent types, or they are related to the treatment of<br>
>>     >> propositions and equality in systems such as Coq?<br>
>>     >><br>
>> <br>
>>     There is a problem of the type checking cost in Agda, and probably <br>
>> in<br>
>>     Coq too.<br>
>>     I do not know of whether it is fundamental or technical. And I <br>
>> have not<br>
>>     seen an answer to this question, so far. On practice, it looks <br>
>> like<br>
>>     this:<br>
>>     Agda can type-check only a small part of the computer algebra <br>
>> library of<br>
>>     methods (with full proofs). With implementing it further, with<br>
>>     increasing the hierarchy level of parameterized modules, the type<br>
>>     check cost seems to grow exponentially in the level.<br>
>>     So, after implementing in Agda an average textbook on computer <br>
>> algebra<br>
>>     (where is known a constructive proof for each statement), say, of <br>
>> 500<br>
>>     pages, it will not be type-checked in 100 years.<br>
>> <br>
>>     Probably, this is a difficult technical problem that will be <br>
>> practically<br>
>>     solved during several years.<br>
>> <br>
>>     Regards,<br>
>> <br>
>>     -----<br>
>>     Sergei<br>
>> <br>
>> <br>
>> <br>
>>     >> There are type systems overlayed on top of initially untyped<br>
>>     >> languages (e.g. the language of Alloy Analyzer) and there are<br>
>>     >> gradual types and designs like TypeScript for to initially <br>
>> untyped<br>
>>     >> programming languages. ACL2 theorem prover for pure LISP, SPASS<br>
>>     >> theorem prover for first-order logic, and "TLA+ model checking <br>
>> made<br>
>>     >> symbolic" model checker for TLA+ all include techniques to <br>
>> recover<br>
>>     >> types from an initially untyped language.<br>
>>     >><br>
>>     >> Best regards,<br>
>>     >><br>
>>     >> Viktor<br>
>>     >><br>
>>     >> On Tue, Mar 3, 2020 at 8:44 PM Jason Gross <br>
>> <<a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a><br>
>>     <mailto:<a href="mailto:jasongross9@gmail.com" target="_blank">jasongross9@gmail.com</a>>><br>
>>     >> wrote:<br>
>>     >><br>
>>     >>> I'm in the process of writing my thesis on proof assistant<br>
>>     >>> performance bottlenecks (with a focus on Coq), and there's a <br>
>> large<br>
>>     >>> class of performance bottlenecks that come from (mis)using the<br>
>>     >>> power of dependent types.  So in writing the introduction, I <br>
>> want<br>
>>     >>> to provide some justification for the design decision of using<br>
>>     >>> dependent types, rather than, say, set theory or classical <br>
>> logic<br>
>>     >>> (as in, e.g., Isabelle/HOL).  And the only reasons I can come <br>
>> up<br>
>>     >>> with are "it's fun" and "lots of people do it"<br>
>>     >>><br>
>>     >>> So I'm asking these mailing lists: why do we base proof <br>
>> assistants<br>
>>     >>> on dependent type theory?  What are the trade-offs involved?<br>
>>     >>> I'm interested both in explanations and arguments given on <br>
>> list,<br>
>>     >>> as well as in references to papers that discuss these sorts of<br>
>>     >>> choices.<br>
>>     >>><br>
>>     >>> Thanks,<br>
>>     >>> Jason<br>
>>     > _______________________________________________<br>
>>     > Agda mailing list<br>
>>     > <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<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/mailman/listinfo/agda</a><br>
>> <br>
<br>
_______________________________________________<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/mailman/listinfo/agda</a><br>
</blockquote></div></div>