[Haskell-cafe] Re: Re: Re: Full strict functor by abusing Haskell exceptions

[wren ng thornton]

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.

-- 
Live well,
~wren