[Haskell-cafe] Re: Re: Re: Full strict functor by abusing Haskell
wren ng thornton
wren at freegeek.org
Fri Sep 17 23:08:04 EDT 2010
On 9/17/10 4:39 PM, Ben Franksen wrote:
> Thanks for the link. What I actually wanted was a mathematical definition,
> though. From the TMR article I gather that a pointed functor could be
> defined as an endo-functor
> F: C -> C
> together with a natural transformation
> pure: Id -> F
> where Id: C -> C is the identity functor.
> No additional laws (beside naturality of pure) are imposed.
> Right so far?
> Why is this an interesting structure?
A functor F gives us a category containing an image of the domain. That
is, it gives us a collection of image objects and arrows between those
image objects. However, for F an endofunctor, we have no way to get from
the domain object to the image object; i.e., even though we can
correlate the types, we have no way to correlate the values of those types.
The natural transformation says that hom_C(X,FX) is inhabited, and
moreover that it has a natural inhabitant. In other words, it
incorporates the action of F into the category. Instead of leaving the
category and then coming back again (along F), we can perform the
mapping from X to FX within the category itself. That is, it gives us
image values, gives us a way to get from the domain subcategory to the
image subcategory while remaining within the category.
F : types -> types
fmap at F : morphisms -> morphisms
pure at F : values -> values
Embedding the action of an endofunctor into the category it operates on
strikes me as a very interesting structure. We encounter these all the
time in programming because we want to implement the operations of the
language within the language being defined.
More information about the Haskell-Cafe