[Haskell-cafe] reordering pure bindings in monads

[Dan Doel]

On Thursday 29 May 2008, Tim Newsham wrote:
> Intuitively it seems like the applicative expression:
>
>    (++) <$> getLine <*> getLine
>
> should represent the same thing as the more traditional liftM2
> expressions:
>
>    do { x <- getLine; y <- getLine; return ((++) x y) }
>
> but it seems to me that you cant directly manipulate the first into
> the second.  I get:
>
>    do x2' <- getLine
>       x1 <- return ((++) x2')
>       x2 <- getLine
>       return (x1 x2)
>
> the only way I can get from here to the liftM2 definition is if I
> treat "x1 <- return ((++) x2')" as "let x1 = (++) x2", and then
> allow it to be reordered after the second getLine.  Then it is
> straightforward to reduce to the liftM2 expression above.
>
> It seems to me that this is a valid transformation if:
>     - no side effects, including pattern match errors, can occur
>       in the let (or x1 <- return ...).
>     - movement doesnt change the dependencies
>       - x1 isnt used between the original line and its new position
>       - there are no new bindings for x2' introduced between the original
>         line and the new line.
>
> Did I overlook anything?  Do any haskell implementations allow rewrites
> like these to occur?

Monad laws. Consider the following:

    do x <- getLine
       f <- return ((++) x)
       y <- getLine
       return (f y)

  === desugar

    getLine >>= \x -> return ((++) x) >>= \f -> getLine >>= \y -> return (f y)

  === return x >>= f = f x

    getLine >>= \x -> (\f -> getLine >>= \y -> return (f y)) ((++) x)

  === beta

    getLine >>= \x -> getLine >>= \y -> return (x ++ y)

  == resugar

    do x <- getLine ; y <- getLine ; return (x ++ y)

I don't know if GHC does any rewrites based on monad laws (I suspect not), but 
if you want to prove two such expressions equal, they're the ticket.

-- Dan