[Haskell-cafe] How do you rewrite your code?

[Ryan Ingram]

On Tue, Mar 2, 2010 at 11:20 AM, Sean Leather <leather at cs.uu.nl> wrote:
> 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