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@F : morphisms -> morphisms pure@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