17

我在 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它们似乎是正确的。有什么方法可以使这个可打字吗？我不认为我在做什么太疯狂了，但也许我做错了什么？

4

2 回答 2

20

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

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

请注意，使用更高级别的多态类型存在（或至少存在）一些限制。但是，您可以将教堂数字包裹在类似的东西中newtype ChurchNum = ChurchNum (forall a. (a -> a) -> a -> a)，这样也可以给它们一个Num实例。

于 2012-10-17T20:15:45.960 回答
5

让我们添加一些类型签名：

type Nat a = (a -> a) -> a -> a

zero :: Nat a
zero = (\f z -> z)

one :: Nat a
one = (\f z -> f z)

two :: Nat a
two = (\f z -> f (f z))

iszero :: Nat (a -> a -> a) -> a -> a -> a
iszero = (\n -> n (\x -> (\x y -> y)) (\x y -> x))

mult :: Nat a -> Nat a -> Nat a
mult = (\m n -> (\s z -> m (\x -> n s x) z))

如您所见，除了iszero.

让我们看看你的表达会发生什么：

*Main> :t (\n -> (iszero n) one n)
<interactive>:1:23:
    Occurs check: cannot construct the infinite type:
      a0
      =
      ((a0 -> a0) -> a0 -> a0)
      -> ((a0 -> a0) -> a0 -> a0) -> (a0 -> a0) -> a0 -> a0
    Expected type: Nat a0
      Actual type: Nat (Nat a0 -> Nat a0 -> Nat a0)
    In the third argument of `iszero', namely `(mult n one)'
    In the expression: (iszero n) one (mult n one)

看看错误如何使用我们的Nat别名！

我们实际上可以使用更简单的表达式得到类似的错误\n -> (iszero n) one n。这就是问题所在。既然我们在打电话iszero n，我们就必须有n :: Nat (b -> b -> b)。此外，由于iszeros 类型，第二个和第三个参数，n并且one，必须具有类型b。现在我们有两个关于 类型的方程n：

n :: Nat (b -> b -> b)
n :: b

这是不可调和的。真可惜。

于 2012-10-17T20:26:34.147 回答