类型仅在haskell中的函数内匹配

Question

我是 haskell 的初学者，正在尝试实现自然数的 Church 编码，如 this guide 中所述。

{-# LANGUAGE RankNTypes #-}

newtype Chur = Chr (forall a. (a -> a) -> (a -> a))

zero :: Chur
zero = Chr (\x y -> y)

-- church to int
c2i :: Chur -> Integer
c2i (Chr cn) = cn (+ 1) 0

-- this works
i1 = c2i zero
-- this doesn't
i2 = zero (+ 1) 0

对于i2，我得到一个类型不匹配：

Couldn't match expected type ‘(Integer -> Integer) -> Integer -> t’
            with actual type ‘Chur’
Relevant bindings include i2 :: t (bound at test.hs:14:1)
The function ‘zero’ is applied to two arguments,
but its type ‘Chur’ has none
In the expression: zero (+ 1) 0
In an equation for ‘i2’: i2 = zero (+ 1) 0

为什么Chur 可以在封装在函数中时接受参数，但不能没有它？

Answer 1

Chur 包裹在函数中时不接受任何参数 - 包裹在 Chur 中的函数会：

c2i (Chr cn) = cn (+ 1) 0

这里，cn 是包裹在 Chur 中的函数。

您可以使用替换方法来查看发生了什么：

    c2i zero
==> c2i (Chr (\x y -> y))
==> (\x y -> y) (+ 1) 0
==> 0

但是

    zero (+ 1) 0
==> (Chr (\x y -> y)) (+ 1) 0

这不起作用，因为(Chr (\x y -> y)) 不是函数。

如果你写了

c2i :: Chur -> Integer
c2i cn = cn (+ 1) 0

您会看到类似的错误。