[Haskell-cafe] type and data constructors in CT
Gregg Reynolds
dev at mobileink.com
Sat Jan 31 15:54:01 EST 2009
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 ?
> 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)? 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?
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
>
>
More information about the Haskell-Cafe
mailing list