[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 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
More information about the Haskell-Cafe
mailing list