(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
.
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 thata -> b -> c
is the same asa -> (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 forfoldMap
asFor clarity, I'm going to give the two different occurrences of
foldMap
different names and use different names for their type variables; we'll havefoldMap₂ . foldMap₁
, whereThus, it must be the case that
But what are
c
ande
, and what's thed
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 thatThis gives rise to the following equalities (remember that Haskell spells type equality
~
):Because these are equalities on function types, we know that the domains and ranges, respectively, are equal to each other:
We can collapse the
d
equalities to conclude, by transitivity, thatAnd then, since both sides are function types, we can break this equality apart to conclude that
So
d ~ (s a -> n)
, or in other words just the result type offoldMap₁
—the trick is thatb -> m
, the input type offoldMap₂
, 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
ande
, we getThus, when we add back the complete list of class constraints (remember that
Monoid m
andMonoid n
are actually the same constraint, sincem ~ n
) and drop the redundant pairs of parentheses, we getWhich, 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 ofb
above, inside the equalities aboutd
. We know that the result type offoldMap₂ . foldMap₁
is going to bet b -> m
for someb
; it so happens that unifying the output offoldMap₁
and the input offoldMap₂
constrainsb
to be the types 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
andt b
will fail to unify), which sometimes leads to interesting types liket (s a)
when it happens behind the scenes.