[Haskell-cafe] type and data constructors in CT
Ben Moseley
ben_moseley at mac.com
Sun Feb 1 09:26:15 EST 2009
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
>>
>>
More information about the Haskell-Cafe
mailing list