How does the relationship between bisequence and bitraverse work in Haskell?

Question

I'm having some trouble "mentally type checking" the relationship between bisequence and bitraverse in Haskell. Here are their signatures, according to the documentation:

bisequence :: (Bitraversable t, Applicative f) => t (f a) (f b) -> f (t a b)
bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> t a b -> f (t c d)

Also according to the documentation, the following relationship holds:

bisequence ≡ bitraverse id id

But this relationship doesn't make sense to me:

• The signature of id is a -> a, so how can it be accepted as the first or second argument to bitraverse, which wants e.g. a -> f c?

• Even if we overcome the first point, the type of bitraverse id id should be Bitraversable t => t a b -> f (t c d), right? But that's not the same as the type of bisequence; it is missing an applicative later on the a and b in the input.

What am I missing? I'm sure these two misunderstandings are related, because they are both about missing applicative layers in the type.

Answer 1

Let's break down all of the variables.

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> t a b -> f (t c d)

Now we have id :: x -> x (I'm using a different variable name here so we don't get confused using the same name to mean two different things). Then when we write bitraverse id, we have that id must unify with the first argument of bitraverse, so

a -> f c ~ x -> x

(~ is the unification relation)

Hence, a ~ x and f c ~ x. Substituting that in gives us

bitraverse id :: Applicative f => (b -> f d) -> t (f c) b -> f (t c d)

Rinse and repeat for the second id, which we'll say has type signature id :: y -> y. We want to unify

b -> f d ~ y -> y

So b ~ y and f d ~ y, by the same logic. Hence,

bitraverse id id :: Applicative f => t (f c) (f d) -> f (t c d)

which is

bisequence :: Applicative f => t (f a) (f b) -> f (t a b) 

by another name.

Notably, when we said the argument to bitraverse was a -> f c, we never said that a wasn't equal to f c. a could be literally anything, and in this case we chose it to be equal to f c (mandated by unification with the type of id).