Seems like the successor combinator isn't quite correct. Here's a encoding of the Church arithmetic in Haskell, the unchurch
function is what the cnhn
( Church Number to Haskell Number, I presume? ) is attempting to implement.
tr :: a -> b -> a
tr x y = x
fl :: a -> b -> b
fl x y = y
succ :: ((a -> b) -> c -> a) -> (a -> b) -> c -> b
succ n f x = f (n f x)
unbool :: (Bool -> Bool -> t) -> t
unbool n = n True False
unchurch :: ((Int -> Int) -> Int -> a) -> a
unchurch n = n (\i -> i + 1) 0
church :: Int -> (a -> a) -> a ->a
church n =
if n == 0
then zero
else \f x -> f (church (n-1) f x)
zero :: a -> b -> b
zero = fl
one :: (a -> a) -> a -> a
one = succ zero
two :: (a -> a) -> a -> a
two = succ one
ten :: (a -> a) -> a -> a
ten = succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))
main = do
print (unchurch ten)
print (unchurch (church 42))
So a function that takes any combinatory number as an argument must be able to take infinitely many types of arguments. But Haskell doesn't allow such functions.
Ahh, but it does since Haskell allows parametric polymorphism. If you look at the encoding of the numbers they all have signature ( (a -> a) -> a -> a
) so the argument to a function taking a church number need only have it's first argument unify the type variables of it's first argument with the function that encodes the church number.
For example we can also define a multiplication operation which is really just a higher order function, which takes two church numbers and multiplies them. This works for any two church numbers.
mult :: (a -> b) -> (c -> a) -> c -> b
mult m n f = m (n f)
test :: (a -> a) -> a -> a
test = mult ten ten
main = print (unchurch test) -- 100