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?
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.