On Tue, Mar 2, 2010 at 11:20 AM, Sean Leather
For all x, f:
x >>= return . f --> fmap f x or f <$> x -- requires importing Control.Applicative
I think the right-hand side (RHS) is more concise and simpler. The types here do change: the type constructor has a Monad constraint in the left-hand side and a Functor constraint in the RHS. Types that are Monad instances are generally also Functor instances, so this is often possible. I'm convinced the semantics are preserved, though I haven't proven it.
(Hand-wavy part of proof) I believe that by parametricity, any two functions of the type: mapX :: forall a b. (a -> b) -> (X a -> X b) that satisfy the functor laws: mapX f . mapX g = mapX (f . g) mapX id = id must be equal to one another, and therefore equal to fmap. (formal part of proof): given any monad M, let mapM f m = m >>= return . f mapM id m -- apply mapM = m >>= return . id -- apply (.) = m >>= (\x -> return (id x)) -- apply id = m >>= (\x -> return x) -- eta reduce = m >>= return -- monad right identity = m -- un-apply id = id m (mapM f . mapM g) m -- apply (.) = mapM f (mapM g m) -- apply mapM twice = (m >>= return . g) >>= return . f -- apply (.) twice = (m >>= \x -> return (g x)) >>= \y -> return (f y) -- monad associativity = m >>= (\x -> return (g x) >>= \y -> return (f y)) -- monad left identity = m >>= (\x -> (\y -> return (f y)) (g x)) -- beta reduce = m >>= (\x -> return (f (g x))) -- unapply (.) = m >>= (\x -> return ((f . g) x)) -- unapply (.) = m >>= (\x -> (return . (f . g)) x) -- eta reduce = m >>= return (f . g) -- un-apply mapM = mapM (f . g) m So, we have mapM id m = id m (mapM f . mapM g) m = mapM (f . g) m and by extensionality mapM id = id mapM f . mapM g = mapM (f . g) So, if the handwavy part of the proof at the beginning holds, mapM = fmap, and your translation is sound. -- ryan