[Haskell-cafe] Naturality condition for inits
derek.a.elkins at gmail.com
Sat Mar 7 17:37:48 EST 2009
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
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.
More information about the Haskell-Cafe