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

[Jeremy Avigad]

Dear all,

A long time ago I wrote a mathematician's perspective on why dependent type
theory is useful for formalizing mathematics:

  http://bulletin.eatcs.org/index.php/beatcs/article/view/81

When I wrote it, I was a newbie to DTT, on sabbatical in France working on
the formalization of the Feit Thompson theorem. (It was like a school
report, "what I did on my sabbatical.")

More recently I have given some survey talks along these lines:

  http://www.andrew.cmu.edu/user/avigad/Talks/fields_type_theory.pdf
  http://www.andrew.cmu.edu/user/avigad/Talks/san_diego.pdf

The first was meant for a general audience of mathematicians and logicians,
the second for a general audience of mathematicians. There is also a
discussion of DTT starting on slide 40 here, with a nice quotation from a
core mathematician, Sébastien Gouëzel:

  http://www.andrew.cmu.edu/user/avigad/Talks/london.pdf

You can still find the quotation on his web page. There is an excellent
paper by Kevin Buzzard, Johan Commelin, and Patrick Massot, on formalizing
perfectoid spaces:

  https://arxiv.org/pdf/1910.12320.pdf

The last paragraph of the first page addresses the importance of DTT.

The short story is that some sort of dependent type theory is useful, and
possibly indispensable, for formalizing mathematics. But it also brings a
lot of headaches, so it is best to use it judiciously. Mathematics don't
care about inductively defined structures beyond the natural numbers, and
don't really care much for elaborate forms of induction and recursion. But
dealing with all kinds of structures and morphisms between them is
absolutely essential, and often these structures depend on parameters. Any
reasonable system for formalizing mathematics has to provide mechanisms to
support reasoning about them.

Best wishes,

Jeremy








On Wed, Mar 4, 2020 at 6:29 AM Dominique Unruh <unruh at ut.ee> wrote:

> Hi,
>
> following up with Thorsten's command about the word "dependent type
> theory", I would like to add a few observations I had in this discussion:
>
>    - I think the word "type theory" itself is unclear in this context. At
>    least several of the emails seem to use different but related ideas of what
>    that means:
>       - It could mean "something where everything has a type" (i.e., not
>       the usual ZF). Then HOL would be type theory. (Thorsten's email quoted
>       below makes sense in that setting because HOL avoids the problem described
>       there.)
>       - It could mean the above with dependent types (but not necessary
>       the Curry-Howard thing from the next item)
>       - It could mean "a system where we use the same language for
>       propositions and proofs via Curry-Howard isomorphism" (I believe this will
>       then also need dependent types since otherwise the proof terms are not
>       powerful enough)
>       - It could mean a system with strong normalization (so that
>       everything terminates), at least some of the answers seem to see this as
>       part of the meaning of "type theory".
>
> Of course, there are many interaction between the different concepts, but
> if we talk about the costs or benefits of adopting type theory, it becomes
> quite important which aspect of it we are adopting. (E.g., if we have, say,
> a good reason why we need the second point, and a big cost for getting the
> four point, then it is important not to just say "type theory has the
> following good reason and the following cost".)
>
> Maybe when discussing *why* type theory, we should prefix our answers by
> what we mean by type theory (e.g., one of the above). Otherwise it will be
> very confusing (at least to me).
>
> Another question is also the context in which we want to use it:
>
>    - Programming (with all the associated things like verification, type
>    checking, etc.)
>    - Math
>
> These have different requirements, so making explicit which domain we are
> thinking of in our answer might make things clearer as well.
>
> Just my personal thoughts, but I hope they may help to add some clarity to
> the discussion.
>
> Best wishes,
> Dominique.
>
>
>
> On 3/4/20 11:42 AM, Thorsten Altenkirch wrote:
>
> First of all I don’t like the word “dependent type theory”. Dependent
> types are one important feature of modern Type Theory but hardly the only
> one.
>
>
>
> To me the most important feature of Type Theory is the support of
> abstraction in Mathematics and computer science. Using  types instead of
> sets means that you can hide implementation choices which is essential if
> you want to build towers of abstraction. Set theory fails here badly. Just
> as a very simple example: in set theory you have the notion of union, so
> for example
>
>
>
> {0,1}  \cup {0,1,2,3} = {0,1,2,3}
>
>
>
> However, if we change the representation of the first set and use lets say
> {true,false} we get a different result:
>
>
>
> {true , false}  \cup {0,1,2,3} = {true,false,0,1,2,3}
>
>
>
> This means that \cup exposes implementation details because the results
> are not equivalent upto renaming. In Type Theory we have the notion of sum,
> sometimes called disjoint union, which is well behaved
>
>
>
> {0,1}  + {0,1,2,3} = {in1 0,in1 1,in2 0,in2 1,in2 2,in2 3}
>
>
>
> {true , false}  + {0,1,2,3} = {in1 true,in1 false ,in2 0,in2 1,in2 2,in2 3}
>
>
>
> Unlike \cup, + doesn’t reveal any implementation details it is a purely
> structural operation. Having only structural operations means that
> everything you do is stable under equivalence, that is you can replace one
> object with another one that behaves the same. This is the essence of
> Voevodsky’s univalence principle.
>
>
>
> There are other nice aspects of Type Theory. From a constructive point of
> view (which should come naturally to a computer scientists) the
> proporsitions as types explanation provides a very natural way to obtain
> “logic for free” and paedagogically helpful since it reduces logical
> reasoning to programming.
>
>
>
> There are performance issues with implementations of Type Theory, however,
> in my experience (mainly agda) the execution of functions at compile time
> isn’t one of them. In my experience the main problem is to deal with a loss
> of sharing when handling equational constraints which can blow up the time
> needed for type checking. I think this is an engineering problem and there
> are some suggestions how to fix this.
>
>
>
> Thorsten
>
>
>
>
>
>
>
> *From: *"coq-club-request at inria.fr" <coq-club-request at inria.fr>
> <coq-club-request at inria.fr> <coq-club-request at inria.fr> on behalf of
> Jason Gross <jasongross9 at gmail.com> <jasongross9 at gmail.com>
> *Reply to: *"coq-club at inria.fr" <coq-club at inria.fr> <coq-club at inria.fr>
> <coq-club at inria.fr>
> *Date: *Tuesday, 3 March 2020 at 19:44
> *To: *coq-club <coq-club at inria.fr> <coq-club at inria.fr>, agda-list
> <agda at lists.chalmers.se> <agda at lists.chalmers.se>,
> "coq+miscellaneous at discoursemail.com"
> <coq+miscellaneous at discoursemail.com>
> <coq+miscellaneous at discoursemail.com>
> <coq+miscellaneous at discoursemail.com>, lean-user
> <lean-user at googlegroups.com> <lean-user at googlegroups.com>
> *Subject: *[Coq-Club] Why dependent type theory?
>
>
>
> 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
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200304/92c9cd9e/attachment.html>