I've been studying the category theory for about three months now. Recently, I felt surprised with the definition of Haskell's Bifunctor:

class Bifunctor f where

    // type signatures
    bimap :: (a -> c) -> (b -> d) -> f a b -> f c d
    first :: (a -> c) -> f a b -> f c b
    second :: (b -> d) -> f a b -> f a d

    // default implementations
    bimap g h = first g · second h // <--- surprising composition
    first g = bimap g id
    second h = bimap id

I felt surprised that first g would compose with second h. I felt confused because...

  1. The return type of second h is f a d.
  2. The argument of first g is f a b.
  3. How can f a d go into f a b?

This is how I reasoned through it. I started with the default implementation of bimap, which has the surprising composition, and used equational reasoning (of a kind) to convert the composition into a type signature. The final type signature has two unknown types x and y.

// default implementation of `bimap`
bimap g h = first g · second h

// replace `g` and `h` with their type signatures
bimap (a -> c) (b -> d) :: first (a -> c) · second (b -> d)

// replace `first (a -> c)` with its return type
// using the types from the bimap scope
bimap (a -> c) (b -> d) :: (f a x -> f c x) · second (b -> d)

// replace `second (b -> d)` with its return type
// using the types from the bimap scope
bimap (a -> c) (b -> d) :: (f a x -> f c x) · (f y b -> f y d)

I noticed that my substitution left x and y as unknown types. That is because first ignores the b that bimap receives, and second ignores the a that bimap receives. At this piont, all we know from the type signatures of first and second is that neither x nor y change. I decided to try to infer the types of x and y based on the assumption that first and second compose.

Here is how I did the manual type inference.

// write the target signature for bimap from its definition
bimap :: (a -> c) -> (b -> d) -> f a b -> f c d

// write the target signature after partial application with `g` and `h`
bimap (a -> c) (b -> d) :: f a b -> f c d

// notice that the target signature's returns type is the function (f a b -> f c d)

// use the target return type to infer the unknown typse
bimap (a -> c) (b -> d) 
    // number the unknown types
    :: (f a x1 -> f c x2) · (f y1 b -> f y2 d)

    // `x2` must be `d` to produce the target (f c d) 
    :: (f a x1 -> f c d) · (f y1 b -> f y2 d)

    // `y1` must be `a` to produce the target (f a b) 
    :: (f a x1 -> f c d) · (f a b -> f y2 d)

    // `y2` must be `a` because it is the same type as y1
    :: (f a x1 -> f c d) · (f a b -> f a d)

    // `x1` must be `d` because it is the same type as x2
    :: (f a d -> f c d) · (f a b -> f a d)

    // perform the composition
    :: (f a b -> f c d)

Lo and behold the composition lands at the target return type.

The type inference demonstrated that, in order for the composition to work, the implementations of first and second must adhere to these constraints:

  1. first must not change its second argument's type
  2. first must change a into c
  3. second must not change its first argument's type
  4. second must change b into d

With some more equational reasoning (of a type) we can see that the default implementations of first and second adhere to those constraints.

first g = bimap g id

// replace `bimap g id` with its type
first g :: (a -> c) -> (x -> x) -> f a x -> f c x

second h = bimap id

// replace `bimap id h` with its type
second h :: (x -> x) -> (b -> d) -> f a b -> f c d

Result: I have convinced myself that first and second do compose.