> Christopher Wadsworth analyzed different properties of numeral systems and the requirements they have to fulfill to be useful for arithmetic.

> Specifically, he calls a numeral system adequate if it allows for a successor (succ) function, predecessor (pred) function, and a zero? function yielding a true (false) encoding when a number is zero (or not).

A numeral system is adequate iff it can be converted to and from Church numerals. Converting from Church numerals requires functions N0 and Nsucc so that

    Church2Num c = c Nsucc N0

while converting to Church numerals requires functions Nzero? and Npred so that

    Num2Church n = Nzero? n C0 (Csucc (Num2Church (Npred n)))

with an implicit use of the fixpoint combinator.

An interesting adequate numeral system is what i call the tuple numerals [1], which are simply iterates of the 1-tuple function T = λxλy.y x

So N0 = id, Nsucc = λnλx.n (T x), Npred = λnλx.n x id, and Nzero? = λnλtλf. n (K t) (K f).

These tuple numerals are useful in proving lower bounds on a functional busy beaver [2].

[1] https://github.com/tromp/AIT/blob/master/numerals/tuple_nume...

[2] https://oeis.org/A333479 (see bms.lam link)

If you’re “into” de Bruijn numerals or Project Euler then you might be familiar with this little treat:

https://projecteuler.net/problem=941

Otherwise, have a go and don’t spoil it! (I have failed thus far.)

Just use Scott-Mogensen encoding, seriously.

    Zero = z. s. z
    Succ = n. z. s. s n

    isZero = n. n True (_. False)
    pred   = n. n Zero (r. r)

Addition requires explicit recursion, however (since numbers aren't folds), so I guess you'll have to either use Y combinator or closure-convert manually:

    add' = add'. m. n. m n (r. Succ (add' add' r n))
    add = add' add'

In any case, arithmetic operations can't be made fully constant-time for obvious reasons so whether your prefer this to Church numerals is a matter of taste. However, for lists/tuples the ability to execute head/tail/cons in constant time is much more important in practice than being able to do append in constant time.