[Agda] [Coq-Club] Why dependent type theory? (resend)

[Thorsten Altenkirch]

First of all there is a difference between “type theory” and “Type Theory”.

The former refers to the theory of types as used in programming while the latter refers to type theory within the tradition started by Per Martin-Loef, incorporating among others concepts dependent types, universes, inductive types, etc. Now it is correct to say that using capital letters cannot hide the fact that there is more than one instance of Type Theory because it is an evolving concept. However, the same applies to set theory, there are many variants of it and in a discussion you may have to state to which one you refer.

However, as for set theory, there are some remarks you can make about “Type Theory” in general and then it is not necessary to make an exact reference to a particular formal system. In my email I made some general remarks but then referred to univalence which refers to Homotopy Type Theory, again there is more then one formal system but at least it narrows down the scope.

Thorsten

From: Dominique Unruh <unruh at ut.ee>
Date: Wednesday, 4 March 2020 at 11:25
To: "coq-club at inria.fr" <coq-club at inria.fr>, Thorsten Altenkirch <psztxa at exmail.nottingham.ac.uk>, agda-list <agda at lists.chalmers.se>, "coq+miscellaneous at discoursemail.com" <coq+miscellaneous at discoursemail.com>, lean-user <lean-user at googlegroups.com>
Subject: Re: [Coq-Club] Why dependent type theory?


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:
o    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.)
o    It could mean the above with dependent types (but not necessary the Curry-Howard thing from the next item)
o    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)
o    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.





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/b691b8ec/attachment.html>