[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,
~wren
More information about the Haskell-Cafe
mailing list