On 31 Jan 2009, at 20:54, Gregg Reynolds wrote:
On Sat, Jan 31, 2009 at 1:02 PM, Ben Moseley <[email protected]>
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
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
