Are the following two implementations of flatten equivalent for all well-behaved Monads?
flatten1 xss = do
xs <- xss
x <- xs
return x
flatten2 xss = do
xs <- xss
xs
Yes, they're identical. They're desugared as
flatten1 xss =
xss >>= \xs -> xs >>= \x -> return x
flatten2 xss = do
xss >>= \xs -> xs
The first one is equivalent to
xss >>= \xs -> xs >>= return
and by the Right identity monad law equivalent to
xss >>= \xs -> xs
In short, yes. To prove it:
You've written:
xss >>= (\xs -> xs >>= \x -> return x)
xss >>= (\xs -> xs >>= return) -- eta
in the first and
xss >>= (\xs -> xs)
xss >>= id
according to the monad laws, return
is a right identity so that
m >>= return === m
so we can do
xss >>= (\ xs -> xs >>= return )
xss >>= (\ xs -> xs )
xss >>= id
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With