Hi Folks,
The following is my summary of section 3.7 of Richard Bird's book, "Introduction to Functional Programming using Haskell."
In most programming languages Booleans and numbers are built-in values. But suppose they weren't, how would you implement decisions and how would you do 'some thing' a number of times?
Alonzo Church realized in the 1940's that Boolean and numeric values can be implemented as functions. In fact, he realized that the function is the only primitive needed in a programming language.
Functions that implement Boolean values are known as Church Booleans (Cbool) and functions that implement numeric values are known as Church numbers (Cnum).
Below I show how to implement the Boolean true and false values as functions. Then I show to implement the logical functions 'and', 'or', and 'not' so that they operate on the true and false functions.
-------------------------------
The Cbool Type Synonym
-------------------------------
First I define a type synonym 'Cbool a'. It is a synonym for any function that takes two arguments of the same type and returns a result of the same type:
type Cbool a = a -> a -> a
Notice that it is a parameterized type synonym which means that it can be customized by replacing 'a' with any type. For example, 'Cbool Integer' is a synonym for any function that takes two arguments of type Integer and returns a result of type Integer:
Integer -> Integer -> Integer
Interestingly, the 'a' can be replaced with 'Cbool a'. So 'Cbool (Cbool a)' is a synonym for any function that takes two arguments of type 'Cbool a' and returns a result of type 'Cbool a':
Cbool a -> Cbool a -> Cbool a
The benefit of using type synonyms is that it enables us to work at a higher level of abstraction. Rather than working with "a function that takes two arguments of the same type and returns a result of the same type" we simply work with "the Cbool type" just as though it was a built-in type. That's nice.
---------------------------------
Functions for true and false
---------------------------------
What are the truth values - true and false - actually for? One might answer that they are for making decisions, for choosing between a pair of alternatives (x, y):
if true then x else y
We can capture this impression by defining true and false as functions. Here's how:
true is a function that picks the first alternative x.
false is a function that picks the second alternative y.
So true and false take two arguments of the same type and return a result of the same type. Hey, that's the Cbool type. So true and false are Cbool types.
true, false :: Cbool a
true x y = x -- true returns the first alternative
false x y = y -- false returns the second alternative
Let's experiment with the Cbool type synonym and with the true and false functions.
Below is a function, test1, which takes one argument - a Cbool Integer - and returns an Integer.
That is, test1 is a function that takes one argument - a function that takes two Integer arguments and returns an Integer - and returns an Integer.
test1 :: Cbool Integer -> Integer
test1 f = f 1 2
Since true and false are of type Cbool a, they are also of type Cbool Integer and therefore can be used as the argument to test1:
t1 = test1 true -- returns 1
t2 = test1 false -- returns 2
Observe that (+) is a function which takes two numeric arguments and returns a numeric result. So (+) is also a Cbool type:
(+) :: Cbool Num
t3 = test1 (+) -- returns 3
The following function, test1' is equivalent to test1 except it doesn't use the Cbool type synonym.
test1' :: (Integer -> Integer -> Integer) -> Integer
test1' f = f 1 2
t1' = test1' true -- returns 1
t2' = test1' false -- returns 2
t3' = test1' (+) -- returns 3
test1' is much less attractive than test1.
'Cbool Integer' is a nice compact type name that shields us from the underlying complexity and enables us to work at a higher level of abstraction.
Now let's see how to implement the logical operators 'not', 'and', and 'or' so that they operate on our true and false functions.
-----------------------
Implementing 'not'
-----------------------
'not' will be defined as a function which takes one argument that is of type Cbool.
Specifically, not's argument is 'Cbool a', where 'a' is 'Cbool a'.
So, not's argument is a function that takes two 'Cbool a' arguments and returns a 'Cbool a'.
not :: Cbool(Cbool a) -> Cbool a
Recall that true and false are of type Cbool a. We've seen that 'a' can be Integer. But 'a' can be any type, including Cbool a. So the true and false functions are suitable arguments for the 'not' function.
Here is the behavior we desire of the 'not' function: If not's argument is true, then return false. If not's argument is false, then return true. This function does the job:
not :: Cbool(Cbool a) -> Cbool a
not f = f false true
t4 = not true -- returns function false
t5 = t4 1 2 -- returns 2
------------------------
Implementing 'and'
------------------------
'and' is a function that takes two arguments. The first argument chooses between the second argument and false. If the first argument is true, then return the second argument. If the first argument is false, then return false.
and :: Cbool(Cbool a) -> Cbool a -> Cbool a
and f g = f g false
t6 = and true true -- returns function true
t7 = and true false -- returns function false
t8 = and false true -- returns function false
t9 = and false false -- returns function false
t10 = true `and` true -- returns function true (notice that infix notation is being used)
----------------------
Implementing 'or'
----------------------
'or' is a function that takes two arguments. The first argument chooses between true and the second argument. If the first argument is true, then return true. If the first argument is false, then return the second argument.
or :: Cbool(Cbool a) -> Cbool a -> Cbool a
or f g = f true g
t11 = or true true -- returns function true
t12 = or true false -- returns function true
t13 = or false true -- returns function true
t14 = or false false -- returns function false
t15 = true `or` true -- returns function true (note the use of infix notation)
Let's get some more experience working with the 'Cbool a' type. Recall that the 'a' in 'Cbool a' can be any type, including 'Cbool Integer' so let's look at a couple functions which use 'Cbool(Cbool Integer)'.
test2 takes one argument of type 'Cbool(Cbool Integer)' and it returns an Integer:
test2 :: Cbool(Cbool Integer) -> Integer
test2 f = (f true false) 1 2
test2 uses its argument to choose between true and false. The result is then applied to 1 2. If test2 is given true as its argument, then true is chosen, which then selects 1. If test2 is given false as its argument, then false is chosen, which then selects 2.
t16 = test2 true -- returns 1
t17 = test2 false -- returns 2
test3 takes one argument which is a 'Cbool(Cbool Integer)' and it returns a 'Cbool Integer':
test3 :: Cbool(Cbool Integer) -> Cbool Integer
test3 f = f true false
test3 chooses between true and false and returns the choice. If test3 is given true as its argument, then true is returned. If test3 is given false as its argument, then false is returned. Thus, test3 is an identity function for true and false.
t18 = test3 true -- returns function true
t19 = t18 1 2 -- returns 1
We are finished with Church Booleans (Cbool). We now examine Church numbers (Cnum).
---------------------
Church Numbers
---------------------
What are the natural numbers actually for? One might answer that they are for controlling the number of times that 'some thing' is to be done.
We can capture this impression by defining the numbers as functions.
Let f denote the 'thing to be done'.
f is a function.
Numbers are used to control the number of times that f should be applied to its arguments.
Each number behaves like this: when given some function f it returns the appropriate number of applications of f.
'zero' means that f is to be applied no times.
Thus, zero f returns the identity (id) function
zero f = id
'one' means that f is to be applied once.
Thus, one f returns f
one f = f
'two' means that f is to be applied twice.
Thus, two f returns f . f
two f = f . f
And so forth.
So each number takes a function (a -> a) as its argument and returns a function (a -> a):
zero, one, two :: (a -> a) -> (a -> a)
The returned function may then be applied to its arguments.
Here are some examples of using numbers:
Let f be this function: append the string "world"
f = (++ "world")
Let the argument to the returned function be: "Hello"
t20 = zero f -- returns id
t21 = t20 "Hello" -- returns "Hello"
t22 = one f -- returns f
t23 = t22 "Hello" -- returns "Helloworld"
t24 = two f -- returns f . f
t25 = t24 "Hello" -- returns "Helloworldworld"
We've seen what zero f does, what one f does, and what two f does. But what does zero do, what does one do, and what does two do?
What is zero? one? two?
'zero' is a function that, given any function h, it ignores h and returns id. We can express that using a Lambda (anonymous) function:
(\h -> id)
Let's take an example: apply that Lambda function to f
(\h -> id) f
= id
'one' is a function that, given any function h, it applies h once:
(\h -> h)
Let's take an example: apply that Lambda function to f
(\h -> h) f
= f
'two' is a function that, given any function h, it applies h twice:
(\h -> h . h)
Let's take an example: apply that Lambda function to f
(\h -> h . h) f
= f . f
-------------------------------
The Cnum Type Synonym
-------------------------------
Let's create a type synonym for (a -> a) -> (a -> a)
We call the type synonym Cnum
type Cnum a = (a -> a) -> (a -> a)
We've seen that zero, one, and two are Church numbers
zero :: Cnum a
one :: Cnum a
two :: Cnum a
test4 is a function that takes one argument which is a 'Cnum String' and it returns a String
test4 :: Cnum String -> String
test4 cn = cn f "Hello"
test4 appends cn copies of "world" onto "Hello"
t26 = test4 zero -- returns "Hello"
t27 = test4 one -- returns "Helloworld"
t28 = test4 two -- returns "Helloworldworld"
Let's trace the evaluation of t28
t28 = test4 two
= two f "Hello"
= (f . f) "Hello"
= ((++ "world") . (++ "world")) "Hello"
= (++ "world") "Helloworld"
= "Helloworldworld"
----------------------------------------
Predecessor of a Church Number
----------------------------------------
Each Church number (except zero) can be defined in terms of its preceding number. Thus two f can be defined using one
two f = f . one f
And one f can be defined using zero
one f = f . zero f
--------------------------------------
Successor of a Church Number
--------------------------------------
The successor of a Church number is defined by applying f one more time.
The successor of zero f is: f . zero f
The successor of one f is: f . one f
The successor of two f is: f . two f
Let's define a 'succ' function.
succ takes as input a Cnum and it returns the next Cnum. For example, succ zero returns one.
So the successor of a Church number, cn, is a number such that when applied to f, it applies f (cn + 1) times. This can be implemented using a Lambda function:
succ :: Cnum a -> Cnum a
succ cn = (\h -> h . cn h)
t29 = succ zero -- returns (\h -> h . zero h)
-- (\h -> h . id)
t30 = t29 f "Hello" -- returns (\h -> h . id) f "Hello"
-- (f . id) "Hello"
-- "Helloworld"
t31 = succ one -- returns (\h -> h . one h)
-- (\h -> h . h)
t32 = t31 f "Hello" -- returns (\h -> h . h) f "Hello"
-- (f . f) "Hello"
-- "Helloworldworld"
t33 = succ two -- returns (\h -> h . two h)
-- (\h -> h . h . h)
t34 = t33 f "Hello" -- returns (\h -> h . h . h) f "Hello"
-- (f . f. f) "Hello"
-- "Helloworldworldworld"
--------------------------------------------------------------------------
Convert Natural Numbers to Church Numbers and Vice Versa
--------------------------------------------------------------------------
First we create a program that converts natural numbers into Church numbers.
The Church number for 0 is zero. The Church number for 'n' is the successor of the Church number for (n - 1).
church :: Int -> Cnum Int
church 0 = zero
church n = succ (church (n-1))
g = (+1)
t35 = church 0 -- returns zero
t36 = t35 g -- returns id
t37 = t36 0 -- returns 0
t38 = church 1 -- returns one
t39 = t38 g -- returns g . id
t40 = t39 0 -- returns 1
t41 = church 2 -- returns two
t42 = t41 g -- returns g . g . id
t43 = t42 0 -- returns 2
t44 = church 5 -- return five
t45 = t44 g -- returns g . g . g . g . g . id
t46 = t45 0 -- returns 5
Next, we create a program that converts Church numbers into natural numbers.
For Church number, cn, the natural number is obtained by applying cn to (+1) 0.
natural :: Cnum Int -> Int
natural cn = cn (+1) 0
t47 = natural zero -- returns 0
t48 = natural one -- returns 1
t49 = natural two -- returns 2
t50 = natural (church 5) -- returns 5
-------------------------------------------------------------------------------------------
Arithmetic with Church Numbers - addition, multiplication, exponentiation
-------------------------------------------------------------------------------------------
We can perform arithmetic with Church numbers.
'plus cn1 cn2' means the 'thing to be done' is to be applied cn2 times and then cn1 times.
plus :: Cnum a -> Cnum a -> Cnum a
plus cn1 cn2 = (\h -> (cn1 h) . (cn2 h))
t51 = plus two one -- returns three
t52 = t51 g 0 -- returns 3
Let's trace that example:
plus two one = (\h -> (two h) . (one h))
= (\h -> (h . h) . (h))
= (\h -> h . h . h) (+1) 0
= ((+1) . (+1) . (+1)) 0
= 3
Here's how to multiply two Church numbers:
times :: Cnum a -> Cnum a -> Cnum a
times cn1 cn2 = cn1 . cn2
Notice that multiplication involves composing the two Church numbers.
Composing cn1 and cn2 means that the 'thing to be done' is to be applied cn2 times and then for each of them apply the 'thing to be done' cn1 times.
t53 = times two two -- returns four
t54 = t53 g 0 -- returns 4
Let's trace that example:
times two two = (\h -> h . h) . (\h -> h . h)
= ((\h -> h . h) . (\h -> h . h)) g 0
= (\h -> h . h) (g . g) 0
= ((g . g) . (g . g)) 0
= 4
Here is a function for exponentiation of Church numbers:
exponentiation e m = e m
e = exponent, expressed as a Church number
m = mantissa, expressed as a Church number
Notice that exponentiation involves applying the first Church number to the second Church number.
The exponent expands h some number of times. Suppose e is two:
(\h -> h . h)
Then, e is applied to m, which has expanded h some number of times. Suppose m is three. Here is e applied to m:
(\h -> h . h) (\h -> h . h . h)
So m is repeated e times:
(\h -> h . h . h) . (\h -> h . h . h)
Thus, m is raised to the e power.
three :: Cnum a
three f = f . f . f
t55 = exponentiation two three -- returns three**two = nine
t56 = t55 g 0 -- returns 9
Let's trace that example:
exponentiation two three
= (\h -> h . h) (\h -> h . h . h)
= (\h -> h . h . h) . (\h -> h . h . h)
= ((\h -> h . h . h) . (\h -> h . h . h)) g 0
= (\h -> h . h . h) (g . g . g) 0
= ((g . g . g) . (g . g . g) . (g . g . g)) 0
= 9
/Roger
