Manually deriving the type of `zipWith . uncurry`

Question

I'm trying to derive the type of zipWith . uncurry

zipWith . uncurry = (.) zipWith uncurry -- concatenation as function

(.) :: (b1 -> c1) -> (a1 -> b1) -> a1 -> c1
zipWith :: (a2 -> b2 -> c2) -> [a2] -> [b2] -> [c2]
uncurry :: (a3 -> b3 -> c3) -> (a3, b3) -> c3

b1 ~ (a2 -> b2 -> c2)
c1 ~ [a2] -> [b2] -> [c2]
a1 ~ (a3 -> b3 -> c3)
b1 ~ (a3, b3) -> c3

Replacing a1 with (a3 -> b3 -> c3) and c1 with [a2] -> [b2] -> [c2] I get:

(.) zipWith uncurry :: a1 -> c1 ~ (a3 -> b3 -> c3) -> [a2] -> [b2] -> [c2]

If I query GHCi for :t zipWith . uncurry I get: (a -> b1 -> b -> c) -> [(a, b1)] -> [b] -> [c]

I think the key is in b1 ~ (a2 -> b2 -> c2) ~ (a3, b3) -> c3 but I don't realize how to match my result with the expected.

Any help?

Thanks,
Sebastián.

Answer 1

If we start with

(.) :: (b -> c) -> (a -> b) -> (a -> c)
zipWith :: (x -> y -> z) -> [x] -> [y] -> [z]
uncurry :: (u -> v -> w) -> (u, v) -> w

Then we match zipWith's type with (b -> c) and uncurry's type with (a -> b):

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

And

a             -> b
(u -> v -> w) -> ((u, v) -> w)

Then we have to equate the b terms

b ~ x      -> (y -> z)
b ~ (u, v) -> w

So w ~ (y -> z) and x ~ (u, v). A table of what we've determined so far:

a ~ u -> v -> w
b ~ x -> y -> z
c ~ [x] -> [y] -> [z]
x ~ (u, v)
w ~ y -> z

So we can substitute x and w in:

a ~ u -> v -> (y -> z)
b ~ (u, v) -> y -> z
c -> [(u, v)] -> [y] -> [z]

And we can now complete the type of zipWith . uncurry:

(u -> v -> y -> z) -> ([(u, v)] -> [y] -> [z])

Which lines up with GHCi's answer as well.

The trick to these is just to line up the arrows and then just substitute back in until you can't reduce it any more.