[Agda] Re: Forall and product

[Peter Selinger]

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