Type signature declaration of some operations with Church numerals

Question

I was trying to implement Church numerals in Haskell. This is my code:

-- Church numerals in Haskell.
type Numeral a = (a -> a) -> (a -> a)

churchSucc :: Numeral a -> Numeral a
churchSucc n f = \x -> f (n f x)

-- Operations with Church numerals.
sum :: Numeral a -> Numeral a -> Numeral a
sum m n = m . churchSucc n

mult :: Numeral a -> Numeral a -> Numeral a
mult n m = n . m

-- Here comes the first problem
-- exp :: Numeral a -> Numeral a -> Numeral a
exp n m = m n

-- Convenience function to "numerify" a Church numeral.
add1 :: Integer -> Integer
add1 = (1 +)

numerify :: Numeral Integer -> Integer
numerify n = n add1 0

-- Here comes the second problem
toNumeral :: Integer -> Numeral Integer
toNumeral 0 = zero
toNumeral (x + 1) = churchSucc (toNumeral x)

My problem comes from exponentiation. If I declare the type signature of toNumeral and exp, the code doesn't compile. However, if I comment the type signature declarations, everything works fine. What would be the correct declarations for toNumeral and exp?

Answer 1

The reason exp cannot be written the way you have it is that it involves passing a Numeral as argument to a Numeral. This requires having a Numeral (a -> a), but you only have a Numeral a. You can write it as

exp :: Numeral a -> Numeral (a -> a) -> Numeral a
exp n m = m n

I don't see what's wrong with toNumeral, aside from the fact that patterns like x + 1 should not be used.

toNumeral :: Integer -> Numeral a -- No need to restrict it to Integer
toNumeral 0 = \f v -> v
toNumeral x
  | x > 0 = churchSucc $ toNumeral $ x - 1
  | otherwise = error "negative argument"

Also, your sum is bugged, because m . churchSucc n is m * (n + 1), so it should be:

sum :: Numeral a -> Numeral a -> Numeral a
sum m n f x = m f $ n f x -- Repeat f, n times on x, and then m more times.

However, church numerals are functions that work on all types. That is, Numeral String should not be different from Numeral Integer, because a Numeral shouldn't care what type it's working on. This is a universal quantification: Numeral is a function, for all types a, (a -> a) -> (a -> a), which is written, with RankNTypes, as type Numeral = forall a. (a -> a) -> (a -> a).

This makes sense: a church numeral is defined by how many times its function argument is repeated. \f v -> v calls f 0 times, so it is 0, \f v -> f v is 1, etc. Forcing a Numeral to work for all a makes sure that it can only do that. However, allowing a Numeral to care what type f and v have removes the restriction, and lets you write (\f v -> "nope") :: Numeral String, even though that clearly isn't a Numeral.

I would write this as

{-# LANGUAGE RankNTypes #-}

type Numeral = forall a. (a -> a) -> (a -> a)

_0 :: Numeral
_0 _ x = x
-- The numerals can be defined inductively, with base case 0 and inductive step churchSucc
-- Therefore, it helps to have a _0 constant lying around

churchSucc :: Numeral -> Numeral
churchSucc n f x = f (n f x) -- Cleaner without lambdas everywhere

sum :: Numeral -> Numeral -> Numeral
sum m n f x = m f $ n f x

mult :: Numeral -> Numeral -> Numeral
mult n m = n . m

exp :: Numeral -> Numeral -> Numeral
exp n m = m n

numerify :: Numeral -> Integer
numerify n = n (1 +) 0

toNumeral :: Integer -> Numeral
toNumeral 0 = _0
toNumeral x
  | x > 0 = churchSucc $ toNumeral $ x - 1
  | otherwise = error "negative argument"

instead, which looks so much cleaner, and is less likely to run into roadblocks than the original.

Demo:

main = do out "5:" _5
          out "2:" _2
          out "0:" _0
          out "5^0:" $ exp _5 _0
          out "5 + 2:" $ sum _5 _2
          out "5 * 2:" $ mult _5 _2
          out "5^2:" $ exp _5 _2
          out "2^5:" $ exp _2 _5
          out "(0^2)^5:" $ exp (exp _0 _2) _5
       where _2 = toNumeral 2
             _5 = toNumeral 5
             out :: String -> Numeral -> IO () -- Needed to coax the inferencer
             out str n = putStrLn $ str ++ "\t" ++ (show $ numerify n)