haskell - 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

问题是 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肯定不是教会数字。我们需要限制类型。教会数字需要为任何 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 (这给了我们更多的定义灵 active ，帮助编译器进行类型检查，并标记我们使用抽象实现的地方):

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同义词在我的代码中很少见。