[Agda] [Coq-Club] Why dependent type theory?

[Ralf Jung]

My first guess would that this has something to do with the exponential blow-up
that I discussed in
<https://www.ralfj.de/blog/2019/05/15/typeclasses-exponential-blowup.html>.

; Ralf

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

-- 
Website: https://people.mpi-sws.org/~jung/