What does this haskell expression mean

Question

I just started learning about Haskell and I'm trying to use the lambda calculus in Haskell. I found this expression which converts a church numeral to a number but I can't seem to figure out what the 0 in this expression means. I can't find it anywhere:

zero = (\f -> \x -> x)
one = (\f -> \x -> f x)
two = (\f -> \x -> f (f x))

getNum church = church (\x-> (x + 1)) 0

It's the very last zero that confuses me. Is it the base case or some argument to this lambda expression?

Answer 1

It's the second argument to the "church" function. Church numerals are a way of doing counting in Lambda Calculus. They work in a similar way to Peano numbers. In those you count like this

Z = 0
S Z = 1
S S Z = 2

Read "Z" as "Zero" and "S" as "Successor". So 1 is the successor of 0, and 2 is the successor of 1. In effect its unary counting.

In Lambda Calculus you only have function application, so you can define 2 as a function that takes an argument "f" and applies it twice.

In your example the Church numbers zero, one and two are defined. Each is a function that takes two arguments. The first argument is the function to apply, and the second is the value to apply it to. The getnum function uses the function succ (i.e. \x -> x+1) which is then applied N times to the base case "0".

You could also define

getPeano church = church ('S':) "Z"

This will prepend the right number of "S"s to the Z to translate a Church number into a Peano number.