[Agda] [lean-user] Why dependent type theory?

[Scott Morrison]

The paper http://home.in.tum.de/~immler/documents/immler2018manifolds.pdf has
some interesting discussion of the difficulty they had with the lack of
dependent types in setting up the basics of differential geometry in
Isabell/HOL:

> Following this approach, we avoid the need to define the type R^n
> parametrized by a natural number n, which is impossible in Isabelle/HOL’s
> simple type theory.

Kevin Buzzard makes an interesting challenge at
https://xenaproject.wordpress.com/2020/02/09/where-is-the-fashionable-mathematics/
to non-dependently typed theorem provers:

> Does this mean that there are entire areas of mathematics which are off
> limits to his system? I conjecture yes. Prove me wrong. Can you define the
> Picard group of a scheme in Isabelle/HOL? I am not sure that it is even
> possible to write this code in Isabelle/HOL in such a way that it will run in
> finite time, because you have to take a tensor product of sheaves of modules
> to define the multiplication, and a sheaf is a dependent type, and your clever
> HOL workarounds will not let you use typeclasses to define module structures
> on the modules which are values of the sheaves.

(We don't have the Picard group of a scheme in _any_ theorem prover, today, as
(far as I'm aware.)

I won't say that Lean and Coq "come naturally" to mathematicians (having to
learn intricacies such as typeclass resolution, and having 4 or 5 different
types of brackets, are not selling points), but even though mathematicians
don't officially know anything about type theory, in practice they already
understand dependent types very well, but would be horrified to have to do
without them.

best regards,
Scott Morrison

On Tue, Mar 3, 2020 at 11:44 AM 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
>
> --
> You received this message because you are subscribed to the Google Groups "lean-user" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to lean-user+unsubscribe at googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/lean-user/CAKObCaqa5NZvJvU_ZpZek%2BOnVEOQETiYpisbgJXhPchMn6PLcQ%40mail.gmail.com.