What Haskell type system magic allows for the definition of join?

Question

The join utility function is defined as:

join :: (Monad m) => m (m a) -> m a
join x = x >>= id

Given that the type of >>= is Monad m => m a -> (a -> m b) -> m b and id is a -> a, how can that function also be typed as a -> m b as it must be in the definition above? What are m and b in this case?

Answer 1

The as in the types for >>= and id aren't necessarily the same as, so let's restate the types like this:

(>>=)    :: Monad m => m a     -> (a -> m b) -> m b
id       ::                        c -> c

So we can conclude that c is the same as a after all, at least when id is the second argument to >>=... and also that c is the same as m b. So a is the same as m b. In other words:

(>>= id) :: Monad m => m (m b) ->               m b

Answer 2

dave4420 hits it, but I think the following remarks might still be useful.

There are rules that you can use to validly "rewrite" a type into another type that's compatible with the original. These rules involve replacing all occurrences of a type variable with some other type:

• If you have id :: a -> a, you can replace a with c and get id :: c -> c. This latter type can also be rewritten to the original id :: a -> a, which means that these two types are equivalent. As a general rule, if you replace all instances of type variable with another type variable that occurs nowhere in the original, you get an equivalent type.
• You can replace all occurrences of a type variable with a concrete type. I.e., if you have id :: a -> a, you can rewrite that to id :: Int -> Int. The latter however can't be rewritten back to the original, so in this case you're specializing the type.
• More generally than the second rule, you can replace all occurrences of a type variable any type, concrete or variable. So for example, if you have f :: a -> m b, you can replace all occurrences of a with m b and get f :: m b -> m b. Since this one can't be undone either, it's also a specialization.

That last example shows how id can be used as the second argument of >>=. So the answer to your question is that we can rewrite and derive types as follows:

1. (>>=)    :: m a -> (a -> m b) -> m b        (premise)
2. id       :: a -> a                          (premise)
3. (>>=)    :: m (m b) -> (m b -> m b) -> m b  (replace a with m b in #1)
4. id       :: m b -> m b                      (replace a with m b in #2)
   .
   .
   .
n. (>>= id) :: m (m b) -> m b                  (indirectly from #3 and #4)