<div class="gmail_quote">On Mon, Jan 23, 2012 at 8:05 PM, Daniel Fischer <span dir="ltr"><<a href="mailto:daniel.is.fischer@googlemail.com">daniel.is.fischer@googlemail.com</a>></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>
> At the end of that paste, I prove the three Haskell monad laws from the<br>
> functor laws and "monoid"-ish versions of the monad laws, but my proofs<br>
> all rely on a property of natural transformations that I'm not sure how<br>
> to prove; given<br>
><br>
> type m :-> n = (forall x. m x -> n x)<br>
> class Functor f where fmap :: forall a b. (a -> b) -> f a -> 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 :-> n, and g :: a<br>
> -> 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 :-> n = (forall x. m x -> n x)</div><div><br></div></div><div style>And I have</div><div style>f :: M :-> N</div><div style>g :: A -> 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 -> N B</div><div style> =</div><div style> f . fmap g :: M A -> 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 :-> 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">
> Is there some<br>
> more fundamental law of natural transformations that I'm not aware of<br>
> that I need to use? Is it possible to write a natural transformation<br>
> in Haskell that violates this law?<br>
><br>
> -- ryan<br>
<br>
</div></div></blockquote></div><br>