<div dir="auto"><div>I'm confused by this.  Are you saying that in Agda typechecking is exponential in the number of files?  Or exponential in the number of nested abstractions?  Or something else?  Do you have a toy example demonstrating this behavior?<br><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Mar 3, 2020, 17:42  <<a href="mailto:mechvel@scico.botik.ru">mechvel@scico.botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On 2020-03-04 00:31, Jason Gross wrote:<br>
>> Which bottlenecks are you referring to? Are they intrinsically 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 only<br>
> one of my thesis) is the one that is due to the fact that arbitrary<br>
> conversion problems can happen during typechecking.  This is used to<br>
> great advantage in proof by reflection (where all of the work is done<br>
> in checking that a proof of "true = true" has the type "some-check =<br>
> true").  But it also causes performance issues if you're not careful.<br>
> To take a toy example, consider two different definitions of<br>
> factorial: n! = n * (n - 1)!, and n! = (n - 1)! * n.  Suppose you have<br>
> two different ways of computing a vector (length-indexed list) 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 of the<br>
> second factorial.  Suppose you now try to prove that the two methods<br>
> give the same result on any concrete list of length of length 10.<br>
> Just to check that this goal is valid, Coq is now trying to compute<br>
> 10! as a natural number.  This example is a bit contrived, but 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 ways.<br>
>  I have a real-world example where changing the input size just a<br>
> little bit caused `reflexivity` to take over 400 hours, rather 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" rel="noreferrer">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 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 in <br>
Coq too.<br>
I do not know of whether it is fundamental or technical. And I have not <br>
seen an answer to this question, so far. On practice, it looks like <br>
this:<br>
Agda can type-check only a small part of the computer algebra 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 algebra <br>
(where is known a constructive proof for each statement), say, of 500 <br>
pages, it will not be type-checked in 100 years.<br>
<br>
Probably, this is a difficult technical problem that will be 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 untyped<br>
>> programming languages. ACL2 theorem prover for pure LISP, SPASS<br>
>> theorem prover for first-order logic, and "TLA+ model checking made<br>
>> symbolic" model checker for TLA+ all include techniques to 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 <<a href="mailto:jasongross9@gmail.com" target="_blank" rel="noreferrer">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 large<br>
>>> class of performance bottlenecks that come from (mis)using the<br>
>>> power of dependent types.  So in writing the introduction, I want<br>
>>> to provide some justification for the design decision of using<br>
>>> dependent types, rather than, say, set theory or classical logic<br>
>>> (as in, e.g., Isabelle/HOL).  And the only reasons I can come 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 assistants<br>
>>> on dependent type theory?  What are the trade-offs involved?<br>
>>> I'm interested both in explanations and arguments given on 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" rel="noreferrer">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
</blockquote></div></div></div>