[Haskell-cafe] Categorical description of systems with dependent types

[Dan Doel]

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