The same equational reasoning techniques that work in the simple case will keep working in this more complicated case. One important thing to remember which enables this is that ->
is right-associative; this means that a -> b -> c
is the same as a -> (b -> c)
; consequently, all functions in Haskell take in exactly one input and produce exactly one output, and so can be composed. (This equivalence is what lies behind the ability to do partial application everywhere.) Thus, we can rewrite the type signature for foldMap
as
foldMap :: (Foldable t, Monoid m) => (a -> m) -> (t a -> m)
For clarity, I'm going to give the two different occurrences of foldMap
different names and use different names for their type variables; we'll have foldMap₂ . foldMap₁
, where
foldMap₁ :: (Foldable s, Monoid n) => (a -> n) -> (s a -> n)
foldMap₂ :: (Foldable t, Monoid m) => (b -> m) -> (t b -> m)
(.) :: (d -> e) -> (c -> d) -> (c -> e)
Thus, it must be the case that
foldMap₂ . foldMap₁ :: c -> e
But what are c
and e
, and what's the d
that allows this to work? Leaving off the class constraints (they simply get unioned together at the end, and will clutter everything up along the way), we know that
foldMap₂ . foldMap₁ ---+
|
|
/-------foldMap₂-------\ /-------foldMap₁-------\ /---+--\
(.) :: (d -> e ) -> (c -> d ) -> (c -> e)
((b -> m) -> (t b -> m)) -> ((a -> n) -> (s a -> n))
This gives rise to the following equalities (remember that Haskell spells type equality ~
):
(c -> d) ~ ((a -> n) -> (s a -> n))
(d -> e) ~ ((b -> m) -> (t b -> m))
Because these are equalities on function types, we know that the domains and ranges, respectively, are equal to each other:
c ~ (a -> n)
e ~ (t b -> m)
d ~ (b -> m)
d ~ (s a -> n)
We can collapse the d
equalities to conclude, by transitivity, that
(b -> m) ~ (s a -> n)
And then, since both sides are function types, we can break this equality apart to conclude that
b ~ s a
m ~ n
So d ~ (s a -> n)
, or in other words just the result type of foldMap₁
—the trick is that b -> m
, the input type of foldMap₂
, is generic enough to unify with the former type! (Here, unification is what the type inferencer does; two types can unify if they could be the same when more specific types were substituted in for the type variables.)
Finally, then, substituting in for c
and e
, we get
(c -> e) ~ ((a -> n) -> e) by the equality for c
~ ((a -> n) -> (t b -> m)) by the equality for e
~ ((a -> m) -> (t b -> m)) by the equality for n
~ ((a -> m) -> (t (s a) -> m)) by the equality for b
Thus, when we add back the complete list of class constraints (remember that Monoid m
and Monoid n
are actually the same constraint, since m ~ n
) and drop the redundant pairs of parentheses, we get
foldMap . foldMap :: (Foldable s, Foldable t, Monoid m)
=> (a -> m) -> t (s a) -> m
Which, up to renaming, is the same as what GHCi gave you.
Note the last step in particular, where the nested type t (s a)
shows up. That comes from the unification of b
above, inside the equalities about d
. We know that the result type of foldMap₂ . foldMap₁
is going to be t b -> m
for some b
; it so happens that unifying the output of foldMap₁
and the input of foldMap₂
constrains b
to be the type s a
. We can always unify type variables with more complicated type expressions (as long as the more complicated expression doesn't involve the original type variable; b
and t b
will fail to unify), which sometimes leads to interesting types like t (s a)
when it happens behind the scenes.