仅在haskell中的函数内键入匹配项

Question

我是haskell的初学者,并试图实现自然数字的Church编码,如本指南中所述.

{-# 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

你会看到类似的错误.