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