Haskell中的Church数的减法

Question

我正在尝试在Haskell中实现Church数，但遇到了一个小问题。当我尝试进行减法时，Haskell会抱怨出现无限类型的错误：

出现检查：无法构造无限类型：t = (t -> t1) -> (t1 -> t2) -> t2

我有99%的把握我的λ演算是正确的（如果不是，请告诉我）。我想知道的是，是否有什么方法可以让Haskell与我的函数一起工作。

module Church where

type (Church a) = ((a -> a) -> (a -> a))

makeChurch :: Int -> (Church a)
makeChurch 0 = \f -> \x -> x
makeChurch n = \f -> \x -> f (makeChurch (n-1) f x)

numChurch x = (x succ) 0

showChurch x = show $ numChurch x

succChurch = \n -> \f -> \x -> f (n f x)

multChurch = \f2 -> \x2 -> \f1 -> \x1 -> f2 (x2 f1) x1

powerChurch = \exp -> \n -> exp (multChurch n) (makeChurch 1)

predChurch = \n -> \f -> \x -> n (\g -> \h -> h (g f)) (\u -> x) (\u -> u)

subChurch = \m -> \n -> (n predChurch) m

- Probie

---

你应该使用类型声明 type Church a = (a -> a) -> a -> a，这样更加简洁，没有差别。 - alternative

还要注意，写出类型签名会非常有帮助。它会告诉你问题出在哪里... - alternative

最终我移除了类型签名，看看ghci是否能够正确推断它们，并希望能够消除错误（但错误并没有改变）...此外，我更喜欢在类型周围加上括号。这使得它更加突出。 - Probie

Answer 1

问题在于 predChurch 过于多态，无法由 Hindley-Milner 类型推断正确地推导出来。例如，人们很容易会写出以下代码：

predChurch :: Church a -> Church a
predChurch = \n -> \f -> \x -> n (\g -> \h -> h (g f)) (\u -> x) (\u -> u)

但是这种类型是不正确的。一个 Church a 的第一个参数应该是一个 a -> a，但你传递了一个有两个参数的函数 n，显然是类型错误。

问题在于 Church a 并没有正确地描述一个 Church 数字。一个 Church 数字仅仅表示一个数字——那么这个类型参数到底代表什么呢？例如：

foo :: Church Int
foo f x = f x `mod` 42

虽然这段代码的类型检查是通过的，但是foo绝对不是一个Church数。我们需要限制类型。Church数应该适用于任何a，而不仅仅是特定的a。正确的定义应该是：

type Church = forall a. (a -> a) -> (a -> a)

要使用这种类型，您需要在文件顶部添加{-# LANGUAGE RankNTypes #-}。

现在我们可以给出所期望的类型签名：

predChurch :: Church -> Church
-- same as before

由于Hindley-Milner无法推导出高阶类型，因此您必须在此处提供类型签名。

然而，在实现subChurch时，会遇到另一个问题：

Couldn't match expected type `Church'
       against inferred type `(a -> a) -> a -> a'

我不完全确定为什么会发生这种情况，我认为forall被类型检查器过于自由地展开了。但这并不让我感到惊讶；由于高阶类型给编译器带来的困难，它们可能有点脆弱。此外，我们不应该使用type来表示抽象，而应该使用newtype（这样可以更灵活地定义，帮助编译器进行类型检查，并标记我们使用抽象实现的位置）：

newtype Church = Church { unChurch :: forall a. (a -> a) -> (a -> a) }

我们需要修改predChurch以根据需要进行滚动和展开：

predChurch = \n -> Church $ 
    \f -> \x -> unChurch n (\g -> \h -> h (g f)) (\u -> x) (\u -> u)

与 subChurch 相同：

subChurch = \m -> \n -> unChurch n predChurch m

但是我们不再需要类型签名——在卷/展操作中有足够的信息可以再次推断类型。

当创建新的抽象时，我总是建议使用newtype。在我的代码中，常规的type同义词非常少见。

- luqui

---

关于“类型”错误，它发生在Haskell中的多态类型必须仅使用单态类型参数进行实例化的情况下：在“type Church = forall a. (a -> a) -> (a -> a)”类型变量a必须是单态的，但在subChurch定义中不是这种情况（在(n predChurch)中，类型变量a被设置为多态的Church）。这里有详细的解释：http://okmij.org/ftp/Haskell/types.html#some-impredicativity - Ed'ka

Answer 2

关于predChurch的定义，在简单类型的λ演算中不适用，只适用于无类型版本。你可以在这里找到一个在Haskell中使用的版本。

- Mikhail Glushenkov

---

谢谢，这就是我在寻找的答案。我只是想知道是否有一些魔法可以让Haskell不关心类型。我已经有一个在Haskell中工作的定义了，我只是想知道是否可以让未经过类型检查的版本在Haskell中工作。再次感谢。 - Probie

@Probie：请记住，第一个比特只涉及简单类型的λ演算，类似于没有多态类型、类型类、data和newtype以及递归绑定的Haskell。 - C. A. McCann

Answer 3

我遇到了同样的问题，但我解决它时没有添加类型签名。

这是解决方案，其中包含从 SICP 中复制的 cons 和 car。

cons x y = \m -> m x y
car z = z (\p q -> p)
cdr z = z (\p q -> q)

next z = cons (cdr z) (succ (cdr z))
pred n = car $ n next (cons undefined zero)

sub m n = n pred m

您可以在这里找到完整的源代码。

写下sub m n = n pred m后，我真的很惊讶，在ghci中加载它时没有类型错误！

Haskell代码非常简洁！ :-)

- wenlong

---

这并不真正起作用。如果你查看GHCi中推断出的类型，它们过于具体化，因此例如showChurch $ sub (plus three two) two会产生类型错误。 - hammar

@hammar 哎呀，你说得对。我只测试了 sub two one。sub three two 会出现类型错误。 - wenlong