Explanation of partial application - join
-
26-06-2021 - |
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 ?
Solution
=<<
'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
id
s 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.
OTHER TIPS
Some useful concepts to use here:
- Any type with a variable
a
can be converted into a different type by replacing every instance ofa
with any other typet
. So if you have the typea -> b -> c
, you can obtain the typea -> d -> c
or the typea -> b -> Int
by replacingb
withd
orc
withInt
respectively. - Any two types that can be converted to each other by replacement are equivalent. For example,
a -> b
andc -> d
are equivalent (a
~c
,b
~d
). - If a type
t
can be converted to a typet'
, butt'
can't be converted back tot
, then we say thatt'
is a specialization oft
. For example,a -> a
is a specialization ofa -> 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.
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
.