[Haskell-cafe] type and data constructors in CT

[Ben Moseley]

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

> On Sat, Jan 31, 2009 at 1:02 PM, Ben Moseley <ben_moseley at mac.com>  
> 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 at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>