Understanding Monads boxing

Today on #haskell@freenode I had an interesting discussion. It all started when I asked if the following statements make any sense:

Just 5 >>= \x -> Just $ x+1
what this does is basically unwraps Just, adds 1 to its value and returns Just. (*
return (Just 5) >>= \y -> y >>= \x -> Just $ x+1
what this does is basically unwraps the monadic value of Just 5, so we have Just 5.
So we have return (Just 5) >>= \y -> y == Just 5. Now (*) applies here.

Let’s check the types:

Prelude> :t Just 5
Just 5 :: Num a => Maybe a
Prelude> :t return (Just 5)
return (Just 5) :: (Monad m, Num a) => m (Maybe a)

So, basically, my question was (as can be seen from the statement above), how is it possible to convert m (Maybe a) to Maybe a? And, if m (m a) -> m a is possible, why isn’t m a -> a possible?

Well, m a -> a can be possible for some monads, for example for the Maybe monad, if we define it like:

fromJust (Just x) = x

But it’s not something that can be easily implemented for just any monad.

Now, as for why m (m a) -> m a is possible (and, in general m (m (… (m a) …)) -> m a), we can take a look at the definition of join, which is:

join x = x >>= id

So, if we try to do something like this:

Prelude> join $ Just (Just 5)
Just 5
Prelude> :t Just (Just 5)
Just (Just 5) :: Num a => Maybe (Maybe a)
Prelude> :t Just 5
Just 5 :: Num a => Maybe a
Prelude> join $ Just (Just 5)
Just 5
Prelude> :t join $ Just (Just 5)
join $ Just (Just 5) :: Num b => Maybe b

We can see basically how it “unboxes” stuff, and in my statement above I implicitly used join, which is the underlined part.

But how does it really work?

Well, if we look at the type of the bind operator:

Prelude> :t (>>=)
(>>=) :: Monad m => m a -> (a -> m b) -> m b

We can now start experimenting. What if we set a = m c?

We get m (m c) -> (m c -> m b) -> m b. Can we find such a function that satisfies this?

For (a -> m b) we can basically use the following lambda \x -> return x
So, for (m a -> m b), what if we omit return, and instead try \x -> x?

Prelude> Just (Just 5)
Just (Just 5)
Prelude> Just (Just 5) >>= \x -> x
Just 5
Prelude> :t Just (Just 5) >>= \x -> x
Just (Just 5) >>= \x -> x :: Num b => Maybe b
Prelude> :t Just (Just 5)
Just (Just 5) :: Num a => Maybe (Maybe a)
Prelude> :t (Just 5)
(Just 5) :: Num a => Maybe a

So, by using return, in the example of m a -> (a -> m b) -> m b we give back a “boxed” value, because we have \x -> return x where x = a, and return x = m a.

But, by not using return in the example of m (m a) -> (m a -> m b) -> m b we give back the same value that we receive, because we have \x -> x where x = m a, and the lambda expression will evaluate to m a.

So, with this we have shown how it’s possible to convert m (m a) to m b, and thus in general m (m (… (m a) …)) to m b.

Some interesting excerpts from the chat (please note that some parts are removed):

 the difference between "return $ Just 5" and "Just 5" is that the first is a monadic value
(instance of Monad), and the second is only instance of data Maybe?
BoR0: Maybe is an instance of Monad, the difference is this:
> return $ Just 5 :: [Maybe Int]
[Just 5]
> return $ Just 5 :: Maybe (Maybe Int)
Just (Just 5)
BoR0: Maybe is an instance of Monad, "Monad m => m" says "any monad will work"
BoR0: So "(>>=) :: Monad m => m a -> (a -> m b) -> m b" says it'll work for *any* Monad,
even if if you don't know yet which one
BoR0: There's no reason why a monad cannot contain another monad inside
> return 5 :: [Int]
[5]
aha, okay. so return $ Just 5 is doubly "wrapped"
BoR0: Yes
BoR0: ^
so if we have return x = Just x for Maybe monad, why doesn't return $ Just 5 give Just (Just 5)
to us?
BoR0: It will, if you ask for it
> return (Just 5) :: Maybe (Maybe Int)
Just (Just 5)
but what does it do without specifying :: ... ?
BoR0: Without the type signature it's polymorphic, it can be any Monad instance
polymorphic! that clarifies it! great
BoR0: Yes, all typeclasses are polymorphic, unless you specify a type OR type inference sees
which type you wanted (actually, this is the only way, the type annotation just explicitly tell the
type inference what you want :)
I somewhere read that IO String can't be converted to String. but with this discussion I think
the opposite, what is wrong now?
so what held for Maybe monad (extracting x from Just x) doesn't necesarilly hold for IO monad?
BoR0: For Maybe, you weren't really extracting. You were putting the value back into a Just
at the end with return. All monadic expressions have a return at the end.
BoR0: Yes, some *specific* monads may provide tools for extracting values (i.e. Maybe
and list, for example). But the generic monad class does not provide a way to do that
BoR0: Since IO doesn't provide a function to extract values, there's no way to get them out
BoR0: monads allow you to go from an arbitrary number of applications of M to A to just M A
Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s