我正在用 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
,它们似乎是正确的。有什么方法可以让这个可以打字吗?我不认为我所做的事情太疯狂,但也许我做错了什么?
最佳答案
从顶层来看,您的定义及其类型都是正确的。问题是,在第二个示例中,您以两种不具有相同类型的不同方式使用 n
——或者更确切地说,它们的类型无法统一,并且试图这样做会产生无限类型。 one
的类似用法可以正常工作,因为每种用法都独立地专门针对不同的类型。
为了以简单的方式完成这项工作,您需要更高级别的多态性。教堂数字的正确类型是 (forall a. (a -> a) -> a -> a)
,但无法推断更高级别的类型,并且需要 GHC 扩展,例如作为RankNTypes
。如果您启用适当的扩展(我认为在这种情况下您只需要rank-2)并为您的定义提供显式类型,那么它们应该可以在不改变实际实现的情况下工作。
请注意,使用更高级别的多态类型存在(或至少存在)一些限制。但是,您可以将教堂数字包装为 newtype ChurchNum = ChurchNum (forall a.(a -> a) -> a -> a)
,这将允许给它们一个 Num
实例也是如此。
关于haskell - Haskell 中的 Lambda 演算 : Is there some way to make Church numerals type check?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/12942397/