Haskell中教堂数字的减法

Question

我正在尝试在 Haskell 中实现教堂数字，但遇到了一个小问题。 Haskell 用

抱怨无限类型

发生检查：无法构造无限类型：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

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

这是解决方案，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

您可以找到完整的源代码here。

写完sub m n = n pred m真的很惊喜，在ghci中加载没有类型错误！

Haskell 代码如此简洁！ :-)

Answer 2

问题在于 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 数字仅代表一个数字——该类型参数到底意味着什么？例如：

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

那是类型检查，但foo 肯定不是教会数字。我们需要限制类型。教会数字需要适用于任何 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

但我们不再需要类型签名——roll/unroll 中有足够的信息来再次推断类型。

在创建新的抽象时，我总是推荐newtypes。常规的type 同义词在我的代码中非常少见。

Answer 3

predChurchdoesn't work in simply typed lambda calculus的这个定义，只在无类型版本中。你可以找到在 Haskell here 中工作的 predChurch 版本。