On Sat, Jan 31, 2009 at 12:00 PM, Gregg Reynolds
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.
What sort of relationship are you expecting? Type constructors and data constructors are injective functions, and the language takes advantage of that in various ways. (E.g., type constructors are allowed, but not general type functions. Data constructors support pattern-matching.) Aside from playing analogous roles and having similar names, I'm not sure there is a deeper relationship.
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.
If Hask is the category of Haskell types and functions, and |Hask| is the discrete category of Haskell types and (only) identity functions, then you can model a type constructor of kind * -> * as a functor from |Hask| to Hask. There's a paper about defining catamorphisms for GADTs and nested recursive types that models type constructors that way.
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.
Sure. If nothing else, any set can be made into a discrete category, and functors from discrete categories are basically functions.
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.
Again, what sort of relationship are you thinking of? Data
constructors always construct values of types of kind *, and people
discussing type constructors are usually talking about kinds at least
as complex as * -> *.
--
Dave Menendez