Let cn denote a Church numeral corresponding to the natural number
n. In particular, c0 = (\f x. x) and c1 = (\f x. f x). Our goal is to
derive a term diffs, so that (diffs ck cl) reduces to a Church numeral
that corresponds to a number abs(k-l). We can easily visualize the
algorithm of computing the diffs as follows. Let us imagine a data
structure 'list'. This data structure is realized by a constant 'nil'
(which signifies the empty list) and an operation 'up' that adds a
link to the existing list. We also need an operation empty? to check
if the list is empty and an operation 'down', which removes the link
from a non-empty list and returns the shortened list. We can easily
convert a Church numeral ck to a list of 'k' links: we iterate the
'up' function 'k' times on the empty list.  To compute (diffs ck cl)
we convert cl to a list of length l, and then apply a down-or-up
operation k times to the list. The down-or-up operation removes a link
from a list. If, however, it encounters an empty list, it "changes the
direction" and starts adding links. Obviously, the result is the list
whose length is abs(k-l). At the last step, we convert the list back
to the corresponding numeral.

To realize the above algorithm more conveniently, let us introduce
P-numerals, which are another representation of naturals in
Lambda-calculus. We shall see shortly where the name comes
from. Recall that the Church numerals are defined as

        c0 f x --> x
        c1 f x --> f (c0 f x) --> f x
        c2 f x --> f (c1 f x) --> f (f x)
        succ cn f x --> f (cn f x)

We define P-numerals as follows:

        p0 f x --> x { the same as c0 }
        p1 f x --> f p0 (p0 f x) --> f p0 x
        p2 f x --> f p1 (p1 f x) --> f p1 (f p0 x)
        succp pn f x --> f pn (pn f x)

The conversion from Church numerals to P-numerals is trivial:
        c2p cn = cn succp p0
The reverse conversion is trivial as well
        p2c pn = pn (\p seed. succ seed) c0

P-numerals represent the "list" we have mentioned earlier. Indeed,
'nil' is realized as p0, the 'up' operation is succp, the emptiness
testing is implemented as
        emptyp? pn = pn (\p seed . false) true
and the 'down' operation is "pn (\p seed . p) p0"

In the following, we would be using the lambda-calculator in Haskell
described in
        http://www.mail-archive.com/hask...@haskell.org/msg10769.html
Note that x ^ t denotes (\x . t) and x # y stands
for an application of x to y. The following is the literate Haskell code:

First, we load the calculator and the definitions of common lambda terms
(such as true, false, lif, and cons), as well as the definitions of the
Church numerals (constants c0, c1, c2 and c3 and the term succ).

Now we can define the diffs term, by literally following the algorithm
outlined above

(\ck. (\cl. (\arg. (\pn. pn (\pn. (\seed. (\c. (\f. (\x. f (c f x))))
seed)) (\f. (\x. x))) ((\p. p (\x. (\y. y))) arg)) (ck
(\arg. (\ud_flag. (\pn. (\p. (\x. (\y. p x y))) ud_flag
((\x. (\y. (\p. p x y))) (\x. (\y. x)) ((\pn. (\f. (\x. f pn (pn f
x)))) pn)) (pn (\prev. (\_. (\x. (\y. (\p. p x y))) ud_flag prev))
((\x. (\y. (\p. p x y))) (\x. (\y. x)) ((\pn. (\f. (\x. f pn (pn f
x)))) (\f. (\x. x))))))) ((\p. p (\x. (\y. x))) arg) ((\p. p
(\x. (\y. y))) arg)) ((\x. (\y. (\p. p x y))) (\x. (\y. y))
((\cn. cn (\pn. (\f. (\x. f pn (pn f x)))) (\f. (\x. x))) cl)))))

I submit the "Haskell" format for the term was more comprehensible.

Here are a few tests:
        Main> eval $ diffs # c1 # c0
        (\f. f)  -- which is c1
        Main> eval $ diffs # c0 # c1
        (\f. f)  -- the same
        Main> eval $ diffs # c3 # c1
        (\f. (\x. f (f x))) -- which is c2
        Main> eval $ diffs # c1 # c3
        (\f. (\x. f (f x))) -- the same
        Main> eval $ diffs # c3 # c3
        (\f. (\x. x)) -- or c0

If we assume the normal or a similar lazy order of evaluation,
computing of an application of up_or_down takes only constant
time. Therefore, the overall complexity of 'diffs' is Theta(k+l), which
is the best one can hope for with unary representation of numerals.
If we used Church numerals internally when computing diffs, the
complexity would have been quadratic.

Let us relate the P-numerals and the list fold. We can choose the
following format for the unary representation of numbers in Haskell:

0  -- []
1  -- [[]]
2  -- [[[]],[]]
3  -- [[[[]],[]],[[]],[]]

This representation has the remarkable property that for all i>j,
repr(j) is the proper suffix of repr(i). This is of course a Peano
representation of integers. An integer n is represented by a list of
n links long, which we will call peano(n). The right fold operation
over such lists will have the following property:

    foldr f z peano(0) --> z
    foldr f z peano(n) --> f peano(n-1) (foldr f z peano(n-1))

Comparing these equations with the definition of P-numerals above, we
see that
        pn = \f z -> foldr f z peano(n)

which explains the name for P-numerals. We should also note that
P-numerals are indeed related to lists. We represent a list by a fold
combinator over it! This realization is in the spirit of
Lambda-calculus of representing data structures by functions.

Dealing with data structures such as [[[[]],[]],[[]],[]] is inconvenient
for many reasons. Therefore, we switch to a different format

0 -- []
1 -- [[]]
2 -- [[],[]]
3 -- [[],[],[]]

This format also has the same property that for i>j, repr(j) is a
proper suffix of repr(i). We can define the following fold operator:

        pn = \f z -> mfoldr f z (take n $ repeat [])

and the regular Church numerals as