Why can function composition with `join` change function inputs?

2
votes

I have recently started learning Haskell, and I was trying to do the following function composition (join . mapM) but got some weird types out of this function that I don't understand. I thought that either GHC would assume that t == m in the mapM type and the output of mapM would become m (m b) which would be join-able or it would not and this would error out because of type mismatch. Instead the following happened:

mapM :: (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b)
join :: Monad m => m (m a) -> m a
join . mapM :: Traversable t => (a -> t a -> b) -> t a -> t b

I don't understand how this is possible. The way I understand it, function composition should use the inputs of the first (or the second depending how you look at it) function and the outputs of the second function. But here the expected input function for mapM changes from a unary function to a binary function and I have no clue why. Even if GHC can't just make the assumption that t == m like I did, which I half expected, it should error out because of type mismatch, not change the input function type, right? What is happening here?

2
haskellmonadsfunction-composition
I don't have time for a full answer, and I'm also not totally sure what you're asking (eg liftM, aka fmap, seems unrelated to this composition). But in short, the output of mapM is a function t a -> m (t b), and join needs a monadic value of the form m ( m c) as input. The only way for these types to unify is for the Monad m to be the function type t a -> b, where t and a are fixed. (It's actually rather surprising to me that this works at all, but the types all match up.) – Robin Zigmond
To avoid any possible doubt, when I say "the Monad m (is) the function type t a -> b", I mean the Monad formally denoted as (->) t a, whose values are functions with input t a. (Sometime I wonder why Haskell has both a direct Monad instance for "functions with a fixed input", and one called the "reader monad" which is exactly the same but in a newtype wrapper. I think it would work better without the "unwrapped" version having a monad/applicative instance - but I'm getting off topic...) – Robin Zigmond
Yes you're right the whole liftM thing has nothing to do with the actual question it was just some context on why I was trying to do this composition, I will edit it out to make the actual question more clear. So if I understood what you said correctly rather than deciding that the m and t types were the same like I though it would it decided that m would become a function of type t a -> b? How would that show up in mapM output type? (t a -> b) (t b)? how is this a joinable thing specifically an m (m a)? – Xcode23
Ok given your extended explanation which I hadn't seen when I was writing my comment. m becomes ((->) t a) and the output of mapM becomes (t a -> t b)? How would (t a -> t b) be a case of (m ( m a))? – Xcode23
Again I don't have much time (might make this into an answer later if no-one else has done it yet), but the output of mapM is t a -> m (t b). If m is the monad (->) (t a) then that's the same as t a - > t a -> t b - or m (m (t b)) for the same monad. join turns that into m (t b), or t a -> t b. – Robin Zigmond

2 Answers

5
votes

First you specialize mapM to:

mapM' :: Traversable t => (a -> x -> b) -> t a -> x -> t b

(since (->) x is a monad)

Then you specialize it further to:

mapM'' :: Traversable t => (a -> t a -> b) -> t a -> t a -> t b

(we're just fixing the x to be t a)

Finally we specialize join appropriately:

join' :: (x -> x -> r) -> x -> r

(again, (->) x is a monad)

And hopefully it becomes more apparent why the composition join' . mapM'' is

join' . mapM'' :: Traversable t => (a -> t a -> b) -> t a -> t b
2
votes

Maybe the following will be more illuminating, instead :

flip mapT :: (Traversable t, Monad m) => t a -> (a -> m b) -> t (m b)
sequenceA :: (Traversable t, Monad m) =>                      t (m b) -> m (t b)
flip mapM :: (Traversable t, Monad m) => t a -> (a -> m b)            -> m (t b)

           flip liftM :: Monad m      => m a -> (a -> m b) -> m (m b)
 join                 :: Monad m      =>                      m (m b) -> m    b
(join .) . flip liftM :: Monad m      => m a -> (a -> m b)            -> m    b
(>>=)                 :: Monad m      => m a -> (a -> m b)            -> m    b

(using some more specialized types than the most general ones, here and there; also with the renamed mapT f = runIdentity . traverse (Identity . f)).

Your specific question is less interesting. Type derivation is a fully mechanical process. Some entities must be compatible for the whole expression to make sense, so their types must unify:

 (join . mapM) a_mb  x  =       -- a_mb :: a -> m b
 = join (mapM  a_mb) x
 = join   ta_mtb     x          -- ta_mtb :: t a -> m (t b)

To join a function is to call it twice,

 =        ta_mtb     x  x

which means x is a t a and so m is t a ->: 

        x :: t a 
 ta_mtb   :: t a -> m   (t b)
 ----------------------------
 ta_mtb x ::        m   (t b)
          ~       t a -> t b
          x ::    t a 
 ----------------------------
 ta_mtb x x ::           t b

thus a_mb :: a -> m b ~ a -> t a -> b.