Lambda calculus in Haskell: Is there some way to make Church numerals type check?

Question

I'm playing with some lambda calculus stuff in Haskell, specifically church numerals. I have the following defined:

let zero = (\f z -> z)
let one = (\f z -> f z)
let two = (\f z -> f (f z))
let iszero = (\n -> n (\x -> (\x y -> y)) (\x y -> x))
let mult = (\m n -> (\s z -> m (\x -> n s x) z))

This works:

:t (\n -> (iszero n) one (mult one one))

This fails with an occurs check:

:t (\n -> (iszero n) one (mult n one))

I have played with iszero and mult with my constants and they seem to be correct. Is there some way to make this typeable? I didn't think what I was doing was too crazy, but maybe I'm doing something wrong?

Paratroops

Answer 1

Your definitions are correct, as are their types, when seen at top-level. The problem is that, in the second example, you're using n in two different ways that don't have the same type--or rather, their types can't be unified, and attempting to do so would produce an infinite type. Similar uses of one work correctly because each use is independently specialized to different types.

To make this work in a straightforward way you need higher-rank polymorphism. The correct type for a church numeral is (forall a. (a -> a) -> a -> a), but higher-rank types can't be inferred, and require a GHC extension such as RankNTypes. If you enable an appropriate extension (you only need rank-2 in this case, I think) and give explicit types for your definitions, they should work without changing the actual implementation.

Note that there are (or at least were) some restrictions on the use of higher-rank polymorphic types. You can, however, wrap your church numerals in something like newtype ChurchNum = ChurchNum (forall a. (a -> a) -> a -> a), which would allow giving them a Num instance as well.

Tibia

Wow, you're right. I did not expect something so fundamental to require higher-rank polymorphism but I guess that's what comes from the lambda calculus being untyped. – Paratroops

@singpolyma: One could argue that higher-rank polymorphism is itself fundamental to a polymorphic typed lambda calculus, not the extra limitations necessary to allow full type inference. – Tibia

@singpolyma: BTW,the mentioned above restrictions will come into play when you try to implement something like mult m n = m (plus n) zero which is a valid expression in untyped lambda but requires impredicative polymorphism in typed. Here is Oleg's workaround for that: okmij.org/ftp/Haskell/types.html#some-impredicativity – Tann

Answer 2

Let's add some type signatures:

type Nat a = (a -> a) -> a -> a

zero :: Nat a
zero = (\f z -> z)

one :: Nat a
one = (\f z -> f z)

two :: Nat a
two = (\f z -> f (f z))

iszero :: Nat (a -> a -> a) -> a -> a -> a
iszero = (\n -> n (\x -> (\x y -> y)) (\x y -> x))

mult :: Nat a -> Nat a -> Nat a
mult = (\m n -> (\s z -> m (\x -> n s x) z))

As you can see, everything seems pretty normal except for the type of iszero.

Let's see what happens with your expression:

*Main> :t (\n -> (iszero n) one n)
<interactive>:1:23:
    Occurs check: cannot construct the infinite type:
      a0
      =
      ((a0 -> a0) -> a0 -> a0)
      -> ((a0 -> a0) -> a0 -> a0) -> (a0 -> a0) -> a0 -> a0
    Expected type: Nat a0
      Actual type: Nat (Nat a0 -> Nat a0 -> Nat a0)
    In the third argument of `iszero', namely `(mult n one)'
    In the expression: (iszero n) one (mult n one)

See how the error uses our Nat alias!

We can actually get a similar error with the simpler expression \n -> (iszero n) one n. Here's what's wrong. Since we are calling iszero n, we must have n :: Nat (b -> b -> b). Also, because of iszeros type the second and third arguments, n and one, must have the type b. Now we have two equations for the type of n:

n :: Nat (b -> b -> b)
n :: b

Which can't be reconciled. Bummer.

Recipient