Returning an item extracted from a monad; excess?

Are the following two implementations equivalent for all well-executed monads?

flatten1 xss = do xs <- xss x <- xs return x flatten2 xss = do xs <- xss xs 
+6
source share
2 answers

Yes, they are the same. They desugared like

 flatten1 xss = xss >>= \xs -> xs >>= \x -> return x flatten2 xss = do xss >>= \xs -> xs 

The first is equivalent

 xss >>= \xs -> xs >>= return 

and the correct monad law equivalent

 xss >>= \xs -> xs 
+9
source

In short, yes. To prove this:

You wrote:

 xss >>= (\xs -> xs >>= \x -> return x) xss >>= (\xs -> xs >>= return) -- eta 

in the first and

 xss >>= (\xs -> xs) xss >>= id 

according to the laws of the monad , return is the correct identity, so that

 m >>= return === m 

so we can do

 xss >>= (\ xs -> xs >>= return ) xss >>= (\ xs -> xs ) xss >>= id 
+5
source

Source: https://habr.com/ru/post/947751/


All Articles