[Haskell-beginners] Understanding Type Synonyms, Church Booleans, and Church Numbers

Costello, Roger L. costello at mitre.org
Tue Dec 18 11:29:01 CET 2012


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



More information about the Beginners mailing list