[Haskell-cafe] type and data constructors in CT
dev at mobileink.com
Sun Feb 1 11:27:57 EST 2009
On Sun, Feb 1, 2009 at 8:26 AM, Ben Moseley <ben_moseley at mac.com> wrote:
> 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".
Aha, hadn't thought of that. In other terms, a natural transformation
is how one gets from one lifted value to different lift of the same
value - from a lift to a hoist, as it were. Just calling it a
function doesn't do it justice. Very enlightening, thanks.
I'm beginning to think Category Theory is just about the coolest thing
since sliced bread. If I understand correctly, we can "represent" a
data constructor in two ways (at least):
qua functor: Dcon : a -> T a
qua nat trans Dcon : Id a -> T a
and thanks to the magic of CT we can think of these as "equivalent"
(involving some kind of isomorphism). BTW, I should mention I'm not a
mathematician, in case it's not blindingly obvious. My interest is
literary - I'm just naive enough to think this stuff could be
explained in plain English, but I'm not quite there yet.
More information about the Haskell-Cafe