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

[Jason Gross]

> 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> 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 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> 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
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200303/2908c238/attachment.html>