haskell - Haskell 中的 Lambda 演算 : Is there some way to make Church numerals type check?

Question

我正在用 Haskell 玩一些 lambda 演算的东西，特别是教堂数字。我定义了以下内容:

let zero = (\f z -> z)
let one = (\f z -> f z)
let two = (\f z -> f (f z))
let iszero = (\n -> n (\x -> (\x y -> y)) (\x y -> x))
let mult = (\m n -> (\s z -> m (\x -> n s x) z))

这有效:

:t (\n -> (iszero n) one (mult one one))

由于发生检查而失败:

:t (\n -> (iszero n) one (mult n one))

我已经用我的常量使用了 iszero 和 mult ，它们似乎是正确的。有什么方法可以让这个可以打字吗？我不认为我所做的事情太疯狂，但也许我做错了什么？

Answer 1

从顶层来看，您的定义及其类型都是正确的。问题是，在第二个示例中，您以两种不具有相同类型的不同方式使用 n ——或者更确切地说，它们的类型无法统一，并且试图这样做会产生无限类型。 one 的类似用法可以正常工作，因为每种用法都独立地专门针对不同的类型。

为了以简单的方式完成这项工作，您需要更高级别的多态性。教堂数字的正确类型是 (forall a. (a -> a) -> a -> a)，但无法推断更高级别的类型，并且需要 GHC 扩展，例如作为RankNTypes。如果您启用适当的扩展(我认为在这种情况下您只需要rank-2)并为您的定义提供显式类型，那么它们应该可以在不改变实际实现的情况下工作。

请注意，使用更高级别的多态类型存在(或至少存在)一些限制。但是，您可以将教堂数字包装为 newtype ChurchNum = ChurchNum (forall a.(a -> a) -> a -> a)，这将允许给它们一个 Num 实例也是如此。