Implementing Smullyan's arithmetical birds in Haskell

Question

While searching for information on Raymond Smullyan's To Mock a Mockingbird, I stumbled upon Stephen Tetley's Haskell code for the basic combinators. I thought it was an interesting idea and decided to implement the "birds that can do arithmetic" from chapter 24 of To Mock a Mockingbird using these combinators. I got as far as defining truth, falsity, successor, predecessor, and zero-check combinators, plus functions for changing combinatory booleans into Haskell booleans and vice versa. But when I try to make a function that takes a combinatory number and returns an integer, I keep running into problems. I'd like to know how to make this function work. Here's what I've got so far:

-- | The first 7 combinators below are from Stephen Tetley's Data.Aviary.Birds
-- | (http://hackage.haskell.org/package/data-aviary-0.2.3/docs/Data-Aviary-Birds.html),
-- | with minor modifications.


-- | S combinator - starling. 
-- Haskell: Applicative\'s @(\<*\>)@ on functions.
-- Not interdefined.
st :: (a -> b -> c) -> (a -> b) -> a -> c
st f g x = f x (g x)

-- | K combinator - kestrel - Haskell 'const'.
-- Corresponds to the encoding of @true@ in the lambda calculus.
-- Not interdefined.
ke :: a -> b -> a
ke a _b = a 

-- | I combinator - identity bird / idiot bird - Haskell 'id'.
id' :: a -> a 
id' = st ke ke 

-- | B combinator - bluebird - Haskell ('.').
bl :: (b -> c) -> (a -> b) -> a -> c
bl = st (ke st) ke

-- | C combinator - cardinal - Haskell 'flip'.
ca :: (a -> b -> c) -> b -> a -> c
ca = st(st(ke st)(st(ke ke)st))(ke ke)

-- | T combinator - thrush.
-- Haskell @(\#)@ in Peter Thiemann\'s Wash, reverse application.
th :: a -> (a -> b) -> b
th = ca id'

-- | V combinator - vireo.
vr :: a -> b -> (a -> b -> d) -> d
vr = bl ca th




-- | The code I added begins here. 




-- | Truth combinator. Functionally superfluous since it can  
-- | be replaced with the kestrel. Added for legibility only.
tr :: a -> b -> a
tr = ke

-- | Falsity combinator.
fs :: a -> b -> b
fs = ke id'

-- | Successor combinator.
sc :: a -> ((b -> c -> c) -> a -> d) -> d
sc = vr fs 

-- | Predecessor combinator.
pd :: ((((a -> a) -> b) -> b) -> c) -> c
pd = th (th id')

-- | Zerocheck combinator.
zc :: ((a -> b -> a) -> c) -> c
zc = th ke



-- | Below are 2 functions for changing combinatory booleans 
-- | to Haskell booleans and vice versa. They work fine as 
-- | far as I can tell, but I'm not very confident about 
-- | their type declarations. I just took the types 
-- | automatically inferred by Haskell.

-- | Combinatory boolean to Haskell boolean.
cbhb :: (Bool -> Bool -> Bool) -> Bool
cbhb cb  = cb True False

-- | Haskell boolean to combinatory boolean.
hbcb :: Bool -> a -> a -> a
hbcb hb | hb     = tr
        | not hb = fs




-- | Combinatory number to Haskell number. 
-- | This is the problematic function that I'd like to implement. 
-- | I think the function is logically correct, but I have no clue
-- | what its type would be. When I try to load it in Hugs it 
-- | gives me a "unification would give infinite type" error. 
cnhn cn | cbhb (zc cn) = 0
        | otherwise    = 1 + cnhn (pd cn)

Here's my very rough guess about what's wrong with the code: the 'cnhn' function takes any combinatory number as an argument. But different combinatory numbers have different types, such as

zero) id' :: a -> a

one) vr(ke id')id' :: ((a -> b -> b) -> (c -> c) -> d) -> d

two) vr(ke id')(vr(ke id')id') :: ((a -> b -> b) -> (((c -> d -> d) -> (e -> e) -> f) -> f) -> g) -> g

and so on. 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.

To make it brief, here are my 3 main questions:

1) What's wrong with the 'cnhn' function? (Is my guess above correct?)

2) Can it be fixed?

3) If not, what other language can I use to implement Smullyan's arithmetical birds?

Thanks for reading a long question.

Answer 1

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