Вручную получим тип `zipWith . uncurry`

Question

Я пытаюсь вывести тип zipWith . uncurry

zipWith . uncurry = (.) zipWith uncurry - конкатенация как функция

(.) :: (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

Замена a1 с (a3 -> b3 -> c3) а также c1 с [a2] -> [b2] -> [c2] Я получил:

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

Если я запрашиваю GHCi для :t zipWith . uncurry Я получил: (a -> b1 -> b -> c) -> [(a, b1)] -> [b] -> [c]

Я думаю, что ключ в b1 ~ (a2 -> b2 -> c2) ~ (a3, b3) -> c3 но я не понимаю, как сопоставить мой результат с ожидаемым.

Любая помощь?

Спасибо,
Себастьян.

Answer 1

Если мы начнем с

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

Тогда мы подходим zipWithТип с (b -> c) а также uncurryТип с (a -> b):

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

А также

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

Тогда мы должны приравнять b термины

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

Так w ~ (y -> z) а также x ~ (u, v), Таблица того, что мы определили до сих пор:

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

Таким образом, мы можем заменить x а также w в:

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

И теперь мы можем завершить тип zipWith . uncurry:

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

Что совпадает с ответом GHCi.

Хитрость заключается в том, чтобы выровнять стрелки, а затем просто заменить их обратно, пока вы не сможете больше их уменьшить.