手动派生 `zipWith 的类型。不咖喱`答案

【问题标题】：Manually deriving the type of `zipWith . uncurry`手动派生 `zipWith 的类型。不咖喱`
【发布时间】：2014-05-03 00:43:51
【问题描述】：

我正在尝试导出 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，但我不知道如何将我的结果与预期相匹配。

有什么帮助吗？

谢谢，
塞巴斯蒂安。

【问题讨论】：

当zipWith 函数使用两个参数时，uncurry 有什么好处。 zipWith (enumFromTo) [0,2..6] [1,3..7] 产生 [[0,1],[2,3],[4,5],[6,7]] 或像zipWith (:) [0,2..6] [[n]|n<-[1,3..7]] 一样为其提供适当的参数产生非常相同. (:) 的第二个参数必须是一个列表。

标签： haskell types ghci unification

【解决方案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 的答案。

解决这些问题的诀窍就是将箭头对齐，然后再替换回去，直到你不能再减少它。

【讨论】：