Haskell中的Lambda演算:有没有办法让教堂数字类型检查？

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.如果您启用了适当的扩展(在这种情况下,您只需要排名-2,我认为)并为您的定义提供显式类型,它们应该在不改变实际实现的情况下工作.

请注意,对于更高级别的多态类型的使用存在(或至少是)某些限制.但是,您可以将教堂数字包装成类似的东西newtype ChurchNum = ChurchNum (forall a. (a -> a) -> a -> a),这也可以为它们提供一个Num实例.

Answer 2

让我们添加一些类型的签名:

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

哪个不甘心.游民.