将整数表示为函数(教会数字？)

Question

给定以下函数定义并假设所有正整数的类似定义给出了一个名为plus的函数的类型定义和代码,它将把两个这样的函数作为参数表示整数并返回一个表示两个输入整数之和的函数.例如,(plus one two)应该评估一个带有两个参数f x并返回的函数(f(f(f x))).

one f x = f x
two f x = f (f x)
three f x = f (f (f x)))

等等

我是函数式编程的新手,我无法理解这一点.我首先不知道如何定义所有正整数的函数而不将它们写出来(这显然是不可能的).如果我有plus(sixty, forty),我的功能怎么能识别六十次被应用60次x？

我打算在米兰达写这篇文章,但我对Haskell更熟悉,所以欢迎任何一方的帮助.

Answer 1

应用等式推理¹和抽象.你有

one   f x = f  x                            -- :: (a -> b) -> a -> b
two   f x = f (f  x)     -- = f (one f x)   -- :: (a -> a) -> a -> a
three f x = f (f (f x))  -- = f (two f x)   -- :: (a -> a) -> a -> a

因此,后继函数next是自然定义的,因此three = next two.是的,它就像写作next two而不是three上面的等式一样简单:

next :: ((b -> c) -> a -> b) -> (b -> c) -> a -> c
-- three f x = next two f x = f (two f x)   -- `two` is a formal parameter
next                num f x = f (num f x)   -- generic name `num`

zero :: t -> a -> a
zero f x = x

这抓住了继承的模式.f将用作后继函数,并x作为零值.其余的如下.例如,

plus :: (t -> b -> c) -> (t -> a -> b) -> t -> a -> c
plus two one f x = two f (one f x)   -- formal parameters two, one
              -- = f (f (one f x))   -- an example substitution
              -- = f (f (f x)        --   uses the global definitions
              -- = three f x         --   for one, two, three

ie one f x将被用作零值two(而不是"通常" x),从而表示three."数字" n表示n次 +1操作的连续.

以上,再次,实际上定义一般plus是因为运营two和one只是两个正式的功能参数:

Prelude> plus three two succ 0    -- built-in `succ :: Enum a => a -> a`
5
Prelude> :t plus three two
plus three two :: (a -> a) -> a -> a
Prelude> plus three two (1:) [0]
[1,1,1,1,1,0]

这里要说的关键是函数是一个在调用时会产生值的对象.它本身就是一个不透明的物体.我们应用于它的"观察者"参数,为它意味着为零提供"意义",或者找到一个继承者,从而定义当我们观察数字值时产生的结果.

¹ 即在任何表达式中的LHS与定义的RHS,或与LHS的RHS自由更换,你认为合适的(直到变量重命名当然,无法捕捉/阴影现有自由变量).

Answer 2

要将数字转换为数字，您可以使用以下内容：

type Numeral = forall a . (a -> a) -> (a -> a)

toChurch :: Int -> Numeral
toChurch 0 _ x = x
toChurch n f x = f $ toChurch (pred n) f x

fromChurch :: Numeral -> Int
fromChurch numeral = numeral succ 0