我试图在 Haskell 中实现 Church 数字。这是我的代码:
-- Church numerals in Haskell.
type Numeral a = (a -> a) -> (a -> a)
churchSucc :: Numeral a -> Numeral a
churchSucc n f = \x -> f (n f x)
-- Operations with Church numerals.
sum :: Numeral a -> Numeral a -> Numeral a
sum m n = m . churchSucc n
mult :: Numeral a -> Numeral a -> Numeral a
mult n m = n . m
-- Here comes the first problem
-- exp :: Numeral a -> Numeral a -> Numeral a
exp n m = m n
-- Convenience function to "numerify" a Church numeral.
add1 :: Integer -> Integer
add1 = (1 +)
numerify :: Numeral Integer -> Integer
numerify n = n add1 0
-- Here comes the second problem
toNumeral :: Integer -> Numeral Integer
toNumeral 0 = zero
toNumeral (x + 1) = churchSucc (toNumeral x)
我的问题来自求幂。如果我声明 toNumeral
和 exp
的类型签名,则代码无法编译。但是,如果我评论类型签名声明,一切都会正常。 toNumeral
和 exp
的正确声明是什么?
最佳答案
原因exp
不能按照您的方式编写,它涉及传递 Numeral
作为 Numeral
的参数。这需要有一个 Numeral (a -> a)
,但你只有 Numeral a
。您可以将其写为
exp :: Numeral a -> Numeral (a -> a) -> Numeral a
exp n m = m n
我不明白 toNumeral
有什么问题,除了像 x + 1
这样的模式不应该使用。
toNumeral :: Integer -> Numeral a -- No need to restrict it to Integer
toNumeral 0 = \f v -> v
toNumeral x
| x > 0 = churchSucc $ toNumeral $ x - 1
| otherwise = error "negative argument"
还有,你的sum
被窃听了,因为 m . churchSucc n
是 m * (n + 1)
,所以应该是:
sum :: Numeral a -> Numeral a -> Numeral a
sum m n f x = m f $ n f x -- Repeat f, n times on x, and then m more times.
但是,教堂数字是适用于所有类型的函数。即Numeral String
不应与 Numeral Integer
不同,因为 Numeral
不应该关心它正在处理什么类型。这是一个通用量化:Numeral
是一个函数,适用于所有类型 a
, (a -> a) -> (a -> a)
,写为 RankNTypes
,如type Numeral = forall a. (a -> a) -> (a -> a)
.
这是有道理的:教会数字是通过其函数参数重复的次数来定义的。 \f v -> v
来电 f
0次,所以是0,\f v -> f v
是 1,等等。强制 Numeral
为所有人工作a
确保它只能做到这一点。但是,允许 Numeral
关心什么类型f
和v
has 删除了限制,并允许您编写 (\f v -> "nope") :: Numeral String
,尽管这显然不是 Numeral
.
我会把它写成
{-# LANGUAGE RankNTypes #-}
type Numeral = forall a. (a -> a) -> (a -> a)
_0 :: Numeral
_0 _ x = x
-- The numerals can be defined inductively, with base case 0 and inductive step churchSucc
-- Therefore, it helps to have a _0 constant lying around
churchSucc :: Numeral -> Numeral
churchSucc n f x = f (n f x) -- Cleaner without lambdas everywhere
sum :: Numeral -> Numeral -> Numeral
sum m n f x = m f $ n f x
mult :: Numeral -> Numeral -> Numeral
mult n m = n . m
exp :: Numeral -> Numeral -> Numeral
exp n m = m n
numerify :: Numeral -> Integer
numerify n = n (1 +) 0
toNumeral :: Integer -> Numeral
toNumeral 0 = _0
toNumeral x
| x > 0 = churchSucc $ toNumeral $ x - 1
| otherwise = error "negative argument"
相反,它看起来干净得多,并且比原来的更不可能遇到障碍。
演示:
main = do out "5:" _5
out "2:" _2
out "0:" _0
out "5^0:" $ exp _5 _0
out "5 + 2:" $ sum _5 _2
out "5 * 2:" $ mult _5 _2
out "5^2:" $ exp _5 _2
out "2^5:" $ exp _2 _5
out "(0^2)^5:" $ exp (exp _0 _2) _5
where _2 = toNumeral 2
_5 = toNumeral 5
out :: String -> Numeral -> IO () -- Needed to coax the inferencer
out str n = putStrLn $ str ++ "\t" ++ (show $ numerify n)
关于haskell - 一些带有 Church 数字的操作的类型签名声明,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/45824350/