One such model, implemented in a functional framework, has been invented by Church, but the idea is much older, comes from Peano. (Later on, Rosser added some reasoning to the idea of Church, and even now some people work on Church numerals. Find the nice article of Ralf Hinze: "Church Numerals, Twice" on the Web!) We basically need two notions: the zero, which is an irreductible concept (whether you write it as 0, `""` or `[]` is irrelevant), and the notion of *successor*, permitting to pass from a number to its ... successor, what else?... This successor passes from 4 to 5, from `"****"` to `"******"`, etc., throw one pebble more... Without knowing which *instance* of numbers is being used, we shall implement numbers as functions over those zero and successor. A number `n` is instantiated as `n s z`, where `z` is (for example) `""`, and `s` is the operator `('*':)`, etc. Or, `z=0; s=(1+)`...

zero s z = zwhich means that the instantiation of zero retrieves exactly what we have put in as zero; the successor is irrelevant. For people who love the combinatorial notation, there exists a parameter-less definition:

zero = flip constwhere

flip f x y = f y x const x y = xare standard Curry combinators, the first change the order of arguments of a binary function, and the second applies to two objects and takes the first one. If you wish, you may also write:

(f . g) x = f (g x)The next step is

one s z = s zwhose meaning is obvious. One can suppress the trailing args, which gives

one = idYes, "one" is the identity. Cute, isn't it? Later we shall see that it is a natural property related to the fact that it is a neutral element for multiplication. Perhaps it would be useful to introduce here some testing interface, the function

