As you know Church numerals are the function representation of natural numbers in lambda calculus. As many functional languages can do, we can implement Church numerals in a wide variety of those functional languages. In Haskell we can do it too. The basis of Church numerals are the zero function and the successor functions. As you may know the zero function has the form of λy.(λy.z) that can be reduced to λyz.z and the successor function that has the form λwyx.y(wyx) with many applications as the natural numbers can have.
The application of the successor function can lead us to function application where we get subsequent natural numbers, the S or successor function applied to 0 — that looks as S.0 — can be applied as (λwyx.y(wyx))(λsz.z) and reduced to λsz.s(z), sequentially for all numbers as 1 = λsz.s(z), 2 = λsz.s(s(z)), 3 = λsz.s(s(s(z))), and so on. So we have an intermediate reduction by substitution in S.1 as λyx.y((λsz.s(z))yx). As Haskell has a very strong basis on this theoretical approach, we can use its type system and anonymous function constructs to build our church encoded numbers, so you must remember that function are treated as first class inhabitants.
A common implementation of Church Numerals in Haskell is the one provided by this article, also a more comprehensive explanation is placed here, where the implementation first starts with the Church type declaration, deriving in a currying type, which receives a function that returns a function.
module Main where
import Text.Show.Functions
type Church a = ( a -> a ) -> ( a -> a )
church :: Integer -> Church Integer
church 0 = y -> x -> x
church n = y -> x -> y ( church ( n - 1 ) y x )
unchurch :: Church Integer -> Integer
unchurch n = n ( x -> x + 1 ) 0
main :: IO ()
main = do let a = unchurch $ church 1
b = church 1
c = unchurch $ church 5
d = church 5
putStrLn ( show a )
putStrLn ( show b )
putStrLn ( show c )
putStrLn ( show d )
Special care should be taken with church function declaration, where it receives an integer and returns the church encoding for the given integer in the form of anonymous function or lambda expression. The case for the church zero declaration has the form non reduced version of the zero function λy.(λy.z), and other instances where n is different from zero, it has applied the successor function in a recursive form on its original form without reductions as λwyx.y(wyx). Both with the subsequent function application in the anonymous function application in the expression y -> x -> n.
The Lisp implementation looks very similar. You can derive to very similar constructs using lambda expression, so it should look like the following code.
(defun church(n)
(if (= n 0)
(lambda (m)
(lambda(y) y))
(lambda (m)
(lambda (x)
(funcall m (funcall (funcall (church (- n 1)) m) x)))
)))
(defun unchurch(c)
(funcall (funcall c (lambda(y)(+ y 1))) 0))
(format t "church: ~S~%" (church 5))
(format t "church: ~S~%" (unchurch (church 5)))
Enjoy using functional languages, they are very flexible ;)
Entries 