我目前正在学习 Church 编码，并且正在尝试实现
mulmul cn cm = \f x -> cn (cm f) x这（我的实现）不起作用，它给出了类型错误
mul cn cm = cn (add cm) zero为什么会这样？
描述的错误
mul cn cm = cn (add cm) zeroghci> unchurch (mul (church 3) (church 4))
<interactive>:2:16: error:
* Couldn't match type `t2' with `(t2 -> t2) -> t3 -> t2'
Expected: (((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((t2 -> t2) -> t3 -> t2)
-> (t2 -> t2)
-> t3
-> t2)
-> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((t2 -> t2) -> t3 -> t2)
-> (t2 -> t2)
-> t3
-> t2)
-> ((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((t2 -> t2) -> t3 -> t2)
-> (t2 -> t2)
-> t3
-> t2)
-> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((t2 -> t2) -> t3 -> t2)
-> (t2 -> t2)
-> t3
-> t2
Actual: (((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((t2 -> t2) -> t3 -> t2)
-> (t2 -> t2)
-> t3
-> t2)
-> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((t2 -> t2) -> t3 -> t2)
-> (t2 -> t2)
-> t3
-> t2)
-> ((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((t2 -> t2) -> t3 -> t2)
-> (t2 -> t2)
-> t3
-> t2)
-> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((t2 -> t2) -> t3 -> t2)
-> (t2 -> t2)
-> t3
-> t2
`t2' is a rigid type variable bound by
the inferred type of
it :: (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2
at <interactive>:2:1-36
* In the first argument of `mul', namely `(church 3)'
In the first argument of `unchurch', namely
`(mul (church 3) (church 4))'
In the expression: unchurch (mul (church 3) (church 4))
* Relevant bindings include
it :: (((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2)
-> ((t2 -> t2) -> t3 -> t2) -> (t2 -> t2) -> t3 -> t2
(bound at <interactive>:2:1)
完整代码
module Church where
import Prelude hiding (not, and, or, fst, snd, add, iszero, zero, one, two, three, mul, exp)
-- | Church Booleans
--
-- You will see that the above macros for true, false and iff are behaving as expected.
-- For example, one may verify that iff true M N is equivalent to M, and iff false M N is equivalent to N.
--
-- >>> iff true "M" "N"
-- "M"
--
-- >>> iff false "M" "N"
-- "N"
--
-- Boolean arithmetic is also encodable in this way. For example,
-- Boolean negation is essentially flipping the two “branches’ ’:
--
-- >>> iff (not true) "M" "N"
-- "N"
true t f = t
false = \t f -> f
iff = \b t f -> b t f
not b = \t f -> b f t
-- | Church Booleans - Test
--
-- >>> iff (and true false) "get true" "get false"
-- "get false"
--
-- >>> iff (and true true) "get true" "get false"
-- "get true"
--
-- >>> iff (and false true) "get true" "get false"
-- "get false"
--
-- >>> iff (and false false) "get true" "get false"
-- "get false"
--
-- >>> iff (or true false) "get true" "get false"
-- "get true"
--
-- >>> iff (or true true) "get true" "get false"
-- "get true"
--
-- >>> iff (or false true) "get true" "get false"
-- "get true"
--
-- >>> iff (or false false) "get true" "get false"
-- "get false"
--
-- >>> iff (not (or true false)) "get true" "get false"
-- "get false"
and b1 b2 = \t f -> if (b1 t f, b2 t f) == (t, t) then t else f
or b1 b2 = \t f -> if (b1 t f, b2 t f) == (f, f) then f else t
-- |- Church Pairs
--
-- For pairs, we need three operations mkpair, fst, and snd that obey the following behavior:
--
-- >>> fst (mkpair "M" "N")
-- "M"
--
-- >>> snd (mkpair "M" "N")
-- "N"
mkpair x y = \s -> iff s x y
fst p = p true
snd p = p false
-- |- Church Triples
--
-- >>> fst3 (mktriple "M" "N" "P")
-- "M"
--
-- >>> snd3 (mktriple "M" "N" "P")
-- "N"
--
-- >>> thd3 (mktriple "M" "N" "P")
-- "P"
mktriple x y z = \ b1 b2 -> iff b1 (b2 y z) x
fst3 p = p false true
snd3 p = p true true
thd3 p = p true false
-- | Church Numbers
--
-- >>> unchurch (add1 zero)
-- 1
--
-- >>> unchurch (add (church 23) (church 17))
-- 40
--
-- >>> iff (iszero (church 0)) "zero is zero" "zero is not zero"
-- "zero is zero"
church 0 = \f x -> x
church n = \f x -> f (church (n-1) f x)
unchurch cn = cn (+ 1) 0
zero = \f x -> x
one = \f x -> f x
two = \f x -> f (f x)
three = \f x -> f (f (f x))
add1 cn = \f x -> f (cn f x)
add cn cm = cm add1 cn
iszero cn = cn (\x -> false) true
-- | Church Numbers - Multiplications and Exponentiations
--
-- >>> unchurch (mul (church 3) (church 4))
-- 12
--
-- >>> unchurch (exp (church 2) (church 3))
-- 8
-- Dk why this doesn't work!!!!!!!!
--mul cn cm = cn (add cm) zero
mul cn cm = \f x -> cn (cm f) x
exp cn cm = cm (mul cn) one
我还发现下面的代码有效
test cn = cn (add1) zero但是这个不起作用。当我尝试输入两个或三个时，这个不起作用，但由于某种原因可以使用零和一
test2 cn = cn (add one) zero这违背了我对柯里化在 Haskell 中如何工作的理解。 ‘add1’和‘add one’不应该是一样的吗？
您使用的类型对于 Haskell 来说太复杂，无法推断，并且还需要 GHC 9.2 或更高版本以及 GHC 扩展。假设您使用的是足够新的 GHC 版本，则要使
mul{-# LANGUAGE ImpredicativeTypes #-}type ChurchNum = forall a. (a -> a) -> a -> aaddmulexpChurchNum -> ChurchNum -> ChurchNum我强烈建议您为其余的定义编写类似的类型。