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). > 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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
