[Agda] Why dependent type theory?

[Ken Kubota]

Within type theory certain mathematical ideas can be expressed with dependent types only.

In particular, if the type of the result returned by a function depends on the argument, dependent types are required.
The example I chose is a function that returns the first unit vector of a given dimension: https://www.owlofminerva.net/files/formulae.pdf#page=12 <https://www.owlofminerva.net/files/formulae.pdf#page=12>


Let me quote from an earlier email available at https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ <https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ> :

But it is also clear that HOL's type system (and therefore Isabelle/HOL's type system) is poor.

Freek Wiedijk on the (current) HOL family: “There is one important reason why the HOLs are not yet attractive enough to be taken to be the QED system:
• The HOL type system is too poor. As we already argued in the previous section, it is too weak to properly do abstract algebra.
But it is worse than that. In the HOL type system there are no dependent types, nor is there any form of subtyping. (Mizar and Coq both have dependent types and some form of subtyping. In Mizar the subtyping is built into the type system. In Coq a similar effect is accomplished through the use of automatic coercions.)
For formal mathematics it is essential to both have dependent types and some form of subtyping.” [Wiedijk, 2007, p. 130, emphasis as in the original]
	https://owlofminerva.net/files/fom_2018.pdf#page=10 <https://owlofminerva.net/files/fom_2018.pdf#page=10>


For example, in HOL or Isabelle/HOL group theory cannot be expressed naturally (since type abstraction is missing), not even mentioning functions involving dependent types like that returning the first unit vector of a given dimension as mentioned above.


Note that there are also formulations of dependent type theory with classical foundations, see: https://owlofminerva.net/files/fom_2018.pdf#page=1 <https://owlofminerva.net/files/fom_2018.pdf#page=1>

I would consider type theory superior to set theory as type theory is a systematic approach, whereas the axioms of set theory are historically contingent.


Kind regards,

Ken Kubota

____________________________________________________


Ken Kubota
doi.org/10.4444/100 <https://doi.org/10.4444/100>



> Am 03.03.2020 um 20:43 schrieb Jason Gross <jasongross9 at gmail.com>:
> 
> 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/b8a82be1/attachment.html>