Explanation of partial application - join

Question

Why does partial application of functions with different signatures work?

Take Control.Monad.join as an example:

GHCi> :t (=<<)
(=<<) :: Monad m => (a -> m b) -> m a -> m b
GHCi> :t id
id :: a -> a
GHCi> :t (=<<) id
(=<<) id :: Monad m => m (m b) -> m b

Why does it accepts id :: a -> a in place of (a -> m b) argument, as they are obviously different ?

Answer 1

Some useful concepts to use here:

1. Any type with a variable a can be converted into a different type by replacing every instance of a with any other type t. So if you have the type a -> b -> c, you can obtain the type a -> d -> c or the type a -> b -> Int by replacing b with d or c with Int respectively.
2. Any two types that can be converted to each other by replacement are equivalent. For example, a -> b and c -> d are equivalent (a ~ c, b ~ d).
3. If a type t can be converted to a type t', but t' can't be converted back to t, then we say that t' is a specialization of t. For example, a -> a is a specialization of a -> b.

Now, with these very useful concepts, the answer to your question is very simple: even if the function's "native" types don't match exactly, they are compatible because they can be rewritten or specialized to get that exact match. Matt Fenwick's answer shows specializations that do it for this case.

Answer 2

It tries to unify a with m b, and simply decides that a must be m b, so the type of (=<<) (under the assumption a ~ m b) is Monad m => (mb -> m b) -> m (m b) -> m b, and once you apply it to id, you are left with Monad m => m (m b) -> m b.

Answer 3

=<<'s type signature says that the first argument is a function from an a (anything) to a monad of b.

Well, m b counts as anything, right? So we can just substitute in m b for every a:

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

ids type says that it is a function from anything to the same anything. So if we sub in m b (not forgetting the monad constraint), we get:

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

Then you can see that the types match.