[Haskell-cafe] type and data constructors in CT

Gregg Reynolds 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.

Thanks much,
-gregg


More information about the Haskell-Cafe mailing list