[Haskell-cafe] Natural Transformations and fmap

[Ryan Ingram]

I know a bit of category theory, but I'm trying to look at it from a
fundamental perspective; I know that I intend (m :-> n) to mean "natural
transformation from functor m to functor n", but the type itself (forall x.
m x -> n x) doesn't necessarily enforce that.

However, the type of natural transformations comes with a free theorem, for
example

   concat :: [[a]] -> [a]

has the free theorem

   forall f :: a -> b, f strict and total, fmap f . concat = concat . fmap
(fmap f)

The strictness condition is needed; consider

   broken_concat :: [[a]] -> [a]
   broken_concat _ = [undefined]
   f = const ()

   fmap f (broken_concat []) = fmap f [undefined] = [()]
   broken_concat (fmap (fmap f) []) = broken_concat [] = [undefined]

The 'taming selective strictness' version of the free theorem generator[1]
allows removing the totality condition on f, but not the strictness
condition.

But in the case of concat, you can prove a stronger theorem:

   forall f :: a -> b, fmap f . concat = concat . fmap (fmap f)

My suspicion is that this stronger theorem holds for all strict and total
natural transformations, but I don't know how to go about proving that
suspicion.  I'm a hobbyist mathematician and a professional programmer, not
the other way around :)

I think it's probably easy to prove that the monoid laws imply that mult'
and one' are strict and total.

> Thus, you can in principle define plenty of natural transformations which
do not have the type f :: forall X. M X -> N X.

Can you suggest one?  I don't see how you can get around f needing to act
at multiple types since it can occur before and after g's fmap:

fmap g . f = f . fmap g

   M A --fmap_M g--> M B
    |                 |
   f_A               f_B
    |                 |
    v                 v
   N A --fmap_N g--> N B

You can have n = m, of course, but that just means f :: M :-> M.

  -- ryan

[1] http://www-ps.iai.uni-bonn.de/cgi-bin/polyseq.cgi
Use this term:
/\a. let flipappend =(\xs :: [a]. fix (\rec :: [a] -> [a]. \ys :: [a].
                      case ys of { [] -> xs; y:zs -> y : rec zs })) in
     let concat = fix (\rec :: [[a]] -> [a]. \xss :: [[a]].
                       case xss of { [] -> []_{a}; xs:yss -> flipappend
(rec yss) xs}) in
     concat

[2] See http://hpaste.org/56903  Summary:

-- both of these types have obvious Functor instances
newtype (f :. g) x = O (f (g x))
data Id x = Id x

class Functor m => Monad m where
   one'  :: Id       :-> m
   mult' :: (m :. m) :-> m

-- instances are required to satisfy monoid laws:
--    one' is a left/right identity for mult':
--        forall x :: m a
--            mult' . O . one' . Id $ x = x = mult' . O . fmap (one' . Id)
$ x
--    mult' is associative:
--        forall x :: m (m (m a))).
--            mult' . O . mult' . O $ x = mult' . O . fmap (mult' . O) $ x

On Thu, Jan 26, 2012 at 9:30 PM, wren ng thornton <wren at freegeek.org> wrote:

> On 1/23/12 10:39 PM, Ryan Ingram wrote:
>
>>     type m :->  n = (forall x. m x ->  n x)
>>     class Functor f where fmap :: forall a b. (a ->  b) ->  f a ->  f b
>>     -- Functor identity law: fmap id = id
>>     -- Functor composition law fmap (f . g) = fmap f . fmap g
>>
>> Given Functors m and n, natural transformation f :: m :-> n, and g :: a ->
>> b, how can I prove (f . fmap_m g) = (fmap_n g . f)?
>>
>
> That is the defining property of natural transformations. To prove it for
> polymorphic functions in Haskell you'll probably want to leverage
> parametricity.
>
>
> I assume you don't know category theory, based on other emails in this
> thread. But the definition of a natural transformation is that it is a
> family of morphisms/functions { f_X :: M X -> N X | X an object/type } such
> that for all g :: a -> b we have that f_b . fmap_m g == fmap_n g . f_a
>
> Thus, you can in principle define plenty of natural transformations which
> do not have the type f :: forall X. M X -> N X. The only requirement is
> that the family of morphisms obeys that equation. It's nice however that if
> a function has that type, then it is guaranteed to satisfy the equation (so
> long as it doesn't break the rules by playing with strictness or other
> things that make it so Hask isn't actually a category).
>
> --
> Live well,
> ~wren
>
>
> ______________________________**_________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/**mailman/listinfo/haskell-cafe<http://www.haskell.org/mailman/listinfo/haskell-cafe>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120127/a9c659c7/attachment.htm>