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
f...@f : morphisms -> morphisms
p...@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.
--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
