Re: [Haskell-cafe] Natural Transformations and fmap

Have you tried generating a free theorem for :-> ? (I haven't as I'm writing from my phone) 24.01.2012, в 9:06, Ryan Ingram написал(а):

On Mon, Jan 23, 2012 at 8:05 PM, Daniel Fischer wrote: On Tuesday 24 January 2012, 04:39:03, Ryan Ingram wrote:

...

At the end of that paste, I prove the three Haskell monad laws from the functor laws and "monoid"-ish versions of the monad laws, but my proofs all rely on a property of natural transformations that I'm not sure how to prove; given

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)?

Unless I'm utterly confused, that's (part of) the definition of a natural transformation (for non-category-theorists).

Alright, let's pretend I know nothing about natural transformations and just have the type declaration

type m :-> n = (forall x. m x -> n x)

And I have f :: M :-> N g :: A -> B instance Functor M -- with proofs of functor laws instance Functor N -- with proofs of functor laws

How can I prove fmap g. f :: M A -> N B = f . fmap g :: M A -> N B

I assume I need to make some sort of appeal to the parametricity of M :-> N.

...

Is there some more fundamental law of natural transformations that I'm not aware of that I need to use? Is it possible to write a natural transformation in Haskell that violates this law?

-- ryan

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe