20

我正在尝试在 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
4

3 回答 3

30

问题是它predChurch太多态，无法通过 Hindley-Milner 类型推断正确推断。例如，很想写：

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

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

问题在于Church a它不能正确地表征一个 Church 数字。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器过于自由地展开。不过，这并不让我感到惊讶；较高等级的类型可能有点脆弱，因为它们给编译器带来了困难。此外，我们不应该将 atype用于抽象，我们应该使用 a 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 中有足够的信息来再次推断类型。

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

于 2011-07-06T12:55:02.640 回答
7

此定义predChurch 不适用于简单类型的 lambda 演算，仅适用于无类型版本。你可以在这里predChurch找到在 Haskell 中工作的版本。

于 2011-07-06T12:38:00.517 回答
-1

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

这是从SICPcons 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 代码非常简洁！:-)

于 2012-04-20T15:05:22.253 回答