[Haskell-cafe] Natural Transformations and fmap
Ryan Ingram
ryani.spam at gmail.com
Tue Jan 24 04:39:03 CET 2012
I've been playing around with the relationship between monoids and monads
(see
http://www.jonmsterling.com/posts/2012-01-12-unifying-monoids-and-monads-with-polymorphic-kinds.htmland
http://blog.sigfpe.com/2008/11/from-monoids-to-monads.html), and I put
together my own implementation which I'm quite happy with, that you can see
at http://hpaste.org/56903 ; relying only on the extensions RankNTypes,
TypeOperators, NoImplicitPrelude, ScopedTypeVariables;
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)? 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/0a9227f8/attachment.htm>
More information about the Haskell-Cafe
mailing list