[Agda] Re: Forall and product

[Thorsten Altenkirch]

Ok, when we think of homogenous tuples AxA then this can also be
understood as a function 2 -> A. This also works for heterogenous tuples
like AxB using dependent functions Pi x:2.if x then A else B. However the
next logical step is Sigma x:A.B x, which have no good representations as
functions (unless we accept very dependent functions which in my mind goes
against the spirit of type theory). For this reason it seems to me that
the generalisation from -> to Pi and from x to Sigma is the primary one,
and the fact that tuples can be represented as functions is secondary.

Thorsten 


On 25/02/2015 23:03, "Peter Selinger" <selinger at mathstat.dal.ca> wrote:

>I hesitate to weigh in on this bikeshedding discussion
>(http://en.wikipedia.org/wiki/Bike_shed). Against my better judgement:
>
>I think most mathematicians and programmers are aware that tuples and
>functions are the same thing: a tuple is a function from indices to
>values, and conversely every function can be viewed as a tuple if one
>regards the domain as an index set. The point is not that one of these
>viewpoints is right and the other wrong, or that one is preferred by
>mathematicians and the other by programmers. Rather, there are
>situations where one may find it more natural to think in terms of
>tuples, and other situations when one may find it more natural to
>think in terms of functions.
>
>The terminology "cartesian product of a family of sets" goes more
>naturally with the tuple viewpoint, and the terminology "dependent
>function type" goes more naturally with the function viewpoint.
>Rather than trying to select one of these terminologies once and for
>all, surely it is enriching to use them both from time to time.
>
>The situation for Sigma-types is completely analogous. I think that
>most people understand that the elements of a disjoint union types are
>pairs (of an index and a value), and conversely, every set of pairs
>can be thought of in this way. Surely the terminologies "disjoint
>union of a family of sets" and "dependent pair type" are not only
>equivalent, but they each suggest a particular viewpoint that may or
>may not be a more natural way to look at a given problem.
>
>So I think all four terminologies have their legitimate uses.
>It's unfortunate that "dependent product" seems to be ambiguous, with
>about half the people thinking it should mean "cartesian product of a
>family of sets" and the other half "dependent pair type". (I'm in each
>camp about half of the time). I agree with Andreas that it may be best
>to avoid that terminology altogether.
>
>-- Peter
>
>Dan Doel wrote:
>> 
>> On Wed, Feb 25, 2015 at 3:26 AM, Andreas Abel <abela at chalmers.se> wrote:
>> 
>> > I guess programmers are more interested in whether something is a
>>pair or
>> > a function than in Descartes or families of sets.
>> >
>> 
>> ​If they are, then shouldn't they recognize that the sum type A + B is
>> inhabited by pairs? The values are pairs of a tag and ​a value of the
>> corresponding type. And sigma types internalize what you get to put in
>>the
>> tag portion of the pair.
>> 
>> Anyhow, I'm pretty sure I'm a programmer, but I've always used and liked
>> the sum-product terminology. I actually thought it was the more common
>> amongst people doing work on dependent type theory (although if you
>>want to
>> eliminate any chance of misinterpretation, "sigma type" and "pi type"
>>seem
>> safest, and serviceable). Maybe I'm a weird programmer, though.
>> 
>> -- Dan
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda





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 send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.