[Haskell-cafe] Natural Transformations and fmap
Ryan Ingram
ryani.spam at gmail.com
Tue Jan 24 06:06:52 CET 2012
On Mon, Jan 23, 2012 at 8:05 PM, Daniel Fischer <
daniel.is.fischer at googlemail.com> 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120123/e00ad82c/attachment.htm>
More information about the Haskell-Cafe
mailing list