为什么这个函数无法进行类型检查？

Question

为什么这个函数无法进行类型检查？

haskellpolymorphismparametric-polymorphism

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] Compiling Main             ( test.hs,
interpreted )
test.hs:2:35:
    Couldn't match expected type `a' with actual type `Bool'
      `a' is a rigid type variable bound by
          the type signature for f :: Bool -> Int -> (a -> Int) -> Int
          at test.hs:1:6
    Relevant bindings include
      z :: a -> Int (bound at test.hs:2:7)
      f :: Bool -> Int -> (a -> Int) -> Int (bound at test.hs:2:1)
    In the first argument of `z', namely `x'
    In the first argument of `(+)', namely `(z x)' Failed, modules loaded: none.

为什么会发生这种情况？

- aochagavia

2

假设我像这样调用 f：f True 3 (\n -> n+1)。你会期望发生什么？ - Tom Ellis

3

记住，类型 f :: Bool -> Int -> (a -> Int) -> Int 意味着调用者可以选择 a 的类型。因此，调用者完全可以选择一个类型为 String -> Int 的函数。 - augustss

3个回答

3

这并不是简单的参数多态的工作方式。函数z在函数签名中是多态的，但在函数体内只有单态。在类型检查定义时，类型检查器会为类型变量a推断出单态类型，以在函数定义中使用。然而，您的f尝试使用两种不同的类型调用z，因此类型检查器为a推断出了两种冲突的类型。

- user355252

2

Even

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`，因此在匹配类型时，它看到你给出了 `Int` 作为 `y` 的类型，`z` 的类型变成了 `(Int -> Int)`。这比 `(a -> Int)` 更不一般。但是，你坚持在那里有一个 `a`（而不是 `Int`）——一个刚性类型变量。换句话说，你的函数 `f` 只能接受类型为 `Int -> Int` 的函数，但你坚持它可以被赋予任何函数 `:: 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。这是不同的类型。

- Will Ness

1

我意识到了这一点，并用 a 进行了回退。 :) - Sibi

啊，刚看到了。 :) 谢谢你提供那个例子，这澄清了问题。 - Will Ness

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Don Stewart · Accepted Answer

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实例化为不同的类型。这就是“rank 1 polymorphism”（一阶多态性）。

您可以将该类型读作：

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

那就是高级多态性的厉害之处了。更多的代码重用。