haskell - 为什么要进行以下类型检查？

Question

为什么要进行以下类型检查？

cancel x y = x
distribute f g x = f x (g x)
identity = distribute cancel cancel

清楚 cancel :: a -> b -> a , distribute :: (a -> b -> c) -> (a -> b) -> a -> c和 identity :: a -> a .现在， distribute cancel :: (a -> b) -> a -> a ，但我不明白为什么 cancel与 a -> b 匹配.

有人可以向我解释一下吗？

Answer 1

让我们使所有类型变量都不同:

identity = distribute cancel1 cancel2
  where distribute :: (a -> b -> c) -> (a -> b) -> a -> c
        cancel1 :: x -> y -> x
        cancel2 :: r -> s -> r

所以，简单地排列我们需要统一的类型来证明分布式调用检查:

distribute :: (a -> b -> c) -> (a -> b)     -> a -> c
cancel1    ::  x -> y -> x
cancel2    ::                   r -> s -> r

cancel1 很明显；我们有:

a ~ x
b ~ y
c ~ x

( ~ 符号基本上是我们在 Haskell 中编写类型相等的方式；如果您打开一些扩展，您可以在实际代码中使用它)

让我们替换那些

distribute :: (x -> y -> x) -> (x -> y)     -> x -> x
cancel1    ::  x -> y -> x
cancel2    ::                   r -> s -> r

对于下一位，我们需要记住箭头是一个二元运算符。它只需要两个参数:一个参数类型和一个结果类型。所以如果我们有一个带有两个箭头的函数类型，其中一个必须在另一个的参数类型或结果类型内。在类似 r -> s -> r 的情况下，我们使用了 -> 的右结合性省略括号，这会让它变得明显:它真的是 r -> (s -> r) .1

那么:

distribute :: (x -> y -> x) -> (x ->  y      ) -> x -> x
cancel1    ::  x -> y -> x
cancel2    ::                   r -> (s -> r)

所以现在我们可以立即阅读:

x ~ r
y ~ s -> r

更多替代:

distribute :: (r -> (s -> r) -> r) -> (r -> (s -> r)) -> r -> r
cancel1    ::  r -> (s -> r) -> r
cancel2    ::                          r -> (s -> r)

因此，cancel1 忽略的是 s -> r 类型的函数，这也是 cancel2 返回的内容。记 f x (g x) distribute 的实现，这是有道理的。 cancel1 和 cancel2 都必须用同样的东西调用；然后cancel1 接收调用cancel2 的结果作为它的第二个参数，它会立即忽略它，因此cancel2 的第二个参数的类型无关紧要，因为它实际上从未在另一个参数上调用过(任何接受 r 的函数)因为它的第一个参数在这里起作用)。这是编写一个什么都不做的函数的一种精心设计的方法:身份。

1 如果您不记得是否 ->是右关联还是左关联，您可能听说过所有 Haskell 函数都接受单个参数，而我们通常通过使用返回其他函数的函数来“伪造”多参数函数。这就是这里发生的事情，以及函数箭头关联到右侧的原因。