Deriving the type of ((.) foldr)

Question

I'm trying to manually derive the type of ((.) foldr)

(.) ::(b1 -> c1) -> (a1 -> b1) -> a1 -> c1
foldr :: (a2 -> b2 -> b2) -> b2 -> [a2] -> b2

Then:

b1 = a2 -> b2 -> b2
c1 = b2 -> [a2] -> b2

Matching the types I get:

((a2 -> b2 -> b2) -> (b2 -> [a2] -> b2)) -> (a1 -> (a2 -> b2 -> b2)) -> a1 -> (b2 -> [a2] -> b2)

But then I get confused on how to reduce this expresion.

Any help?

Thansks,
Sebastián.

Answer 1

Your correctly figured out the type of the (.) in (.) foldr. The (.) is applied to one argument (the foldr) so you can throw away the ((a2 -> b2 -> b2) -> (b2 -> [a2] -> b2)) and what remains is the type of (.) foldr:

(a1 -> a2 -> b2 -> b2) -> a1 -> (b2 -> [a2] -> b2)

Make sure that foldr can have type ((a2 -> b2 -> b2) -> (b2 -> [a2] -> b2)) before you throw it away. If you got the matching right, this check cannot fail, but it is a good sanity check.

Answer 2

If we have

(.)   :: (b -> c) -> (a -> b) -> (a -> c)
foldr :: (x -> y -> y) -> y -> [x] -> y

Then for (.) foldr, the b -> c has to line up with the type of foldr, so

b             -> c
(x -> y -> y) -> (y -> [x] -> y)

Which implies

b ~ (x -> y -> y)
c ~ (y -> [x] -> y)

So substituting back in:

--                 b                       c
(.) foldr :: (a -> (x -> y -> y)) -> (a -> (y -> [x] -> y))

Since -> is left associative, we can drop the extra parentheses:

(.) foldr :: (a -> x -> y -> y) -> (a -> y -> [x] -> y)

And if you want you can go a step further with

(.) foldr :: (a -> x -> y -> y) -> a -> y -> [x] -> y

So if we ask GHCi what the type is, we get

> :t (.) foldr
(.) foldr :: (a -> a1 -> b -> b) -> a -> b -> [a1] -> b

Where a ~ a, a1 ~ x, and b ~ y, so we've arrived at the correct answer.