推断 lambda 表达式的类型

Question

给定一个具有以下类型的函数 a：
a :: x -> Bool
以及以下类型的另一个函数 b：
b :: Bool -> y
我正在尝试找出推断以下函数类型的步骤：
c = \d -> d a b
有人可以帮助解释如何做到这一点，而不仅仅是通过 ghc 的 :type 函数吗？ 谢谢

Answer 1

c = \d -> d a b 的类型将是 c :: ((x -> Bool) -> (Bool -> y) -> t) -> t

其中d 是一个接收(x -> Bool) 和(Bool -> y) 并返回t 类型值的函数。

所以c是一个接收d类型函数并返回t类型值的函数

如果您的意思是c = \d -> d (a b)，则类型将为c :: (Bool -> y) -> y

一些额外的解释。

要知道c我们首先要知道d做什么所以我们看c = \d -> d a b

我们看到\d -> d a b，所以我们知道d的第一个参数是函数a，类型为(x -> Bool)。我们也知道d 的第二个参数，它是函数b，类型为(Bool -> y)。但我们不知道它返回什么，因为这是 Haskell，它必须返回一些东西，所以我只是将 t 写为未知类型。 所以d 是d :: a -> b -> t。

代入a和b的类型，我们得到d :: (x -> Bool) -> (Bool -> y) -> t。

现在对于c，c 是一个 lambda，它接受一个我们可以推断为 d 类型的值，并返回其输出。所以我们得到c :: d -> (d's output)。

代入d的类型，我们得到c :: ((x -> Bool) -> (Bool -> y) -> t) -> t

Answer 2

另一种方法是使用类型签名，以确保获得特定 lambda 表达式的类型签名，同时避免 :t。

在这种情况下，x 不受限制。

idFunction = \x -> x

如果我们想限制特定类型，我们可以直接注解x。 （这需要 GHCi 中的 :set -XScopedTypeVariables 或文件中的 {-# LANGUAGE ScopedTypeVariables #-}）。

idFunction = \(x :: Int) -> x

或者我们可以添加一个类型签名

idFunction :: Int -> Int
idFunction = \x -> x

在您的示例中，您只有类型签名，但没有函数体。让我们添加一些简单的函数体，以便我们可以使用编译器做一些事情，然后我们将尝试添加一个类型签名到 c 确认我们对类型应该是什么的信念。我们将从错误的类型签名开始。

a :: Int -> Bool
a x = x > 0

b :: Bool -> String
b y = show y

c :: ((Bool -> Bool) -> (Bool -> Bool) -> t) -> t
c = \d -> d a b

编译器会在c中发现一些错误：

<interactive>:10:17: error:
    • Couldn't match type ‘Bool’ with ‘Int’
      Expected type: Bool -> Bool
        Actual type: Int -> Bool
    • In the first argument of ‘d’, namely ‘a’
      In the expression: d a b
      In the expression: \ d -> d a b

<interactive>:10:19: error:
    • Couldn't match type ‘[Char]’ with ‘Bool’
      Expected type: Bool -> Bool
        Actual type: Bool -> String
    • In the second argument of ‘d’, namely ‘b’
      In the expression: d a b
      In the expression: \ d -> d a b

现在，如果我们给c 提供正确的类型签名，它将编译

c :: ((Int -> Bool) -> (Bool -> String) -> t) -> t
c = \d -> d a b

通常没有任何理由回避:t。当您在 GHCi 中工作时，它是一个非常好的工具，但是当您在库中构建复杂的函数时，您不一定可以访问:t，因此另一种方法是测试不同的类型签名并查看编译器的反应.