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

Blast

You should make the type declaration type Church a = (a -> a) -> a -> a. Its cleaner, not different. – Allograph

Also note that it helps a ton to write out the type signatures. It will tell you exactly where the problem is... – Allograph

I ended up removing the type signatures, to see if ghci could infer them properly, and hopefully get rid of the error (the error has not changed)... also, I prefer the parentheses around the type. It makes it stand out more to me – Blast

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.

Bract

As for the type error, it happens because in Haskell polymorphic types must be instantiated only with monomorphic type arguments: in type Church = forall a. (a -> a) -> (a -> a) type variable a must be monomorphic, but in subChurch definition it isn't the case (in (n predChurch) type variable a is set to Church which is polymorphic). Here is detailed explanation: okmij.org/ftp/Haskell/types.html#some-impredicativity – Bradlybradman

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.

Diathermic

Thanks, that was the answer I was looking for. I was just wondering if there was some sort of magic I could do to make haskell not care about the type. I already have a definition that works in haskell, I just wanted to know if I could get the untyped version to work in haskell. Thanks again. – Blast

@Probie: Keep in mind that the first bit only refers to the simply-typed λ-calculus, which is akin to Haskell without any of: polymorphic types, type classes, data and newtype, and recursive bindings. – Breeching

Answer 3

I have encountered the same problem. And I solved it without adding type signature.

Here's the solution, with cons car copied from SICP.

cons x y = \m -> m x y
car z = z (\p q -> p)
cdr z = z (\p q -> q)

next z = cons (cdr z) (succ (cdr z))
pred n = car $ n next (cons undefined zero)

sub m n = n pred m

You can find full source here.

I'm really amazed after writing sub m n = n pred m, and load it in ghci without type error!

Haskell code is so concise! :-)

Fortin

This doesn't really work. If you look at the inferred types in GHCi, they're too specialized, so e.g. showChurch $ sub (plus three two) two gives type errors. – Cortezcortical

@Cortezcortical Oooops, you are right. I tested sub two one only. sub three two gives type errors. – Fortin