[Haskell-cafe] Categorical description of systems with dependent
types  Dan Doel dan.doel at gmail.com Fri Dec 3 02:43:35 CET
2010  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 prog