How do I derive the type for this function:

Question

I'm trying to get better at playing "type tetris". I have the functions:

(=<<) :: Monad m => (a -> m b) -> m a -> m b
zip :: [a] -> [b] -> [(a, b)]

And GHCi tells me:

(zip =<<) :: ([b] -> [a]) -> [b] -> [(a, b)]

I'm having a hard time figuring out how to arrive at that final signature from the first two. My intuition (for lack of a better word) is saying that the first argument of =<< namely a -> mb is somehow reconciled against the signature of zip, and then it should all fall out from that. But I can't understand how to make that leap. Can it be broken down in to a series of easy to follow steps?

Answer 1

(zip =<<) is equivalent to (>>= zip), which makes it perhaps a bit more readable. Either way, zip occupies the (a -> m b) slot in those functions, as you've correctly observed.

One more intuitive transformation to make is thinking about the arity of =<<. It "takes" two parameters, so if we apply it to one, we should only be left with one more. Hence, the signature ([b] -> [a]) -> [b] -> [(a, b)] is an unary function!

(zip =<<) :: ([b] -> [a]) -> ([b] -> [(a, b)])
             ------------    -----------------
                 m a'                m b'

So what's m? The Monad instance exists for functions (r ->) (or, alternatively, (->) r). So in this case r :: [b] (and thus m :: ([b] ->)), a' :: [a] and b' :: [(a, b)].

Consequently, zip fits just as we asserted at the beginning:

a'  -> m b'                    -- substitute [(a,b)] for b'
a'  -> m [(a, b)]              -- substitute [a] for a'
[a] -> m [(a, b)]              -- substitute ([b] ->) for m
[a] -> ([b] -> [(a,b)])

[a] -> [b] -> [(a,b)]

Answer 2

It helps to do two things before everything else:

1. put explicit parentheses so that x->y->z becomes x->(y->z)
2. rename type variables so that there are no clashes

Wit this in mind let's rewrite the types

(=<<) :: Monad m => (a -> m b) -> (m a -> m b)
zip :: [x] -> ([y] -> [(x, y)])

Now match the types. The first argument to =<< is zip, so (a -> m b) is the same as [x] -> ([y] -> [(x, y)]).

a          ->        m b
[x]        ->        ([y] -> [(x, y)])

So a is [x] and m b is ([y] -> [(x, y)]). Rewriting -> in prefix notation, we get -> [y] [(x, y)], which is the same as (-> [y]) [(x, y)].

m             b
(-> [y])      [(x, y)]

So m is (-> [y]) (which is a monad indeed) and b is [(x, y)].

So now we know what is a, what is b and what is m. Let's rewrite (m a -> m b) in these terms:

(m            a)          ->          (m            b)
((-> [y])     [x])        ->          ((-> [y])     [(x, y)])

Rewriting in the infix style again, we get

([y] -> [x])              ->          ([y] -> [(x, y)])

which is, up to variable names, is the same answer GHC is giving you.

Answer 3

You just write them down one under another, with vertical alignment as an aid, while renaming the type variables consistently so there's no accidental capture:

(=<<) :: Monad m => (a1  ->     m    b1       ) -> m a1 -> m b1
zip   ::             [a] -> ([b] ->  [(a, b)])
                     [a] -> ([b] ->) [(a, b)]
                     [a] -> (->) [b] [(a, b)]
-----------------------------------------------------------
               a1 ~ [a] ,  m ~ (->) [b] ,  b1 ~ [(a, b)]               (*)
-----------------------------------------------------------
(zip =<<) :: Monad m =>                            m a1 -> m b1
                                          ((->) [b]) a1 -> ((->) [b]) b1
                                            ([b] -> a1) -> ([b] -> b1)
                                           ([b] -> [a]) -> ([b] -> [(a, b)])
                                           ([b] -> [a]) ->  [b] -> [(a, b)]

provided that Monad ((->) [b]) instance exists. Which it does:

> :i Monad
class Monad (m :: * -> *) where
    .......
instance Monad ((->) r) -- Defined in `GHC.Base'

If we follow the types in the specific case of function monad, we can see that (g =<< f) x == g (f x) x, and so

(zip =<<) f xs = zip (f xs) xs

from which it's easier to see its type's meaning.

---

(*) is the substitution resulting from the successful unification of the types a1 -> m b1 and [a] -> [b] -> [(a, b)] (which is [a] -> ([b] -> [(a, b)]), when fully parenthesized, because ->s in types associate to the right). Or in fully prefix form,

    (->)  a1   ( m            b1       )
    (->)  [a]  ( ((->) [b])   [(a, b)] )