<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:"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;}
@font-face
{font-family:AgmenaPro-Regular;
panose-1:2 11 6 4 2 2 2 2 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:blue;
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";}
span.apple-converted-space
{mso-style-name:apple-converted-space;}
span.HTMLPreformattedChar
{mso-style-name:"HTML Preformatted Char";
mso-style-priority:99;
mso-style-link:"HTML Preformatted";
font-family:Consolas;}
span.EmailStyle21
{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;}
--></style>
</head>
<body lang="EN-GB" link="blue" vlink="purple">
<div class="WordSection1">
<p class="MsoNormal"><span style="mso-fareast-language:EN-US">Hi Ettore,<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">In set theory the union of two sets (written \cup) is the set which contains the elements which are in one set or the other. Hence I cannot see what is “mathematically incorrect” in my example<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">Cheers,<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"><b><span style="font-size:12.0pt;color:black">From: </span></b><span style="font-size:12.0pt;color:black">Ettore Aldrovandi <ealdrov@math.fsu.edu><br>
<b>Date: </b>Wednesday, 4 March 2020 at 21:59<br>
<b>To: </b>Thorsten Altenkirch <psztxa@exmail.nottingham.ac.uk><br>
<b>Cc: </b>"coq-club@inria.fr" <coq-club@inria.fr>, 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: [Agda] [Coq-Club] Why dependent type theory?<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">Hi, <o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">I think the example below is not mathematically correct. The problem is that \cup is not the same as \sqcup. The latter is of course a coproduct in the category of sets, whereas the former is a push-out, so a colimit of a more complicated
diagram. In the line <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<p class="MsoNormal" style="text-indent:36.0pt">{0,1} \cup {0,1,2,3} = {0,1,2,3}<o:p></o:p></p>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">of course the two sets {0,1} and {0,1,2,3} are not disjoint, whereas in the line <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<p class="MsoNormal" style="text-indent:36.0pt">{true , false} \cup {0,1,2,3} = {true,false,0,1,2,3}<o:p></o:p></p>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">the union is actually disjoint, i.e. a coproduct. In the example with the sum, <o:p></o:p></p>
</div>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<p class="MsoNormal" style="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>
</div>
<div>
<p class="MsoNormal" style="text-indent:36.0pt"><span lang="DE"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="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>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">in the first line {0,1} is actually made disjoint from {0,1,2,3}. To turn this around, suppose you do a push-out<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">{true, false} \coprod_{0,1} {0,1,2,3}<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">where you use the maps f : {0,1} -> {true, false} and i : {0,1} ->{0,1,2,3} . Then, since f is an isomorphism, you get something isomorphic to the union. <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">So, this example doesn’t really show that \cup exposes the implementation. But part of this example becomes possible because in sets we have naively “disembodied” elements leading to constructions of this sort…<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">…I guess, I’m just learning this stuff myself. (First post here, actually!)<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Best,<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">—Ettore<o:p></o:p></p>
</div>
<div>
<div>
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<p class="MsoNormal">On Mar 4, 2020, at 04:42, Thorsten Altenkirch <<a href="mailto:Thorsten.Altenkirch@nottingham.ac.uk">Thorsten.Altenkirch@nottingham.ac.uk</a>> wrote:<o:p></o:p></p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal">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.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">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>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="text-indent:36.0pt">{0,1} \cup {0,1,2,3} = {0,1,2,3}<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="text-indent:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">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>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="text-indent:36.0pt">{true , false} \cup {0,1,2,3} = {true,false,0,1,2,3}<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">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<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="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>
</div>
<div>
<p class="MsoNormal" style="text-indent:36.0pt"><span lang="DE"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="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>
</div>
<div>
<p class="MsoNormal"><span lang="DE"> </span><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">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>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">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>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">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>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">Thorsten<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="text-indent:36.0pt"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> <o:p></o:p></p>
</div>
<div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<div style="margin-left:36.0pt">
<p class="MsoNormal"><b><span style="font-size:12.0pt">From:<span class="apple-converted-space"> </span></span></b><span style="font-size:12.0pt">"<a href="mailto:coq-club-request@inria.fr"><span style="color:#954F72">coq-club-request@inria.fr</span></a>" <<a href="mailto:coq-club-request@inria.fr"><span style="color:#954F72">coq-club-request@inria.fr</span></a>>
on behalf of Jason Gross <<a href="mailto:jasongross9@gmail.com"><span style="color:#954F72">jasongross9@gmail.com</span></a>><br>
<b>Reply to:<span class="apple-converted-space"> </span></b>"<a href="mailto:coq-club@inria.fr"><span style="color:#954F72">coq-club@inria.fr</span></a>" <<a href="mailto:coq-club@inria.fr"><span style="color:#954F72">coq-club@inria.fr</span></a>><br>
<b>Date:<span class="apple-converted-space"> </span></b>Tuesday, 3 March 2020 at 19:44<br>
<b>To:<span class="apple-converted-space"> </span></b>coq-club <<a href="mailto:coq-club@inria.fr"><span style="color:#954F72">coq-club@inria.fr</span></a>>, agda-list <<a href="mailto:agda@lists.chalmers.se"><span style="color:#954F72">agda@lists.chalmers.se</span></a>>,
"<a href="mailto:coq+miscellaneous@discoursemail.com"><span style="color:#954F72">coq+miscellaneous@discoursemail.com</span></a>" <<a href="mailto:coq+miscellaneous@discoursemail.com"><span style="color:#954F72">coq+miscellaneous@discoursemail.com</span></a>>,
lean-user <<a href="mailto:lean-user@googlegroups.com"><span style="color:#954F72">lean-user@googlegroups.com</span></a>><br>
<b>Subject:<span class="apple-converted-space"> </span></b>[Coq-Club] Why dependent type theory?</span><o:p></o:p></p>
</div>
</div>
<div>
<div style="margin-left:36.0pt">
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div style="margin-left:36.0pt">
<p class="MsoNormal">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"<span class="apple-converted-space"> </span><o:p></o:p></p>
</div>
<div>
<div style="margin-left:36.0pt">
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div style="margin-left:36.0pt">
<p class="MsoNormal">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>
<div>
<div style="margin-left:36.0pt">
<p class="MsoNormal">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>
<div>
<div style="margin-left:36.0pt">
<p class="MsoNormal"> <o:p></o:p></p>
</div>
</div>
<div>
<div style="margin-left:36.0pt">
<p class="MsoNormal">Thanks,<o:p></o:p></p>
</div>
</div>
<div>
<div style="margin-left:36.0pt">
<p class="MsoNormal">Jason<o:p></o:p></p>
</div>
</div>
</div>
<pre style="caret-color: rgb(0, 0, 0);font-variant-caps: normal;text-align:start;-webkit-text-stroke-width: 0px;word-spacing:0px"><span style="font-size:10.5pt">This message and any attachment are intended solely for the addressee<o:p></o:p></span></pre>
<pre><span style="font-size:10.5pt">and may contain confidential information. If you have received this<o:p></o:p></span></pre>
<pre><span style="font-size:10.5pt">message in error, please contact the sender and delete the email and<o:p></o:p></span></pre>
<pre><span style="font-size:10.5pt">attachment. <o:p></o:p></span></pre>
<pre><span style="font-size:10.5pt"><o:p> </o:p></span></pre>
<pre><span style="font-size:10.5pt">Any views or opinions expressed by the author of this email do not<o:p></o:p></span></pre>
<pre><span style="font-size:10.5pt">necessarily reflect the views of the University of Nottingham. Email<o:p></o:p></span></pre>
<pre><span style="font-size:10.5pt">communications with the University of Nottingham may be monitored <o:p></o:p></span></pre>
<pre><span style="font-size:10.5pt">where permitted by law.<o:p></o:p></span></pre>
<pre><span style="font-size:10.5pt"><o:p> </o:p></span></pre>
<pre><span style="font-size:10.5pt"><o:p> </o:p></span></pre>
<pre><span style="font-size:10.5pt"><o:p> </o:p></span></pre>
<p class="MsoNormal"><span style="font-size:10.5pt;font-family:"AgmenaPro-Regular",serif">_______________________________________________<br>
Agda mailing list<br>
</span><a href="mailto:Agda@lists.chalmers.se"><span style="font-size:10.5pt;font-family:"AgmenaPro-Regular",serif;color:#954F72">Agda@lists.chalmers.se</span></a><span style="font-size:10.5pt;font-family:"AgmenaPro-Regular",serif"><br>
</span><a href="https://lists.chalmers.se/mailman/listinfo/agda"><span style="font-size:10.5pt;font-family:"AgmenaPro-Regular",serif;color:#954F72">https://lists.chalmers.se/mailman/listinfo/agda</span></a><o:p></o:p></p>
</div>
</blockquote>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</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>