In Category Theory for Programmers by Bartosz Milewski, Milewski writes the following code to define return and the 'fish' operator (composition in Kleisli category) for the Writer monad.
return :: a -> Writer a
return x = (x, "")
(>=>) :: (a -> Writer b) -> (b -> Writer c) -> (a -> Writer c)
m1 >=> m2 = \x ->
let (y, s1) = m1 x
(z, s2) = m2 y
in (z, s1 ++ s2)
He then proceeds to define fmap as follows:
fmap f = id >=> (\x -> return (f x))
I have difficulties understanding how the id function is used here. The first argument to the fish operator clearly is (a -> Writer b) but id has the type signature a -> a.
Is this an error or a flaw in my understanding? Replacing id with return makes more sense to me.
Don't forget the universal quantifications.
Fish (>=>) has type (a -> Writer b) -> ..... for any a and b.
id has type a -> a for any a.
Hence, in particular, fish also has type (Writer b -> Writer b) -> ... for any b (just take a = Writer b as a special case).
Further, id has also type Writer b -> Writer b (again, as a special case).
The "trick" here is to "merge" the two types using unification.
We start by requiring (a -> Writer b) = (a' -> a'), and then we infer a = a' and Writer b = a'. From here, we can see that these two types can be unified, so there is no contradiction in passing the arguments.
(Also note that here we renamed the a in the type of id to a' to avoid confusion with the other a for the fish)