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
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
Here is another example using 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
Testing the operation add
, mult
and exp
(using 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
Testing the operation add
, mult
and exp
(using s=('|':)
and z=""
):
Main> add two three ('|':) ""
"|||||" --5 sticks
Main> mult four three ('|':) ""
"||||||||||||" --12 sticks
Main> exp two three ('|':) ""
"||||||||" --8 sticks
Or exp four two
(4^2 = 16) which is written as:
Main> two four (+1) 0
16
It works fine!
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.
which works for any type
a
, i.e. it really meansThe 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):
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:...or, as I'd prefer to write it,
Quick test:
Now with these types, you can also implement the exponentiation directly:
And it works as expected: