Stefan O'Rear schrieb:
On Mon, Aug 13, 2007 at 04:35:12PM +0200, apfelmus wrote:
My assumption is that we have an equivalence
forall a,b . m (a -> m b) ~ (a -> m b)
because any side effect executed by the extra m on the outside can well be
delayed until we are supplied a value a. Well, at least when all arguments
are fully applied, for some notion of "fully applied"
(\a x -> a >>= ($ x)) ((\f -> return f) X) ==> (β)
(\a x -> a >>= ($ x)) (return X) ==> (β)
(\x -> (return X) >>= ($ x)) ==> (monad law)
(\x -> ($ x) X) ==> (β on the sugar-hidden 'flip')
(\x -> X x) ==> (η)
X
Up to subtle strictness bugs arising from my use of η :), you're safe.
Yes, but that's only one direction :) The other one is the problem:
return . (\f x -> f >>= ($ x)) =?= id
Here's a counterexample
f :: IO (a -> IO a)
f = writeAHaskellProgram >> return return
f' :: IO (a -> IO a)
f' = return $ (\f x -> f >>= ($ x)) $ f
==> (β)
return $ \x -> (writeAHaskellProgram >> return return) >>= ($ x)
==> (BIND)
return $ \x -> writeAHaskellProgram >> (return return >>= ($ x))
==> (LUNIT)
return $ \x -> writeAHaskellProgram >> (($ x) return)
==> (β)
return $ \x -> writeAHaskellProgram >> return x
Those two are different, because
clever = f >> return () = writeAHaskellProgram
clever' = f' >> return () = return ()
are clearly different ;)
Regards,
apfelmus
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
