[Haskell-cafe] type and data constructors in CT

[Gregg Reynolds]

On Mon, Feb 2, 2009 at 3:27 PM, David Menendez <dave at zednenem.com> wrote:


> Does that help at all?
>

I think it does.  But ... it gives me crazy ideas.  Like:  a functor is a
kind of magic non-computing function!  That's why they didn't call it a
function?  We know it maps A to FA, but we don't know how (maybe we don't
care): there's no algorithm, just a functorific magic carpet that transports
us across the border to FA.  We couldn't compute FA even if we wanted to -
different categories are like alternate universes, it would be like
producing a widget in an alternate physical universe, we have no way of even
thinking of how to do that.

Ditto for data constructors as natural transformations: they don't compute,
they just do magic.  They're the CT surgeon's devious way of working on the
guts of a categorical object without getting his hands dirty with mundane
functions - getting from value A to (an?) image value of A under the functor
F, which we cannot do directly by algorithm or computation.  We do not - can
not - have an actual function that computes A's image.  We have to work
indirectly, using non-computing magic carpets - first Id takes us to Id A,
then we follow the nat trans to FA.

Ok, that probably triggers the gag reflex for a real mathematician, but it
sure sounds like a good story to me (remember, I'm taking notes for a
guide/tutorial for newbies that may or may not ever get written.)

Thanks very much for the help,

-gregg
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090203/f7cc2484/attachment.htm