Haskell中的Lambda演算：是否有一种方法使Church数在类型检查时通过？

Question

我正在使用Haskell玩一些lambda演算的东西，具体来说是关于Church数。 我定义了以下内容：

let zero = (\f z -> z)
let one = (\f z -> f z)
let two = (\f z -> f (f z))
let iszero = (\n -> n (\x -> (\x y -> y)) (\x y -> x))
let mult = (\m n -> (\s z -> m (\x -> n s x) z))

这个有效：

:t (\n -> (iszero n) one (mult one one))

这个操作会因为出现检查而失败：

:t (\n -> (iszero n) one (mult n one))

我已经使用我的常量玩了一下iszero和mult，它们似乎是正确的。有没有什么方法可以使这些可输入？我认为我所做的并不太疯狂，但也许我做错了什么？

- singpolyma

Answer 1

你的定义和它们的类型在顶层看起来是正确的。问题在于，在第二个例子中，你使用了n两种不同的方式，它们的类型不能统一，尝试这样做会产生无限类型。类似one的使用可以正常工作，因为每个使用都独立地专门用于不同的类型。

要使其直接运行，您需要更高级别的多态性。一个 church 数字的正确类型是 (forall a. (a -> a) -> a -> a)，但更高级别的类型不能被推断出，并需要 GHC 扩展，例如RankNTypes。如果您启用了适当的扩展（在这种情况下只需要等级2，我想），并为您的定义给出显式类型，则它们应该能够在不改变实际实现的情况下工作。

请注意，对更高阶多态类型的使用存在（或者至少曾经存在）一些限制。但是，你可以将你的 church 数字包装在类似于newtype ChurchNum = ChurchNum (forall a. (a -> a) -> a -> a)的东西中，这将允许它们拥有一个Num实例。

- C. A. McCann

---

哇，你说得对。我没想到这么基本的东西需要更高阶的多态性，但我猜这就是来自于 λ演算是无类型的。 - singpolyma

有人认为，更高阶的多态性本身对于多态类型的λ演算是基本的，而不是允许完全类型推断所必需的额外限制。 - C. A. McCann

@singpolyma：顺便说一下，当你尝试实现类似于mult m n = m (plus n) zero这样的东西时，上述限制将会发挥作用，这是未类型化lambda中的有效表达式，但在类型化中需要不定量多态性。这是Oleg的解决方法：http://okmij.org/ftp/Haskell/types.html#some-impredicativity - Ed'ka

Answer 2

让我们添加一些类型签名：

type Nat a = (a -> a) -> a -> a

zero :: Nat a
zero = (\f z -> z)

one :: Nat a
one = (\f z -> f z)

two :: Nat a
two = (\f z -> f (f z))

iszero :: Nat (a -> a -> a) -> a -> a -> a
iszero = (\n -> n (\x -> (\x y -> y)) (\x y -> x))

mult :: Nat a -> Nat a -> Nat a
mult = (\m n -> (\s z -> m (\x -> n s x) z))

正如您所看到的，除了iszero的类型之外，一切都很正常。

让我们来看看您的表达式会发生什么：

*Main> :t (\n -> (iszero n) one n)
<interactive>:1:23:
    Occurs check: cannot construct the infinite type:
      a0
      =
      ((a0 -> a0) -> a0 -> a0)
      -> ((a0 -> a0) -> a0 -> a0) -> (a0 -> a0) -> a0 -> a0
    Expected type: Nat a0
      Actual type: Nat (Nat a0 -> Nat a0 -> Nat a0)
    In the third argument of `iszero', namely `(mult n one)'
    In the expression: (iszero n) one (mult n one)

看看这个错误如何使用我们的 Nat 别名！

实际上，我们可以通过更简单的表达式 \n -> (iszero n) one n 得到类似的错误。以下是问题所在。由于我们在调用 iszero n，因此我们必须有 n :: Nat (b -> b -> b)。此外，由于 iszero 的类型要求第二和第三个参数 n 和 one 必须具有类型 b。现在我们有了两个关于 n 类型的方程式:

n :: Nat (b -> b -> b)
n :: b

这是无法调和的。很遗憾。

- opqdonut