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

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.

Live well,

More information about the Haskell-Cafe mailing list