# [Haskell-cafe] Natural Transformations and fmap

Ryan Ingram ryani.spam at gmail.com
Sat Jan 28 01:56:20 CET 2012

```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
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

 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

 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
>
>
> ______________________________**_________________