haskell - 幂函数 Haskell

Question

如何使用 Haskell 获得教堂数字中的幂函数？

我正在尝试应用规则，即 λxy.yx 但有些东西不能正常工作。

exponentiation :: (Num a) => Func a
exponentiation x y = y x

Answer 1

Church 数字算术往往涉及相当奇怪的类型，因此在 Haskell 中它不像在无类型语言中那样优雅。原则上，教会数字是一个函数，它接受任何自同态并在同一类型上给出另一个自同态，即

five :: (a -> a) -> a -> a

它适用于任何类型a，即它确实意味着

{-# LANGUAGE ExplicitForall, UnicodeSyntax #-}
five :: ∀ a . (a -> a) -> a -> a

当您对这些数字进行有趣的算术运算时，诀窍是计算的各个组件实际上可能正在处理不同类型的自同态，包括本身是高阶函数的自同态。跟踪这一切变得相当棘手。

因此，在 Haskell 中玩弄 Church 算术最不痛苦的方法是将所有多态性包装成一个自然数类型（其实现恰好是 Church 编码）：

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}
newtype Nat = Nat {getChurchNum :: ∀ a . (a -> a) -> a -> a}

然后你可以给所有的基本操作清晰的类型签名，只是你总是需要把与数字对应的术语放在Nat包装器中，以隐藏多态性：

zero :: Nat
zero = Nat (\f x -> x)

suc :: Nat -> Nat
suc = \(Nat n) -> Nat (\f x -> n f (f x))

...或者，正如我更愿意写的那样，

instance Enum Nat where
  succ (Nat n) = Nat (\f -> n f . f)

instance Num Nat where
  fromInteger 0 = Nat (const id)
  fromInteger n = succ . fromInteger $ n-1
  Nat a + Nat b = Nat (\f -> a f . b f)
  Nat a * Nat b = Nat (a . b)

instance Show Nat where
  show (Nat n) = show (n (+1) 0 :: Int)

快速测试：

GHCi> [0, 1, 2, 4, 8, 3+4, 3*4 :: Nat]
[0,1,2,4,8,7,12]

现在使用这些类型，您还可以直接实现求幂：

pow :: Nat -> Nat -> Nat
pow (Nat n) (Nat m) = Nat (m n)

它按预期工作：

GHCi> [pow a b :: Nat | a<-[0,1,2,3], b<-[0,1,2,3]]
[1,0,0,0,1,1,1,1,1,2,4,8,1,3,9,27]

Answer 2

这是另一个使用WinHugs的示例：

type Church a = (a -> a) -> a -> a

zero :: Church a
zero = \s z -> z

one :: Church a
one = \s z -> s z

two :: Church a
two = \s z -> s (s z)

three :: Church a
three = \s z -> s (s (s z))

four :: Church a
four = \s z -> s (s (s (s z)))

succ :: Church a -> Church a
succ n f = f . n f

add :: Church a -> Church a -> Church a
add x y = \s z -> x s (y s z)

mult :: Church a -> Church a -> Church a
mult x y = x.y

exp :: Church a -> (Church a -> Church a) -> Church a
exp x y = y x

测试操作add, multand exp（使用s=(+1)and z=0）：

Main> add two three (+1) 0
5
Main> mult four three (+1) 0
12
Main> exp two three (+1) 0
8

测试操作add, multand exp（使用s=('|':)and z=""）：

Main> add two three ('|':) ""
"|||||" --5 sticks
Main> mult four three ('|':) ""
"||||||||||||" --12 sticks
Main> exp two three ('|':) ""
"||||||||" --8 sticks

或者exp four two(4^2 = 16) 写成：

Main> two four (+1) 0
16

它工作正常！