5

在关于函数式编程的讲座中，我们看到了以下 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”
    在 `(+)' 的第一个参数中，即 `(zx)' 失败，加载的模块：无。

为什么会这样？

4

3 回答 3

9 
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

这就是高阶多态性有多酷。更多代码重用。

于 2014-09-16T11:07:54.520 回答
3

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

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

于 2014-09-16T10:50:50.517 回答
2

甚至

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

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

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

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

对于上面的表达式，推断的类型是(Num t) => Bool -> t -> (t -> t) -> t，因此在匹配类型时，它会看到您给出了Intfory并且类型z变为(Int -> Int)。这不如(a -> Int). _ 但是你坚持要有一个athere （不是一个Int）——一个严格的类型变量。换句话说，您的函数f只能接受 type 的函数Int -> Int，但您坚持认为它可以被赋予任何function :: a -> Int，包括:: String -> Int等（正如@augustsson 在评论中指出的那样）。您声明的类型太宽泛。

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

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

于 2014-09-16T16:19:49.163 回答