In one of the solutions on codewars I've met the following expression:
join bimap
where join :: Monad m => m (m a) -> m a,
and bimap :: Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d. The resulting expression has the type: Bifunctor p => (c -> d) -> p c c -> p d d.
I can guess that the type of bimap could be written in the form
(->) (a->b) ((->) (c->d) p a c -> p b d), but I can't figure out how p a c turns to p c c and p b d to p d d.
Please, give me some hints how to untangle this puzzle.
First, let’s look at the type of join as applied to a function. Let’s say you have a function f :: t -> u -> v; or, equivalently, f :: (->) t ((->) u v). We can attempt to unify this with join :: Monad m => m (m a) -> m a by comparing the two types:
(->) t ((->) u v)
Monad m => m (m a) -> m a
Thus, we can attempt to unify the types by setting m ~ (->) t and a ~ v:
(->) t ((->) u v)
(->) t ((->) t v) -> (->) t v
But there is a problem: we additionally need t ~ u in order for these types to match up! Thus we can conclude that join can only applied to a function when the first two arguments have the same type — and if they are not, we can only apply join to that function if there is a way to make them equal.
Now, think about bimap :: Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d. Normally, a, b, c, d and p may be any type. But if you want to apply join to bimap, this adds the constraint that the first two arguments of bimap must have the same type: that is, (a -> b) ~ (c -> d). From this we can conclude that a ~ c and b ~ d. But, of course, this implies that p a c must be the same as p a a, and p b d the same as p b b, solving the puzzle.