Re: [Haskell-cafe] type and data constructors in CT

On 31 Jan 2009, at 20:54, Gregg Reynolds wrote:

On Sat, Jan 31, 2009 at 1:02 PM, Ben Moseley wrote:

...

You can view a polymorphic unary type constructor of type ":: a -> T" as a polymorphic function.

Shouldn't that be * :: a -> T a ?

Yes, you're right. And when I say "polymorphic unary type constructor" I really mean "polymorphic unary /data/ constructor" ...

...

In general, polymorphic functions correspond roughly to natural transformations (in this case from the identity functor to T).

Are you saying a type constructor is a nat trans and not a functor (component)?

Nope ... what I was trying to say is that the data constructor bit is like a nat trans. (You're right that a unary type constructor often does correspond to a functor - providing there's a corresponding arrow/ function component).

Seems much more like a plain ol' functor mapping of object to object to me - the objects being types. Can you clarify what you mean about the correspondence with natural transformations?

So, the idea is that any polymorphic Haskell function (including Data constructors) can be seen as a natural transformation - so a "function" from any object (ie type) to an arrow (ie function). So, take "listToMaybe :: [a] -> Maybe a" ... this can be seen as a natural transformation from the List functor ([] type constructor) to the Maybe functor (Maybe type constructor) which is a "function" from any type "a" (eg 'Int') to an arrow (ie Haskell function) eg "listToMaybe :: [Int] -> Maybe Int". Hope that makes somewhat more sense. Cheers, --Ben

I admit I haven't thought through "polymorphic function", mainly because there doesn't seem to be any such beast in category theory, and to be honest I've always thought the metaphor is misleading. After all, a function by definition cannot be polymorphic. It seems like fancy name for a syntactic convenience to me - a way to express /intensionally/ a set of equations without writing them all out explicitly.

Thanks,

gregg

...

--Ben

On 31 Jan 2009, at 17:00, 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.

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.

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.

If somebody could point me in the right direction I'd be grateful. Might even write a tutorial. Can't have too many of those.

Thanks,

Gregg _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe