On Thursday 02 December 2010 7:54:18 pm Larry Evans wrote:
[snip] *Maybe* the computer science people are trying to minimize the concepts. In this case, the one concept common to both the sum and product ( in the math peoples viewpoint) is there's a function:
field2type: field_name -> Type
in the case of a product or record, r, it's:
product = f:fieldname -> field2type(f)
in the case of a disjoint sum its:
sum = (f:fieldname, field2type(f))
or something like that.
I'll be honest: I don't really know what you're saying above. However, I can throw in my 2 cents on the naming thing. The product-function naming obviously comes from thinking about, "what if the type of later arguments of a tuple could depend on earlier ones, and what if the result type of a function could depend on the argument?" These are quite ordinary questions for a practicing programmer to think about, which is probably why computer science people (supposedly) favor this naming. I might even use this naming myself when appropriate, although I'd say 'tuple' (or record) instead of 'product' to (hopefully) avoid confusion. The sum-product naming, by contrast, comes from thinking about, "we have n-ary sums and products for any natural n; for instance, A + B and A * B are binary. This can be viewed as sums and products of families of types indexed by finite sets. What if we generalize this to sums and products of families indexed by *arbitrary* types?" Unlike the above, I don't think this is something that is likely to be sparked naturally during programming. However, it's quite close to similar constructions in set theory, which probably explains why mathematicians favor it. If you get into category theoretic views of programming languages, I think the sum-product naming makes sense there, and it's hard to make the product- function naming work. For instance: The A-indexed product Π x:A. F[x] has an A-indexed family of projections: proj a : (Π x:A. F[x]) -> F[a] The A-indexed sum Σ x:A. F[x] has an A-indexed family of injections: in a : F[a] -> (Σ x:A. F[x]) Which are visibly generalizations of the definitions of (co)products you'd encounter modelling non-dependently typed languages. Perhaps this is on the math end of things, though. -- Dan