Representing Integers as Functions (Church Numerals?)

Apply equational reasoning1, and abstraction. You have

one   f x =       f x                       -- :: (a -> b) -> a -> b
two   f x =    f (f x)   -- = f (one f x)   -- :: (a -> a) -> a -> a
three f x = f (f (f x))  -- = f (two f x)   -- :: (a -> a) -> a -> a
--                            ~~~~~~~~~~~

Thus, a successor function next is naturally defined, so that three = next two. Yes, it is as simple as writing next two instead of three in the equation above:

next :: ((b -> c) -> a -> b) -> (b -> c) -> a -> c
-- three f x = next two f x = f (two f x)   -- `two` is a formal parameter
--                            ~~~~~~~~~~~
next                num f x = f (num f x)   -- generic name `num`

zero :: t -> a -> a
zero f x = x

This captures the pattern of succession. f will be used as a successor function, and x as zero value. The rest follows. For instance,

plus :: (t -> b -> c) -> (t -> a -> b) -> t -> a -> c
plus two one f x = two f (one f x)   -- formal parameters two, one
              -- = f (f (one f x))   -- an example substitution
              -- = f (f (f x)        --   uses the global definitions
              -- = three f x         --   for one, two, three

i.e. one f x will be used as a zero value by two (instead of the "usual" x), thus representing three. A "number" n represents a succession of n +1 operations.

The above, again, actually defines the general plus operation because two and one are just two formal function parameters:

Prelude> plus three two succ 0    -- built-in `succ :: Enum a => a -> a`
5
Prelude> :t plus three two
plus three two :: (a -> a) -> a -> a
Prelude> plus three two (1:) [0]
[1,1,1,1,1,0]

The key thing to gasp here is that a function is an object that will produce a value, when called. In itself it's an opaque object. The "observer" arguments that we apply to it, supply the "meaning" for what it means to be zero, or to find a successor, and thus define what result is produced when we make an observation of a number's value.

1i.e. replace freely in any expression the LHS with the RHS of a definition, or the RHS with the LHS, as you see fit (up to the variables renaming of course, to not capture/shadow the existing free variables).


To convert a number to a numeral you can use something like:

type Numeral = forall a . (a -> a) -> (a -> a)

toChurch :: Int -> Numeral
toChurch 0 _ x = x
toChurch n f x = f $ toChurch (pred n) f x

fromChurch :: Numeral -> Int
fromChurch numeral = numeral succ 0