Subtraction of church numerals in haskell

Question

I'm attempting to implement church numerals in Haskell, but I've hit a minor problem. Haskell complains of an infinite type with

Occurs check: cannot construct the infinite type: t = (t -> t1) -> (t1 -> t2) -> t2

when I try and do subtraction. I'm 99% positive that my lambda calculus is valid (although if it isn't, please tell me). What I want to know, is whether there is anything I can do to make haskell work with my functions.

module Church where

type (Church a) = ((a -> a) -> (a -> a))

makeChurch :: Int -> (Church a)
makeChurch 0 = \f -> \x -> x
makeChurch n = \f -> \x -> f (makeChurch (n-1) f x)

numChurch x = (x succ) 0

showChurch x = show $ numChurch x

succChurch = \n -> \f -> \x -> f (n f x)

multChurch = \f2 -> \x2 -> \f1 -> \x1 -> f2 (x2 f1) x1

powerChurch = \exp -> \n -> exp (multChurch n) (makeChurch 1)

predChurch = \n -> \f -> \x -> n (\g -> \h -> h (g f)) (\u -> x) (\u -> u)

subChurch = \m -> \n -> (n predChurch) m

Answer 1

The problem is that predChurch is too polymorphic to be correctly inferred by Hindley-Milner type inference. For example, it is tempting to write:

predChurch :: Church a -> Church a
predChurch = \n -> \f -> \x -> n (\g -> \h -> h (g f)) (\u -> x) (\u -> u)

but this type is not correct. A Church a takes as its first argument an a -> a, but you are passing n a two argument function, clearly a type error.

The problem is that Church a does not correctly characterize a Church numeral. A Church numeral simply represents a number -- what on earth could that type parameter mean? For example:

foo :: Church Int
foo f x = f x `mod` 42

That typechecks, but foo is most certainly not a Church numeral. We need to restrict the type. Church numerals need to work for any a, not just a specific a. The correct definition is:

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

You need to have {-# LANGUAGE RankNTypes #-} at the top of the file to enable types like this.

Now we can give the type signature we expect:

predChurch :: Church -> Church
-- same as before

You must give a type signature here because higher-rank types are not inferrable by Hindley-Milner.

However, when we go to implement subChurch another problem arises:

Couldn't match expected type `Church'
       against inferred type `(a -> a) -> a -> a'

I am not 100% sure why this happens, I think the forall is being too liberally unfolded by the typechecker. It doesn't surprise me though; higher rank types can be a bit brittle because of the difficulties they present to a compiler. Besides, we shouldn't be using a type for an abstraction, we should be using a newtype (which gives us more flexibility in definition, helps the compiler with typechecking, and marks the places where we use the implementation of the abstraction):

newtype Church = Church { unChurch :: forall a. (a -> a) -> (a -> a) }

And we have to modify predChurch to roll and unroll as necessary:

predChurch = \n -> Church $ 
    \f -> \x -> unChurch n (\g -> \h -> h (g f)) (\u -> x) (\u -> u)

Same with subChurch:

subChurch = \m -> \n -> unChurch n predChurch m

But we don't need type signatures anymore -- there is enough information in the roll/unroll to infer types again.

I always recommend newtypes when creating a new abstraction. Regular type synonyms are pretty rare in my code.

Answer 2

This definition of predChurch doesn't work in simply typed lambda calculus, only in the untyped version. You can find a version of predChurch that works in Haskell here.