为什么此功能无法进行类型检查？

Question

在关于函数式编程的讲座中，我们看到了以下 Haskell 函数：

f :: Bool -> Int -> (a -> Int) -> Int
f x y z = if x then y + y else (z x) + (z y)

预计此函数将无法进行类型检查。但是，没有解释发生这种情况的原因。在 GHCI 中尝试时，我得到以下输出：

Prelude> :l test [1 of 1] 编译 Main ( test.hs, 解释） 测试.hs:2:35: 无法将预期类型“a”与实际类型“Bool”匹配 `a' 是一个刚性类型变量，由 f :: Bool -> Int -> (a -> Int) -> Int 的类型签名 在 test.hs:1:6 相关绑定包括 z :: a -> Int（绑定在 test.hs:2:7） f :: Bool -> Int -> (a -> Int) -> Int (绑定在 test.hs:2:1) 在“z”的第一个参数中，即“x” 在 `(+)' 的第一个参数中，即 `(z x)' 失败，加载的模块：无。

为什么会这样？

Answer 1

这根本不是简单的参数多态性的工作原理。函数z 在函数签名中是多态的，但在主体中它是唯一的单态。

在对定义进行类型检查时，类型检查器会推断类型变量 a 的单态类型，以在整个函数定义中使用。但是，您的 f 尝试使用两种不同的类型调用 z，因此类型检查器会推断出 a 的两种冲突类型。

Answer 2

f :: Bool -> Int -> (a -> Int) -> Int
f x y z = if x then y + y else (z x) + (z y)

类型签名断言我们的函数z 在其第一个参数中是多态的。它接受任何类型的值a 并返回Int。但是，类型变量a 的作用域也意味着它在所有使用中都必须是相同的类型a。 a 不能在同一使用站点实例化为不同类型。这是“等级 1 多态性”。

你可以把类型当真：

f :: forall a. Bool -> Int -> (a -> Int) -> Int

所以：

z (x :: Bool) + z (y :: Int)

无效，因为a 被限制为两种不同的独立类型。

语言扩展允许我们更改a 的范围，以便可以将其实例化为多态变量——即在同一使用站点保存不同类型，包括具有多态函数类型：

Prelude> :set -XRankNTypes

Prelude> let f :: Bool -> Int -> (forall a . a -> Int) -> Int 
             f x y z = if x then y + y else (z x) + (z y)

现在a 类型没有全局作用域，各个实例化可能会有所不同。 这让我们可以编写“更多态”的函数f 并使用它：

Prelude> f True 7 (const 1)
14

这就是高阶多态性的酷炫之处。更多代码重用。

Answer 3

均匀

f :: Bool -> Int -> (a -> Int) -> Int
f x y z = if x then y + y else (z y) + (z y)

不会进行类型检查（正如 cmets 中指出的那样），并产生相同的错误，因为 Haskell 为表达式推断 最不通用的类型，并且您的类型比推断的更通用。正如"A Gentle Introduction to Haskell" 所说，

表达式或函数的主要类型是最不通用的类型，直观地说，“包含表达式的所有实例”。

如果你明确指定一个类型，Haskell 会假设你这样做是有原因的，并坚持将推断的类型与给定的类型相匹配。

对于上面的表达式，推断类型是(Num t) => Bool -> t -> (t -> t) -> t，所以在匹配类型时，它看到你给y 提供了Int，z 的类型变成了(Int -> Int)。与(a -> Int) 相比更少。但是你坚持在那里有一个a（不是Int）——一个rigid类型的变量。换句话说，您的函数f 只能接受Int -> Int 类型的函数，但您坚持可以赋予它any 函数:: a -> Int，包括:: String -> Int 等（如@ augustsson 在 cmets 中指出）。您声明的类型过于宽泛。

类似地，如果您只有一个(z x)，它将与x 的给定类型匹配，并为z 函数到达比声明类型(Bool -> Int) 更窄的值。又一次抱怨严格的类型变量。

实际上，您声明了 (Num t) => Bool -> t -> (t1 -> t) -> t 类型，但它实际上是 (Num t) => Bool -> t -> (t -> t) -> t。它是一种不同的类型。