How to get the exponentiation function in church numerals using Haskell?
I'm trying to apply the rule, which is λxy.yx but something doesn't work right.
exponentiation :: (Num a) => Func a
exponentiation x y = y x
Church numeral arithmetic tends to involve rather strange types, so it's not quite as elegant in Haskell as in an untyped language. In principle, a church numeral is a function that takes any endomorphism and gives another endomorphism on the same type, i.e.
five :: (a -> a) -> a -> a
which works for any type a, i.e. it really means
{-# LANGUAGE ExplicitForall, UnicodeSyntax #-}
five :: ∀ a . (a -> a) -> a -> a
The trick when you're doing interesting arithmetic with such numbers is that the individual components of a calculation may actually be dealing with different-typed endomorphisms, including endomorphisms that are themselves higher-order functions. It gets quite tricky to keep track of all this.
Hence the least painful way to toy around with Church arithmetic in Haskell is to wrap all the polymorphism into a single type for natural numbers (whose implementation happens to be Church-encoding):
{-# LANGUAGE RankNTypes, UnicodeSyntax #-}
newtype Nat = Nat {getChurchNum :: ∀ a . (a -> a) -> a -> a}
Then you can give all the fundamental operations clear type signatures, just you always need to put the terms which correspond to numbers in the Nat wrapper, to hide the polymorphism:
zero :: Nat
zero = Nat (\f x -> x)
suc :: Nat -> Nat
suc = \(Nat n) -> Nat (\f x -> n f (f x))
...or, as I'd prefer to write it,
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)
Quick test:
GHCi> [0, 1, 2, 4, 8, 3+4, 3*4 :: Nat]
[0,1,2,4,8,7,12]
Now with these types, you can also implement the exponentiation directly:
pow :: Nat -> Nat -> Nat
pow (Nat n) (Nat m) = Nat (m n)
And it works as expected:
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]