[Haskell-cafe] Naturality condition for inits

[Derek Elkins]

On Sat, 2009-03-07 at 22:18 +0000, R J wrote:
> Here's another Bird problem that's stymied me:
> 
> The function "inits" computes the list of initial segments of a list;
> its type is inits :: [a] -> [[a]].  What is the appropriate naturality
> condition for "inits"?

A natural transformation is between two Functors f and g is a
polymorphic function t :: (Functor f, Functor g) => f a -> g a.  The
naturality condition is the free theorem which states*:
for any function f :: A -> B, t . fmap f = fmap f . t
Note that fmap is being used in two different instances here.

For lists, fmap = map and so we have for any polymorphic function [a] ->
[a] using reverse as a representative,
map f . reverse = reverse . map f.

inits is a natural transformation between [] and [] . [] (where . is
type-level composition and not expressible in Haskell).  Functors
compose just by composing their fmaps, so fmap for [] . [] is simply
map . map, therefore the naturality condition for inits is the
following:
for any function f :: A -> B,
inits . map f = map (map f) . inits
which you can easily prove.

* Actually there are some restrictions relating to bottom.