<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:Wingdings;
panose-1:5 0 0 0 0 0 0 0 0 0;}
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:Consolas;
panose-1:2 11 6 9 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#0563C1;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:#954F72;
text-decoration:underline;}
pre
{mso-style-priority:99;
mso-style-link:"HTML Preformatted Char";
margin:0cm;
margin-bottom:.0001pt;
font-size:10.0pt;
font-family:"Courier New";}
p.msonormal0, li.msonormal0, div.msonormal0
{mso-style-name:msonormal;
mso-margin-top-alt:auto;
margin-right:0cm;
mso-margin-bottom-alt:auto;
margin-left:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
span.EmailStyle19
{mso-style-type:personal;
font-family:"Calibri",sans-serif;
color:windowtext;}
span.HTMLPreformattedChar
{mso-style-name:"HTML Preformatted Char";
mso-style-priority:99;
mso-style-link:"HTML Preformatted";
font-family:"Consolas",serif;}
span.EmailStyle22
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
/* List Definitions */
@list l0
{mso-list-id:69550554;
mso-list-template-ids:456150978;}
@list l0:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:36.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l0:level2
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:72.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:"Courier New";
mso-bidi-font-family:"Times New Roman";}
@list l0:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:108.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:144.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level5
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:180.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:216.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:252.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level8
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:288.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l0:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:324.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1
{mso-list-id:178591015;
mso-list-template-ids:915202802;}
@list l1:level1
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:36.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Symbol;}
@list l1:level2
{mso-level-number-format:bullet;
mso-level-text:o;
mso-level-tab-stop:72.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:"Courier New";
mso-bidi-font-family:"Times New Roman";}
@list l1:level3
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:108.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level4
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:144.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level5
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:180.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level6
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:216.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level7
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:252.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level8
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:288.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
@list l1:level9
{mso-level-number-format:bullet;
mso-level-text:;
mso-level-tab-stop:324.0pt;
mso-level-number-position:left;
text-indent:-18.0pt;
mso-ansi-font-size:10.0pt;
font-family:Wingdings;}
ol
{margin-bottom:0cm;}
ul
{margin-bottom:0cm;}
--></style>
</head>
<body lang="EN-GB" link="#0563C1" vlink="#954F72">
<div class="WordSection1">
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">First of all there is a difference between “type theory” and “Type Theory”.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">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.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">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.<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Thorsten<o:p></o:p></span></p>
<p class="MsoNormal"><span style="mso-fareast-language:EN-US"><o:p> </o:p></span></p>
<div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal" style="margin-left:36.0pt"><b><span style="font-size:12.0pt;color:black">From:
</span></b><span style="font-size:12.0pt;color:black">Dominique Unruh <unruh@ut.ee><br>
<b>Date: </b>Wednesday, 4 March 2020 at 11:25<br>
<b>To: </b>"coq-club@inria.fr" <coq-club@inria.fr>, Thorsten Altenkirch <psztxa@exmail.nottingham.ac.uk>, agda-list <agda@lists.chalmers.se>, "coq+miscellaneous@discoursemail.com" <coq+miscellaneous@discoursemail.com>, lean-user <lean-user@googlegroups.com><br>
<b>Subject: </b>Re: [Coq-Club] Why dependent type theory?<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<p style="margin-left:36.0pt">Hi,<o:p></o:p></p>
<p style="margin-left:36.0pt">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:<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:72.0pt;text-indent:-18.0pt;mso-list:l1 level1 lfo1">
<![if !supportLists]><span style="font-size:10.0pt;font-family:Symbol"><span style="mso-list:Ignore">·<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]>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:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:108.0pt;text-indent:-18.0pt;mso-list:l1 level2 lfo1">
<![if !supportLists]><span style="font-size:10.0pt;font-family:"Courier New""><span style="mso-list:Ignore">o<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]>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:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:108.0pt;text-indent:-18.0pt;mso-list:l1 level2 lfo1">
<![if !supportLists]><span style="font-size:10.0pt;font-family:"Courier New""><span style="mso-list:Ignore">o<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]>It could mean the above with dependent types (but not necessary the Curry-Howard thing from the next item)<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:108.0pt;text-indent:-18.0pt;mso-list:l1 level2 lfo1">
<![if !supportLists]><span style="font-size:10.0pt;font-family:"Courier New""><span style="mso-list:Ignore">o<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]>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:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:108.0pt;text-indent:-18.0pt;mso-list:l1 level2 lfo1">
<![if !supportLists]><span style="font-size:10.0pt;font-family:"Courier New""><span style="mso-list:Ignore">o<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]>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".<o:p></o:p></p>
<p style="margin-left:36.0pt">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".)<o:p></o:p></p>
<p style="margin-left:36.0pt">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).<o:p></o:p></p>
<p style="margin-left:36.0pt">Another question is also the context in which we want to use it:<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:72.0pt;text-indent:-18.0pt;mso-list:l0 level1 lfo2">
<![if !supportLists]><span style="font-size:10.0pt;font-family:Symbol"><span style="mso-list:Ignore">·<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]>Programming (with all the associated things like verification, type checking, etc.)<o:p></o:p></p>
<p class="MsoNormal" style="mso-margin-top-alt:auto;mso-margin-bottom-alt:auto;margin-left:72.0pt;text-indent:-18.0pt;mso-list:l0 level1 lfo2">
<![if !supportLists]><span style="font-size:10.0pt;font-family:Symbol"><span style="mso-list:Ignore">·<span style="font:7.0pt "Times New Roman"">
</span></span></span><![endif]>Math<o:p></o:p></p>
<p style="margin-left:36.0pt">These have different requirements, so making explicit which domain we are thinking of in our answer might make things clearer as well.<o:p></o:p></p>
<p style="margin-left:36.0pt">Just my personal thoughts, but I hope they may help to add some clarity to the discussion.<o:p></o:p></p>
<p style="margin-left:36.0pt">Best wishes,<br>
Dominique.<o:p></o:p></p>
<p style="margin-left:36.0pt"><o:p> </o:p></p>
<p style="margin-left:36.0pt"><o:p> </o:p></p>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">On 3/4/20 11:42 AM, Thorsten Altenkirch wrote:<o:p></o:p></p>
</div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal" style="margin-left:36.0pt"><span style="mso-fareast-language:EN-US">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.</span><o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="mso-fareast-language:EN-US"> </span><o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt">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
<o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:36.0pt">{0,1} \cup {0,1,2,3} = {0,1,2,3}<o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:36.0pt"> <o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt">However, if we change the representation of the first set and use lets say {true,false} we get a different result:<o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:36.0pt">{true , false} \cup {0,1,2,3} = {true,false,0,1,2,3}<o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="mso-fareast-language:EN-US"> </span><o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="mso-fareast-language:EN-US">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</span><o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="mso-fareast-language:EN-US"> </span><o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:36.0pt"><span lang="DE">{0,1} + {0,1,2,3} = {in1 0,in1 1,in2 0,in2 1,in2 2,in2 3}</span><o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:36.0pt"><span lang="DE"> </span><o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:36.0pt"><span lang="DE">{true , false} + {0,1,2,3} = {in1 true,in1 false ,in2 0,in2 1,in2 2,in2 3}</span><o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span lang="DE"> </span><o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt">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.<o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt">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.<o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt">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.<o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt">Thorsten<o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt;text-indent:36.0pt"> <o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="mso-fareast-language:EN-US"> </span><o:p></o:p></p>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="mso-fareast-language:EN-US"> </span><o:p></o:p></p>
<div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal" style="margin-left:72.0pt"><b><span style="font-size:12.0pt;color:black">From:
</span></b><span style="font-size:12.0pt;color:black"><a href="mailto:coq-club-request@inria.fr">"coq-club-request@inria.fr"</a>
<a href="mailto:coq-club-request@inria.fr"><coq-club-request@inria.fr></a> on behalf of Jason Gross
<a href="mailto:jasongross9@gmail.com"><jasongross9@gmail.com></a><br>
<b>Reply to: </b><a href="mailto:coq-club@inria.fr">"coq-club@inria.fr"</a> <a href="mailto:coq-club@inria.fr">
<coq-club@inria.fr></a><br>
<b>Date: </b>Tuesday, 3 March 2020 at 19:44<br>
<b>To: </b>coq-club <a href="mailto:coq-club@inria.fr"><coq-club@inria.fr></a>, agda-list
<a href="mailto:agda@lists.chalmers.se"><agda@lists.chalmers.se></a>, <a href="mailto:coq+miscellaneous@discoursemail.com">
"coq+miscellaneous@discoursemail.com"</a> <a href="mailto:coq+miscellaneous@discoursemail.com">
<coq+miscellaneous@discoursemail.com></a>, lean-user <a href="mailto:lean-user@googlegroups.com">
<lean-user@googlegroups.com></a><br>
<b>Subject: </b>[Coq-Club] Why dependent type theory?</span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:72.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:72.0pt">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" <o:p></o:p></p>
<div>
<p class="MsoNormal" style="margin-left:72.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:72.0pt">So I'm asking these mailing lists: why do we base proof assistants on dependent type theory? What are the trade-offs involved?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:72.0pt">I'm interested both in explanations and arguments given on list, as well as in references to papers that discuss these sorts of choices.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:72.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:72.0pt">Thanks,<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:72.0pt">Jason<o:p></o:p></p>
</div>
</div>
<pre style="margin-left:36.0pt">This message and any attachment are intended solely for the addressee<o:p></o:p></pre>
<pre style="margin-left:36.0pt">and may contain confidential information. If you have received this<o:p></o:p></pre>
<pre style="margin-left:36.0pt">message in error, please contact the sender and delete the email and<o:p></o:p></pre>
<pre style="margin-left:36.0pt">attachment. <o:p></o:p></pre>
<pre style="margin-left:36.0pt"><o:p> </o:p></pre>
<pre style="margin-left:36.0pt">Any views or opinions expressed by the author of this email do not<o:p></o:p></pre>
<pre style="margin-left:36.0pt">necessarily reflect the views of the University of Nottingham. Email<o:p></o:p></pre>
<pre style="margin-left:36.0pt">communications with the University of Nottingham may be monitored <o:p></o:p></pre>
<pre style="margin-left:36.0pt">where permitted by law.<o:p></o:p></pre>
<pre style="margin-left:36.0pt"><o:p> </o:p></pre>
<pre style="margin-left:36.0pt"><o:p> </o:p></pre>
<pre style="margin-left:36.0pt"><o:p> </o:p></pre>
</blockquote>
</div>
<PRE>
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.
</PRE></body>
</html>