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.

Billiton

You need higher ranked types to give sensible types to Church encoded naturals in Haskell. – Aguedaaguero

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

Whisky

Alternatively, church n = foldr (.) id . replicate n – Reggi

I just consulted the book again and found that the numerical scheme used in this book was invented by Henk Barendregt, which is similar to but different from Church's. In this scheme the successor combinator is defined as V(KI), where Vxyz = zxy, Kxy = x, and Ix = x. So although unchurch does what I'm trying to do with cnhn for Church arithmetic, I'd like to know if there's a function that does it for Barendregt arithmetic. – Billiton

I see you are right about parametric polymorphism though. Obviously Haskell allows such things, since there are many functions that take multiple types of arguments, e.g. id. So the problem with cnhn must be something else. – Billiton

There is no such thing at the Barendregt arithmetic. The scheme you're describing is the precisely the church arithmetic, just with the arguments to the combinators rearranged. – Whisky

I guess I used the wrong word here. It's not a different arithmetic, it's just a different numerical scheme for the same arithmetic. What I wanted to say was that, given this different numerical scheme which takes V(KI) as the successor, it seems that cnhn should do the same thing as unchurch, but it gives an error. So I'm trying to figure out what's wrong with it. – Billiton