为什么这个函数不能typecheck？

Question

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

预计此函数将无法typeCheck。然而，没有解释发生这种情况的原因。在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.

为什么会出现这种情况？

Answer 1

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。不能在同一使用站点实例化为不同的类型。这是“1级息肉”。

您可以将该类型读为：

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

所以：

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

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)

Prelude> f True 7 (const 1)
14