Haskell中教堂数字的减法

Question

我正在尝试在 Haskell 中实现教堂数字，但遇到了一个小问题。 Haskell 通过 Occurs 检查抱怨无限类型

：无法构造无限类型：t = (t -> t1) -> (t1→t2)→ t2

当我尝试做减法时。我 99% 确信我的 lambda 演算是有效的（如果不是，请告诉我）。我想知道的是，我是否可以做些什么来让 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

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 数字。我们需要限制类型。教堂数字需要适用于任何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'

我不是 100% 确定为什么会发生这种情况，我认为 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 同义词在我的代码中非常罕见。

Answer 2

predChurch 的这个定义在简单类型的 lambda 中不起作用微积分，仅在非类型化版本中。您可以找到适用于 Haskell 的 predChurch 版本在这里。

Answer 3

我也遇到过同样的问题。我在没有添加类型签名的情况下解决了这个问题。

这是解决方案，其中 cons car 复制自 SICP。

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 mn = n pred m 后，我真的很惊讶，并将其加载到 ghci 中，没有类型错误！

Haskell 代码是如此简洁！ :-)