On Sat, 2009-01-31 at 11:00 -0600, Gregg Reynolds wrote:
Hi,
I think I've finally figured out what a monad is, but there's one thing I haven't seen addressed in category theory stuff I've found online. That is the relation between type constructors and data constructors.
The typical (albeit incomplete) view is that data constructors are the (components of the) initial algebra of the functor corresponding to the signature of a given algebraic data type. This is discussed in quite a few places online.
As I understand it, a type constructor Tcon a is basically the object component of a functor T that maps one Haskell type to another. Haskell types are construed as the objects of category "HaskellType". I think that's a pretty straightforward interpretation of the CT definition of functor.
But a data constructor Dcon a is an /element/ mapping taking elements (values) of one type to elements of another type. So it too can be construed as a functor, if each type itself is construed as a category.
What are "elements" of a type? How are you "construing a type as a category"? One answer is that you are viewing types as sets. Ignoring the problems with that identification, a set can be viewed as a discrete category and functors between discrete categories are just functions. This is like going around three sides of a square; you don't gain anything over just saying "types are sets, and functions are set functions." Note that there is nothing special about data constructors here. Every function between types is such a functor. Most articles that apply CT to Haskell take one of two approaches. They either talk about a category of Haskell types and functions with no explanation of what those "actually" are, i.e. the understanding that it behaves like (idealized) Haskell, or they refer to some existing approach to (idealized) semantics, e.g. sets or domains. In either case, the meaning of the objects and arrows is effectively taken for granted. An approach along the lines you are suggesting would be useful for a categorical semantics of Haskell, but it would just be one possible semantics among many. For most of the aforementioned articles, the only value of such a thing would be to be able to formally prove that the constructions talked about exist (except that they usually don't for technical reasons.) Usually in those articles, the readers are assumed to know Haskell and to not know much about category theory, so trying to explain types and functions to them categorically is unnecessary and obfuscatory. It would make sense if you were going the other way, explaining Haskell to categorists.
So this gives us two functors, but they operate on different things, and I don't see how to get from one to the other in CT terms. Or rather, they're obviously related, but I don't see how to express that relation formally.
One way to do this would be to use indexed categories or more generally two categories.