Signature of `join bimap` in Haskell

Question

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.

Answer 1

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.

Answer 2

Here is the full instantiation of join and bimap using visible type applications. It's messy as there is a lot happening behind the scenes

joinBimap :: forall bi a a'. Bifunctor bi => (a -> a') -> (bi a a -> bi a' a')
joinBimap = join @((->) (a -> a')) @(bi a a -> bi a' a') (bimap @bi @a @a' @a @a')

Here is the output of join @((->) _) bimap in ghci, with and without bimap

>> :set -XTypeApplications
>> import Control.Monad (join)
>> import Data.Bifunctor (Bifunctor(bimap))
>>
>> :t join @((->) _) bimap
.. :: Bifunctor p => (c -> b) -> p c c -> p b b
>> :t join @((->) _)
.. :: (_ -> _ -> a) -> _ -> a

The only sensible implementation with the type of join @((->) _) is

joinReader :: (env -> env -> a) -> (env -> a)
joinReader (·) env = env · env

---

It is tricky to introduce type variable in ghci. We don't have the means to write something like \@a @a' -> join @((->) (a -> a')).

One way without adding arguments to the function is to give it a partial type signature that quantifies the new type variables

>> :set -XScopedTypeVariables
>> :set -XPartialTypeSignatures -Wno-partial-type-signatures
>>
>> :t join @((->) (a -> a')) bimap :: forall a a'. _
.. :: Bifunctor p => (a -> a') -> p a a -> p a' a'

It is also possible to take a proxy object which it has to be applied to to get the expected term. If the type variables are more than one, or of other kinds than Type a proxy object like \(_ :: _ a a') -> .. can be used.

>> :t (\(_ :: a) (_ :: a') -> join @((->) (a -> a'))) undefined undefined
.. :: ((a1 -> a') -> (a1 -> a') -> a2) -> (a1 -> a') -> a2
>>
>> import Data.Function ((&))
>> :t undefined & \(_ :: _ a a') -> join @((->) (a -> a')
.. :: ((a1 -> a') -> (a1 -> a') -> a2) -> (a1 -> a') -> a2

Answer 3

Type derivation is a purely mechanical affair:

join foo x = foo x x
=>
join bimap x = bimap x x 
  :: ( ((a->b)~(c->d)) => p a c -> p b d ) 
  ~  (   (a~c, b~d)    => p a c -> p b d ) 
  ~  p c c -> p d d

And again, slower:

bimap :: Bifunctor p => (a -> b) -> (c -> d) -> p a c -> p b d
bimap (x :: a -> b) (y :: c -> d) :: Bifunctor p => p a c -> p b d
                     x :: a -> b
----------------------------------
                         a~c, b~d
----------------------------------
bimap (x :: a -> b) (x :: a -> b) :: Bifunctor p => p c c -> p d d

And why is join foo x = foo x x, you ask? We don't even know what this foo is? But we see that the result of join foo is a function, as we apply it to an x. And with functions,

join :: Monad m        => m      (m      a)  -> m      a
     :: Monad ((->) r) => (->) r ((->) r a)  -> (->) r a
     :: Monad ((->) r) => (r  -> (r  ->  a)) -> (r ->  a)
     :: Monad ((->) r) => (r  ->  r  ->  a ) ->  r ->  a 
     foo               :: (r  ->  r  ->  a ) 
---------------------------------------------
join foo                                     ::  r ->  a

join foo is a function; hence foo is a function, foo :: r -> r -> a:

join foo                                         x =   a
  where
  a = foo                  x      x -- :: a

Here we've even derived an implementation for join on functions, mechanically, from its type.