<html><head></head><body bgcolor="#FFFFFF"><div>Have you tried generating a free theorem for :-&gt; ? (I haven't as I'm writing from my phone)<br><br><div><br></div></div><div><br>24.01.2012, в 9:06, Ryan Ingram &lt;<a href="mailto:ryani.spam@gmail.com">ryani.spam@gmail.com</a>&gt; написал(а):<br><br></div><div></div><blockquote type="cite"><div><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 "monoid"-ish versions of the monad laws, but my proofs<br>
&gt; all rely on a property of natural transformations that I'm not sure how<br>
&gt; to prove; given<br>
&gt;<br>
&gt; &nbsp; &nbsp; type m :-&gt; n = (forall x. m x -&gt; n x)<br>
&gt; &nbsp; &nbsp; class Functor f where fmap :: forall a b. (a -&gt; b) -&gt; f a -&gt; f b<br>
&gt; &nbsp; &nbsp; -- Functor identity law: fmap id = id<br>
&gt; &nbsp; &nbsp; -- 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'm utterly confused, that's (part of) the definition of a natural<br>
transformation (for non-category-theorists).<br></blockquote><div><br></div><div style="">Alright, let'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="">&nbsp; fmap g. f :: M A -&gt; N B</div><div style="">&nbsp; =</div><div style="">&nbsp; 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>&nbsp;</div><div>&nbsp;</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'm not aware of<br>
&gt; that I need to use? &nbsp;Is it possible to write a natural transformation<br>
&gt; in Haskell that violates this law?<br>
&gt;<br>
&gt; &nbsp; -- ryan<br>
<br>
</div></div></blockquote></div><br>
</div></blockquote><blockquote type="cite"><div><span>_______________________________________________</span><br><span>Haskell-Cafe mailing list</span><br><span><a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a></span><br><span><a href="http://www.haskell.org/mailman/listinfo/haskell-cafe">http://www.haskell.org/mailman/listinfo/haskell-cafe</a></span><br></div></blockquote></body></html>