[Haskell-cafe] reordering pure bindings in monads
Dan Doel
dan.doel at gmail.com
Thu May 29 23:35:18 EDT 2008
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
More information about the Haskell-Cafe
mailing list