Type of `foldMap . foldMap`

Question

(This is an from exercise in the Typeclassopedia.)

How do I calculate the type of the composition of two non-trivial functions such as foldMap . foldMap?

For simple cases, it's easy: Just look at the type of (.)

(.) :: (b -> c) -> (a -> b) -> (a -> c)

and find the types a, b and c for the two functions.

In the case of foldMap, the type is

foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m

I see no way to “split” the type of this function into two parts so I can get an “a”, “b” and “c” as in the type for (.).

I then asked ghci to calculate its type. It succeeded with the following type:

Prelude Data.Foldable> :t foldMap . foldMap 
foldMap . foldMap
  :: (Foldable t, Foldable t1, Data.Monoid.Monoid m) =>
     (a -> m) -> t (t1 a) -> m

How can I derive that type from foldMap and (.)'s types? I'm especially confused as to how the “new” type t (t1 a) that is not found in foldMap's type can show up in the type for foldMap . foldMap.

Answer 1

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.

Answer 2

foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m

can also be seen as

foldMap :: (Foldable t, Monoid m) => (a -> m) -> (t a -> m)

since -> associates to the right. Inserted into the definition of

(.) :: (y -> z) -> (x -> y) -> (x -> z)

we get that

x = (Monoid m) => a -> m
y = (Foldable ty, Monoid m) => ty a -> m

And here you gotta replace a with ty a in foldMap:

z = (Foldable ty, Foldable tz, Monoid m) => tz (ty a) -> m

What you get out of (.) is

x -> z

which is just another way of saying

(Foldable ty, Foldable tz, Monoid m) => (a -> m) -> (tz (ty a) -> m)

which, when the unnecessary parentheses are removed is

(Foldable ty, Foldable tz, Monoid m) => (a -> m) -> tz (ty a) -> m

or – as ghci writes it –

(Foldable t, Foldable t1, Monoid m) => (a -> m) -> t (t1 a) -> m

Answer 3

Omitting the typeclass constraints for the moment, the signature for foldMap and (.) may be written:

foldMap :: (a -> m) -> (t a -> m)
    (.) :: (y -> z) -> (x -> y) -> (x -> z) -- this is just a change of variables

Here we have used the fact that function application associates to the right.

So analyzing the type signature of foldMap . foldMap sets up these correspondences:

      foldMap          .              foldMap
(a -> m) -> (t a -> m)   ( a' -> m') -> (t' a' -> m')    (a' -> m') -> (t a -> m)
  (y     ->    z)     ->        (x   ->   y)          ->     (x     ->    z)

I.e. we have the following type equalities:

y = a -> m
z = t a -> m
x = a' -> m'
y = t' a' -> m'
x = a' -> m'
z = t a -> m

which reduces to:

a = t' a'
m = m'

i.e. the type of foldMap . foldMap is (a' -> m) -> (t (t' a') -> m) or equivalently (a' -> m) -> t (t' a) -> m.