<div class="gmail_quote">On Mon, Jan 23, 2012 at 8:05 PM, Daniel Fischer <span dir="ltr">&lt;<a href="mailto:daniel.is.fischer@googlemail.com">daniel.is.fischer@googlemail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="im">On Tuesday 24 January 2012, 04:39:03, Ryan Ingram wrote:<br>
&gt; At the end of that paste, I prove the three Haskell monad laws from the<br>
&gt; functor laws and &quot;monoid&quot;-ish versions of the monad laws, but my proofs<br>
&gt; all rely on a property of natural transformations that I&#39;m not sure how<br>
&gt; to prove; given<br>
&gt;<br>
&gt;     type m :-&gt; n = (forall x. m x -&gt; n x)<br>
&gt;     class Functor f where fmap :: forall a b. (a -&gt; b) -&gt; f a -&gt; f b<br>
&gt;     -- Functor identity law: fmap id = id<br>
&gt;     -- Functor composition law fmap (f . g) = fmap f . fmap g<br>
&gt;<br>
&gt; Given Functors m and n, natural transformation f :: m :-&gt; n, and g :: a<br>
&gt; -&gt; b, how can I prove (f . fmap_m g) = (fmap_n g . f)?<br>
<br>
</div>Unless I&#39;m utterly confused, that&#39;s (part of) the definition of a natural<br>
transformation (for non-category-theorists).<br></blockquote><div><br></div><div style>Alright, let&#39;s pretend I know nothing about natural transformations and just have the type declaration</div><div class="im" style>
<div><br></div><div>type m :-&gt; n = (forall x. m x -&gt; n x)</div><div><br></div></div><div style>And I have</div><div style>f :: M :-&gt; N</div><div style>g :: A -&gt; B</div><div style>instance Functor M -- with proofs of functor laws</div>
<div style>instance Functor N -- with proofs of functor laws</div><div style><br></div><div style>How can I prove</div><div style>  fmap g. f :: M A -&gt; N B</div><div style>  =</div><div style>  f . fmap g :: M A -&gt; N B</div>
<div style><br></div><div><span style>I assume I need to make some sort of appeal to the parametricity of M :-&gt; N.</span> </div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="HOEnZb"><div class="h5">
&gt; Is there some<br>
&gt; more fundamental law of natural transformations that I&#39;m not aware of<br>
&gt; that I need to use?  Is it possible to write a natural transformation<br>
&gt; in Haskell that violates this law?<br>
&gt;<br>
&gt;   -- ryan<br>
<br>
</div></div></blockquote></div><br>