I&#39;ve been playing around with the relationship between monoids and monads (see <a href="http://www.jonmsterling.com/posts/2012-01-12-unifying-monoids-and-monads-with-polymorphic-kinds.html">http://www.jonmsterling.com/posts/2012-01-12-unifying-monoids-and-monads-with-polymorphic-kinds.html</a> and <a href="http://blog.sigfpe.com/2008/11/from-monoids-to-monads.html">http://blog.sigfpe.com/2008/11/from-monoids-to-monads.html</a>), and I put together my own implementation which I&#39;m quite happy with, that you can see at <a href="http://hpaste.org/56903">http://hpaste.org/56903</a> ; relying only on the extensions RankNTypes, TypeOperators, NoImplicitPrelude, ScopedTypeVariables;<br>
<br>At the end of that paste, I prove the three Haskell monad laws from the functor laws and &quot;monoid&quot;-ish versions of the monad laws, but my proofs all rely on a property of natural transformations that I&#39;m not sure how to prove; given<br>
<br>    type m :-&gt; n = (forall x. m x -&gt; n x)<br>    class Functor f where fmap :: forall a b. (a -&gt; b) -&gt; f a -&gt; f b<br>    -- Functor identity law: fmap id = id<br>    -- Functor composition law fmap (f . g) = fmap f . fmap g<br>
<br>Given Functors m and n, natural transformation f :: m :-&gt; n, and g :: a -&gt; b, how can I prove (f . fmap_m g) = (fmap_n g . f)?  Is there some more fundamental law of natural transformations that I&#39;m not aware of that I need to use?  Is it possible to write a natural transformation in Haskell that violates this law?<br>
<br>  -- ryan<br>