sh n = n (1+) 0(unless you prefer

one = \f -> fis obviously id, for the zero we also have a stylistically similar construct

zero = \f -> idas we have already seen above. Of course

two = \f -> f . f three = \f -> f . f . fetc.,

incr n s z = n s (s z) --or= s (n s z)

incr n s = n s . sand now

one = incr zeroTest:

incr n s z = s (n s z)or

incr n s = s . n sExercice. Prove inductively that

add n m = n incr mIt looks like guessing... But, if we know the semantics of a generic

Or, we can reason on the instance level; we shall concatenate the chain of m successors with the chain of n successors. Or, we assemble m, and we continue n times more the instance incrementation:

(add n m) s z = n s (m s z)or

add n m s = n s . m sExercice. Show that

Anyway... We can now construct `two = add one one; three = add two one; four = add two two` etc.

mul n m s z = n (m s) zor:

We may think differently. n times m is adding m to zero n times (or vice-versa). So, this should also work:

-- mul n m=(add m ...(add m (add m zero)))or-- n times

mul n m = n (add m) zeroExercice. Once again, try to demonstrate the equivalence of the two variants, the commutativity, the associativity, and also the distributivity:

*Anyway, there is one property of all those constructs which should be acknowledged: none of the definition above is recursive! Think a little bit: could it be recursive? Recurring on WHAT?* Compare this with the more popular "naive" (not so...) construction of addition based on patterns:

0 + x = x (incr n) + x = incr (n+x)etc. This is adapted to sequential data-like number constructions:

data Nat = Zero | Succ Natfor which obviously:

add Zero n = n add n Zero = n add (Succ n) m = incr (add n m) --works well. This is the original Peano numeral system. I have seen somewhere somebody calling this model "Peano-Church numerals". Well... This is a different model. The relation between the two can be found in the Ralf Hinze 'Theoretical Pearl' article: "Church Numerals Twice". Of course, in the true P-Ch model the additions, the multiplications, etc. reduce to the applications of the successor, so constructing a number 765176596197659 (by any means...) will take quite a time, even without any explicit primitive recursivity. This is intriguing, where the computer wastes its time?... Note that while the addition in the recursive Peano model has the complexity n (linear), in the Church/Rosser formulation it is - apparently - constant. Multiplication idem, while in the recursive model it goes like n*m, as to be expected...+ commut., not needed (?)

-- pow n m = (mul n ( ... (mul n (mul n one)))) --orm times

pow n m = m (mul n) oneThis is OK, but a bit boring. For the inverted application formula we may prove easily that

On the other hand

pow n (incr m) = incr m n = m n . nEnough? Don't forget that the composition is the multiplication, so we got n

The Rosser formula for the exponentiation has an interesting set-theoretical face. You should/might know that in the theory of sets, for any sets A and B, the notation B^{A} denotes the *set of all functions from A to B*. Typically, when teaching this stuff, one applies the argument based on cardinality. Adding one element to A, permits to find |B| more mappings, from the additional element to all of B. So, the number of mappings is multiplied by |B|, in agreement with : B^{A+1} = B^{A} * B. Here we see naturally that "exponentiation = inverse application".

A warning... You don't see any recursivity, but, please, try: `pow ten ten` or something not too far. On my GHCi I get immediately the stack overflow message, already for 7^{7}, unless I change the stack length.
Well, I lied. Not immediately. But, eventually. So somebody stacks things. Who and *where*? You won't pass from the kindergarten to the primary FP school unless you answer this question...

The Peano numerals with their arithmetics can be expressed in terms of a specific 'fold' function (all below is inspired by the Ralf Hinze paper), defined as

fold s z Zero = z fold s z (Succ n) = s (fold s z n)If you have some acquaintance with standard Haskell

We see that

fold Succ Zero Zero = Zero fold Succ Zero (Succ Zero) = Succ (fold Succ Zero Zero) = Succ Zeroand if

fold Succ Zero (Succ n) = Succ mwhich implies:

zero = flip const --keep theseone = id add n m = fold Succ m n mul n m = fold (add m) zero n pow n m = fold (mult n) one m

Now "re-derive" the more abstract Church numerals from the Peano model:

We see thattype Church = (a->a) -> a -> anat :: Church -> Natnat c = c Succ Zerochurch :: Nat -> Churchchurch n = \s z -> fold s z n

(nat . church) x = nat (\s z -> fold s z x) = fold Succ Zero x = xso

(church . nat) x = \s z -> fold s z (x Succ Zero) --cannot be reduced, since[1]

Wadler claims that for *any* function `a : A -> A'` we have

awhere the functorial counterpart of^{*}. r_{A}= r_{A'}. a^{*}

We cannot spend more time on that, but we shall know that the theorem is not restricted to lists, but to all polymorphic types. For Church, the parametricity condition can be formulated/used as follows. Let `x : Church`. Let `A,A'` be arbitrary types. Then for all `f : A->A; f' : A'->A'`, and `h : A->A'` we have

h . xIntuitively it is clear._{A}f = x_{A'}f' . h <<== h . f = f' . h

fold s z . Succ = s . fold s z --we obtainCheck this!

fold s z . x Succ = x s . fold s z --So:Prove it!

This completes the proof,[1]= \s z -> fold s z (x Succ Zero) = \s z -> (fold s z . (x Succ)) Zero = \s z -> (x s . fold s z) Zero = \s z -> x s (fold s z Zero) = x s z --(from the def of fold)

pdecr (Succ n) = n pdecr Zero = Zero --The subtraction iterates the decrementation:sorry, no other value available...

psub n Zero = n psub n (Succ m) = psub (pdec n) mBut in the functional version we don't have patterns, since we don't have any constant data, everything is parametric. For some time Church himself thought that the subtraction is not possible in this model. But it is, although its complexity is awful. The reasoning goes as follows: begin with zero, and keep counting until n, but storing the last two numbers. Then when you get n, the previous one is its predecessor.

suc (_,b) = (b,incr b) dec n = x where (x,_) = n suc (undefined,zero)There is no recursivity either, but we are not dupe, we know that

sub n m = m dec nbut all attempt to

The solution of the dilemma exists, but it is a bit ugly, and formally a bit advanced, using the s.c. existential types. The idea is to *hide* the type of the Church numeral in such a way that it can be instantiated differently in the same construct in which it appears several times. We remind that a Church numeral - in general - is a function which iterates its 'successor' argument, producing the 'iterated successor', so the generic type is `(a->a)->(a->a)`. We may declare thus

type Church = forall a . (a->a)->a->a --and the last declaration turns out to be faulty. The Rosser forms for the addition, multiplication and power are OK. But this definition:and thenzero :: Church zero = flip const one :: Church ... incr :: Church->Church

The solution is to hide theInferred type is less polymorphic than expected

Quantified type variable `a' escapes

newtype Church = Ch (forall a . (a->a)->(a->a))etc. Let's recall the definitions in order to keep them in one place, with two variants of some entities, Rosser, and "high level" (primed):

sh (Ch n) = n (1 +) 0 :: Integer --Also, the decrementors and the subtraction:For testingzero :: Church zero = Ch (flip const) one :: Church one = Ch id incr :: Church->Church incr (Ch n) = Ch (\s -> n s . s) one' = incr zero add' (Ch n) m = n incr m add (Ch n) (Ch m) = Ch (\s -> n s . m s) two = add one one two' = incr one three = add one two three' = add' one' two' -- =================================== mul (Ch n) (Ch m) = Ch (n . m) mul' (Ch n) m = n (add m) zero pow (Ch n) (Ch m) = Ch (m n) four = mul two two five = add two three six = mul two three six' = mul' two' three' seven = add three four eight=pow two three nine = pow three two ten = mul two five

dec (Ch n) = Ch (\s z -> fst (n (\(_,x)->(x,s x)) (undefined,z))) dec' (Ch n) = fst (n (\(_,x)->(x,incr x)) (undefined,zero)) sub n (Ch m) = m dec n sub' n (Ch m) = m dec' nwork (apparently) correctly. Recall that

cons x y f = f x y car f = f const cdr f =f (flip const)The partial application

data Rel = LT | EQ | GT --But for the Church numerals? We cannot compare functions, even "boxed" in a constructorGHC Base defines them.p_ord Zero Zero = EQ p_ord (Succ a) (Succ b) = p_ord a b p_ord _ Zero = GT p_ord _ _ = LT

iszero (Ch n) = n (\z -> False) Truewhich doesn't need a conditional

We end these notes here, leaving to the reader the functional construction of Booleans, of `Rel`, of a conditional `if` (or something equivalent), and of other goodies which show that the lambda calculus gives you the Universe...