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

[Ettore Aldrovandi]

Hi Thorsten,

of course you are correct about the union of  two sets (\cup). What I thought was not correct as an example is the comparison between \cup and +, because those are two different constructions, the latter being a disjoint union, or \sqcup, if we want to use a different notation. 

I think I agree with the idea that types help hide the implementation, but the example as a whole does not support it because of \cup vs. \sqcup. From a categorical viewpoint, those are different types of colimits. The union, as in the rest of my example, is a colimit along the index category  {* <- * -> *}, whereas the disjoint union is a colimit along { * *} .

I hope this clarifies it. Sorry for the confusion,

—Ettore


> On Mar 5, 2020, at 10:39, Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk <mailto:Thorsten.Altenkirch at nottingham.ac.uk>> wrote:
> 
> Hi Ettore,
>  
> 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
>  
> Cheers,
> Thorsten
>  
> From: Ettore Aldrovandi <ealdrov at math.fsu.edu <mailto:ealdrov at math.fsu.edu>>
> Date: Wednesday, 4 March 2020 at 21:59
> To: Thorsten Altenkirch <psztxa at exmail.nottingham.ac.uk <mailto:psztxa at exmail.nottingham.ac.uk>>
> Cc: "coq-club at inria.fr <mailto:coq-club at inria.fr>" <coq-club at inria.fr <mailto:coq-club at inria.fr>>, agda-list <agda at lists.chalmers.se <mailto:agda at lists.chalmers.se>>, "coq+miscellaneous at discoursemail.com <mailto:coq+miscellaneous at discoursemail.com>" <coq+miscellaneous at discoursemail.com <mailto:coq+miscellaneous at discoursemail.com>>, lean-user <lean-user at googlegroups.com <mailto:lean-user at googlegroups.com>>
> Subject: Re: [Agda] [Coq-Club] Why dependent type theory?
>  
> Hi,
>  
> 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 
>  
>> {0,1}  \cup {0,1,2,3} = {0,1,2,3}
>  
> of course the two sets {0,1} and {0,1,2,3} are not disjoint, whereas  in the line 
>  
>> {true , false}  \cup {0,1,2,3} = {true,false,0,1,2,3}
>  
> the union is actually disjoint, i.e. a coproduct. In the example with the sum, 
>  
>> {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}
>  
> 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
>  
> {true, false} \coprod_{0,1} {0,1,2,3}
>  
> 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. 
>  
> 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…
>  
> …I guess, I’m just learning this stuff myself. (First post here, actually!)
>  
> Best,
>  
> —Ettore
>  
> 
>> On Mar 4, 2020, at 04:42, Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk <mailto:Thorsten.Altenkirch at nottingham.ac.uk>> 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
> 
>  
> 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/20200305/2f775953/attachment.html>